[sv-ac] 17.3.1 Behavior of instantiated checkers // Need clarifications.

From: ben cohen <hdlcohen_at_.....>
Date: Wed Sep 23 2009 - 02:40:29 PDT
Below are LRM statements,  I have 2 questions on the procedural concurrent
assertion  instantiated in the checker as a procedural checker instance.
In this LRM example, there are three instantiations of c1: check_outside,
check_inside, and check_loop.
*Question 1: *How many times will p0 be visited in any time step?
once for check_outside, once for check_inside regardelss of the *en *signal,
and 4 times in check_loop
*Question 2*: Is p0 sensitive to the module check (*if (en*)), or is that
ignored? Based on the text of the LRM, I would think that
p0 is executed at every @ (posedge clk) and is insensitive to the
"procedural code" surrounding the checker.
Thus p0 is  added the queue regardless of the module test of *en. *
*
*
Thanks,
Ben
// LRM stuff
Procedural concurrent assertion statements in a checker shall be treated
just like other procedural
assertion statements as described in 16.15.6. However, static concurrent
assertion statements within a
checker are treated as if they appear at the checker’s instantiation point

*If the checker is procedural, all static assertion statements in the
checker are added to the pending*
*procedural assertion queue for their process when the checker instantiation
is reached in process*
*execution, and then may mature or be flushed like any procedural concurrent
assertion (see*
*16.15.6.2)*

Each of the three instantiations has its own version of sum, which is
updated at every positive clock
edge, regardless of whether that instance was visited in procedural code.
Even in the case of
check_loop, there is only one instance of sum, and it will be updated using
the sampled value of
in1

Each of the three instantiations will queue an evaluation of p0 at every
posedge of the clock (according
to the rules in 16.15.6), which will mature and report a violation during
any time step when sum
is not less than MAX_SUM, *regardless of the behavior of the procedural code
in module m*.

checker c1(event clk, logic[7:0] a, b);
  logic [7:0] sum;
  always @(clk) begin
     sum <= a + 1’b1;
     p0: assert property (sum < `MAX_SUM);
  end
..
endchecker

module m(...);
*c1 check_outside(posedge clk, in1, in2);*
always @(posedge clk) begin
  automatic logic [7:0] v1=0;
   *if (en*) begin  *c1 check_inside(posedge clk, in1, v1);   end*
  for (int i = 0; i < 4; i++) begin
   v1 = v1+5;
   *if (i != 2)* begin
   *c1 check_loop(posedge clk, in1, in_array[v1]);*
end
end

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Wed Sep 23 02:42:11 2009

This archive was generated by hypermail 2.1.8 : Wed Sep 23 2009 - 02:43:25 PDT