SVA sampling of always( a ##1 b[->1] )

SystemVerilog
, , ,
1

Hi All,

I an trying to understand the following procedural concurrent assertion

initial begin
  assert property(@(posedge clk) always(a ##1 b[->1]) );
end

Let’ say the posedge of clock occurs at t1,t2,t3,t4,….

(1) If a is sampled false at t1 then assertion fails

(2) If a is sampled true at t1 then it waits for assertion of b at the nearest posedge of clock

(Q1) For (2) would a be sampled again at t2 ?

(Q2) For (2) if b is sampled true at t10 then should a be true at the next clock t11 ?

(Q3) Does the concurrent assertion essentially check for ::

(a ##1 b[→1]) ##1 ( a ##1 b[→1] ) ##1 ( a ##1 b[→1] )

i.e (a ##1 b[→1])[*infinite times]

Thanks

2

There’s an implicit always property associated with a concurrent assertion property. Your procedural assertion is essentially the same as this concurrent assertion:

assert property(@(posedge clk) (a ##1 b[->1]) ;

a is sampled every clock cycle, which initiates a new concurrent assertion thread if it is true. If the condition is false, the assertion thread will fail. There could be multiple threads waiting for b to be true. However, b only needs to happen once to satisfy all the active threads.

3

Thanks Dave. To answer my own questions

(Ans1) a will be sampled for the next attempt.

Once a is sampled true for an attempt, it’s never sampled again for that attempt

(Ans2) a should be true for the attempt that starts at t11. For the attempt that started at t1, a isn’t sampled after t1

(Ans3) The embedded concurrent assertion is equivalent to

// 'always' is equivalent to sampling the sequence on every clock
assert property(@(posedge clk) (a ##1 b[->1]) ;

Two interesting observations ::

(1) If a is true at t1 and b is true at t10, the pass action block doesn’t execute ( even though the sequence matched )

(Q1) Does this implicitly mean pass action blocks are redundant for property expressions of type always(sequence) ?

(2) For the following stimulus

always #5 clk = !clk;
  
initial begin
  assert property(@(posedge clk) always(a ##1 b[->1])) $display("T:%0t Pass",$time); 
                                                 else  $display("T:%0t Fails",$time);
end

initial begin
  // a is false for the 1st attempt at t1
  #14; a = 1; // a is true for the 2nd attempt at t2

  // a is true for the attempts at t3,t4 & t5
  #40; a = 0; // a is false for the 6th attempt at t6

  // At t7 sequence (a ##1 b[->1]) matches for 2nd,3rd,4th and 5th attempt
  #10; b = 1; // a is false for the 7th attempt at t7
  #05; $finish();
end

The output I observe across all 4 EDA tools is

T:5 Fails

(Q2) Shouldn’t the output be as follows ?

T:5 Fails
T:55 Fails
T:65 Fails
// I am not sure if 4 pass action blocks should execute at t7 (T:65 units)
// for the attempts started at t2,t3,t4 & t5
4

I think that they are, for slightly silly reasons. Normally, an assertion looks something like:

foo_A: assert (@(posedge clk) P) $info("phew");

This means that at every posedge of the clock, we should be able to match property P (and the assertion will fail if we can’t). What’s more, we’ll print out an info message of “phew” each time one of the properties completes. (Obviously, don’t do this! The log file will be awful!)

Of course, we won’t necessarily get one “phew” appearing every cycle. For a silly (untested) example:

bar_A: assert (@(posedge clk) ##[0:10] not_yet ##1 now) $info("now!");

If the now signal gives a 1-cycle pulse every 5 cycles, we’ll get five properties completing (and printing “now”) at the same time every five cycles.

How about something even longer?

qux_A: assert (@(posedge clk) always (1 + 1 == 2)) $info("time has ended");

What does this mean? Well the always will use the current clocking (which has been established with the @(posedge clk).

Given the clocking that it has inherited, always (1 + 1 == 2) is a property that will run forever and check that 1+1 == 2 on every clock tick. Since this never finishes, the property will never finish matching, and we will never see the information message.

What’s worse, after N ticks, we will have started N parallel copies of the check. This seems a little silly!

5

I think I’ve finally understood this example, but it definitely isn’t expressed in the most conventional way! I believe it’s doing the following:

  • At the start of time, begin to execute an initial block.
  • This contains a concurrent assertion (rather unusual! You’d normally do this outside of the initial block).
  • That concurrent assertion waits until the posedge of clk and then tries to match the following property: always (a ##1 b[->1]), printing out a message on a match or a sequence of signals that doesn’t match.

Now, a property of the form always P (clocked on @(posedge clk) here) will fail to match if there is any clock edge where P doesn’t match. At that point, the always P property will have failed to match and we’ll get a message to tell us so. (And no other message)

In your example, the first posedge of the clock is at time 5. At that point, a is false. As such, the a ##1 b[->1] property does not match, so the always (a ##1 b[->1]) property doesn’t match (on its first iteration) and you get the failure message at time 5.

And nothing else! The property that you started in your initial block has completed (with failure).

Given that you were expecting multiple failures, I think you probably wanted something like this instead:

my_assertion:
  assert property (@posedge (clk) (a ##1 b[->1])
  display("T:%0t Pass",$time); 
  else $display("T:%0t Fails",$time);

If I’ve got it right, this will start trying to match at each positive clock edge (times 5, 15, …, 65) and:

  • The attempt at time 5 will fail (because a is false)
  • The attempts that start at time 15, 25, 35, 45 will complete at time 65 (the first cycle when b is true)
  • The attempts at times 55 and 65 will fail (because a is false again)

I think that’s what you were expecting to happen (and I think you’ll get four pass messages at time 65)

1 Like
6

I’ve been examining the LRM and believe it may be misleading or even incorrect when comparing implicit_always and explicit_always assertions They are not equivalent. Some of this discrepancy might stem from misunderstandings between static formal evaluation of a property versus dynamic simulation evaluation of the same property.

An explicit always property is either true or false once. It can be false at any time, but it can only be true at the end of the simulation. This slightly modified example gives me different results on different simulators, which means there is more work to be done clarifying the LRM.

module top;
  
  bit clk,a,b;
  initial repeat(20) #5 clk = !clk;
  
initial begin
  assert property(@(posedge clk) always(a ##1 b[->1])) $display("T:%0t Pass",$time); 
                                                 else  $display("T:%0t Fails",$time);
end

initial begin
  $dumpfile("dump.vcd"); $dumpvars;
  // a is false for the 1st attempt at t1
  #4; a = 1; // a is true for the 2nd attempt at t2

  // a is true for the attempts at t3,t4 & t5
  #40; a = 0; // a is false for the 6th attempt at t6

  // At t7 sequence (a ##1 b[->1]) matches for 2nd,3rd,4th and 5th attempt
  #20; b = 1; // a is false for the 7th attempt at t7
  #20 b =0;
  #60 ;
end
endmodule
1 Like
7

LRM 16.12.11 Always property mentions

A verification statement that is not placed inside an initial procedure
specifies that an evaluation attempt of its top-level property shall 
begin at each occurrence of its leading clocking event.

This tells us that there is only 1 attempt ( i.e the 1st attempt ) for concurrent assertion embedded in an initial block.

An exception to this rule is always( sequence ) as the same LRM section further states

In the following two examples, there is a one-to-one correspondence between the
evaluation attempts of p specified by the implicit always from the verification
statement implicit_always and the evaluation attempts of p specified by the
explicit always operator in explicit_always:

Implicit form: implicit_always: assert property(p);

Explicit form: initial explicit_always: assert property(always p);

This explicitly states that the number of evaluation attempts are same in both cases ( due to always )

I modified the embedded concurrent assertion to

initial 
 assert property(@(posedge clk) always((1,$display("Attempt starts at time:%0t",$time)) ##0 a ##1 b[->1]) ) $display("T:%0t Pass",$time); 
                                else  $display("T:%0t Fails",$time);

With Dave’ stimulus I observe output as ( across 2 EDA tools ) ::

Attempt starts at time:5
Attempt starts at time:15
Attempt starts at time:25
Attempt starts at time:35
Attempt starts at time:45
T:45 Fails

We observe an attempt on each clocking event, till the 1st error occurs.

There are no further attempts

With my stimulus I observe output as

Attempt starts at time:5
T:5 Fails

As the very 1st attempt fails there are no further attempts

@Dave, as my understanding there is a dedicated Mantis group to report issues in the LRM.

Similar to this forum, can anyone register and raise a ticket over there ?