SVA multiple start did not happen

SystemVerilog
1

Hi,
Here is the code, I was expecting that if either z |-> a1, or z|-> a2 should trigger a new trace. But by looking at the waveform and the log, the 1st part when z is high, there is only one trace triggered, and in the 2nd part when z is high again, all conditions did get triggered, just curious why they are not consistent???

sequence a1;
(a, $display(“New a1 starts at %t”, $realtime)) ##2 (b, $display(“a1 match at %t”, $realtime));
endsequence

sequence a2;
(c, $display(“New a2 starts at %t”, $realtime)) ##1 (d, $display(“a2 match at %t”, $realtime));
endsequence

sequence abcd;
a1 or a2;
endsequence

property zabcd;
@(posedge clk)
z |-> abcd ;
endproperty

assert property(zabcd) $display(“zabcd Pass at %t”, $realtime);

//-- log file –

KERNEL: New a1 starts at 30

ASSERT: Error: ASRT_0005 testbench.sv(27): Assertion FAILED at time: 70ns, scope: tb, start-time: 30ns

KERNEL: New a1 starts at 130

KERNEL: New a1 starts at 150

KERNEL: New a1 starts at 170

KERNEL: a1 match at 170

KERNEL: New a2 starts at 170

KERNEL: zabcd Pass at 170

KERNEL: New a1 starts at 190

KERNEL: a1 match at 190

KERNEL: New a2 starts at 190

KERNEL: a2 match at 190

KERNEL: zabcd Pass at 190

KERNEL: zabcd Pass at 190

RUNTIME: Info: RUNTIME_0068 testbench.sv (52): $finish called.

1280×208 38.3 KB

For more detail, please check below
edaplayground link …

2

In reply to plin317:

It would help to explain what output you were expecting. Perhaps you meant to use ‘$rose(z)’ instead of just ‘z’.

Also, it is a good practice to drive your stimulus offset from the posedge clk. In this example, use the negedge instead. That will make it clearer what the sampled values are for the assertion. That also avoids potential race conditions when the stimulus is driving your dut.

3

In reply to dave_59:

Hi Dave,
Based on the signal waveform, I was thinking that

  1. shouldn’t it start a new trace at #50 as (Z is 1’b1) and C is 1’b1, and at #70 D is 1’b1 to get a ‘a2 PASS’??
  2. same thing that it should start another trace at #70 as (Z is 1’b1) and C is still 1’b1, and at #80, D is 1’b1, so we should see another ‘a2 PASS’??
  3. we can see at #170 a2 start a trace and PASS at #190.

Did I have a wrong understanding of how ‘or’ works??

thanks
/Peter

4

In reply to plin317:

After playing around the test bench, it is working, so most likely the original issue is TB related. I am closing this one.