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

Hi,

In my opinion it is sensitive to if (en)

Thanks
Abhishek

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Wednesday, September 23, 2009 3:10 PM
To: sv-ac@eda.org; Korchemny, Dmitry; Lisa Piper; Eduard Cerny
Subject: [sv-ac] 17.3.1 Behavior of instantiated checkers // Need clarifications.

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<http://www.mailscanner.info/>, and is
believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.