First_match usage

SystemVerilog
,
1

Looking for a solution why this is not working

property write;
int a;
int b;
int c;
@(posedge clk) ((cmd == 'hA && id == 'hB && req && ready), a = 'hB+42, b = 'hA+43, c= 'hC+44) ## [2:50] first_match(out[15:0] == 'h8 && out[31:16] == 'h9) |=> (next_out[15:0] == 'h10 && next_out[31:16] == 'h21);
endproperty

I see that if (cmd == 'hA && id == 'hB && req && ready) is matched two times in the 50 clock cycles, a,b and c are not getting updated with latest values to compare.

2

I tried this, seems to be working

property write;
int a;
int b;
int c;
@(posedge clk) first_match(A ## [2:50] b) |=> c);
endproperty

but it is choking when A occurs two times before b has arrived in 50 clock cycles.

3

In reply to gv_bing:

See if this explanation helps. Otherwise you need to show us a complete example.

4

Dave, I tried this, seems to be working, do you think it is correct?

property write;
int a;
int b;
int c;
@(posedge clk) first_match(A ## [2:50] b) |=> first_match(c));
endproperty

5

In reply to gv_bing:

You never stated your requirements, so how do we know what is correct? first_match(c) of a Boolean is unnecessary.

6

Sorry, I did not give the requirements correctly.

what im looking for is
at every clock cycle
watch for (cond1) then capture some data in local variables a,b
then wait for 2 to 50 clock cycles
check for another set of signals and compare with a
then wait for one more cycle
check for another set of signals and compare with b

it is something like this
module dummy (input cond1, cond2, cond3);
property write;
int a,b;
@(posedge clk) first_match (($rose cond1), a=addr, b=data) ## [2:50] (cond2 == a) |=> cond3 == b;
end property

assert (write);

endmodule

7

Case where it is failing is
cond1 may appear twice before cond2 can happen.

8

In reply to gv_bing:

Does cond1 overlap cond2? What about cond3?

9

In reply to dave_59:


property write;
  int a,b;
   @(posedge clk) first_match (($rose(cond1), a=addr, b=data) ## [2:50] cond2 == a) 
                     |=> cond3 == b;
end property

cond1 may appear twice before cond2 can happen.

At each clocking event there is an attempt, and if that attempt is successful the local Variables are updated, and they are local to that thread ONLY. If $rose(cond1)appears again in another cycle then a new thread is started, independently from the other thread.
During a successful attempt, Local variables are updated for that attempt in the sequence matched item. Again, those local variables are local to that thread for that attempt, and not for any other attempt.Read my paper https://verificationacademy.com/news/verification-horizons-march-2018-issue and understand the equivalency (but not implementation) of an SVA assertion using automatic tasks with automatic local variables that are started with fork-join.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle

10

No none of the conds will overlap.

Cond1 first then after 2 to 50 clks cond2 then next clock cycle cond3.

In reply to dave_59: