'SV Assertion - Implication matches unique valid sequences

I have assertion property as assert property P;

property P;
@(posedge clk) A |-> ##[1:5] B;
endproperty 

clk - 0 1 2 3 4 5 6 7 8 9 10
A   - 0 1 0 1 0 0 0 0 0 0 0 
B   - 0 0 0 0 1 0 0 1 0 0 0

Here B = 1 at Clock num 4 satisfies assertion For A at Clocks 1 and 3.

How to write an assertion that checks for each A==1 we see a unique B==1 , meaning A=1 at Clk 1 should match against B=1 at Clk 4 AND A=1 at Clk 3 should match against B=1 at Clk 7.

Thanks,

system-verilogsystem-verilog-assertions


Solution 1:[1]

Depending on you max number of outstanding A request without ack I would do something like:

// modeling layer

int A_cnt, B_cnt

always @(posedge clk)
  if (A)
    A_cnt += 1
  if (B)
    B_cnt += 1

property P;
int A_id_lv
@(posedge clk) 
(A, A_id_lv=A_cnt) |-> ##[1:5] B && B_cnt == A_id_lv;
endproperty

I did not compile the code, this is a first draft, but I think the concept is there

Solution 2:[2]

int now_serving;
int ticket;
function int get_ticket();
  return ticket++;
endfunction

property P;
int serving_ticket;
@(posedge clk) (A, serving_ticket = get_ticket())  |-> ##[1:5] (B && now_serving == serving_ticket);
endproperty 

assert property(P) now_serving++;
else now_serving++;

This is uniqueness, credit to Ben, author of the systemverilog assertion handbook.

Solution 3:[3]

I don't think there is a way you can do it with modelling layer code. When the SVA is triggered on A==1 it cannot know if there has been a previous A that hasn't been "acked" with a B

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 Viktorinox
Solution 2 ouflak
Solution 3 Viktorinox

Related Questions