Assertion failing - no clue why!

SystemVerilog
, , ,
1

I am writing this assertion on the output signals of a module:

Requirement:
After the signal_eop happens, data valid should remain low for that port_id until signal_sop occurs for that same port_id.

property ChkDataValid;
int id;
@( posedge clk ) disable iff ( !rst_l )
( $rose(signal_eop), id=src_port)
|=> (!(data_valid & (src_port == id))) throughout ( (($rose(signal_sop)) && (src_port == id))[->1] );
endproperty
assert property ( ChkDataValid );

In my design, signal_eop rises on 1st clock cycle when data_valid=1 and src_port=0 and then on 2nd clock cycle signal_eop holds high but data_valid transitions to 0 with src_port=0. It fails on 2nd clock cycle.

please help me figure out what may be wrong with my assertion.

Thanks a lot.

2

In reply to somys:
You error is in the location of the “!” operator


You have:  
(!(data_valid & (src_port==id))) throughout ( (($rose(signal_sop)) && (src_port == id))[->1] );

Should be: 
(!data_valid && src_port==id) throughout ($rose(signal_sop) && src_port==id)[->1];

BTW, you have way too many parentheses, makes code hard to follow.

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

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy

3

In reply to ben@SystemVerilog.us:

In reply to somys:
You error is in the location of the “!” operator
You have:
(!(data_valid & (src_port==id))) throughout ( (($rose(signal_sop)) && (src_port == id))[->1] );
Should be:
(!data_valid && src_port==id) throughout ($rose(signal_sop) && src_port==id)[->1];

Thanks a lot for replying.

In my case, the src_port can be different than “id” at times and for those id’s, data valid is allowed to be 1 after $rose(signal_eop) is seen for a specific ID. data valid should be 0 until $rose(signal_sop) is seen for that same ID.

Doesn’t your solution require data_valid=0 and src_port==id all the time? and not allow src_port to be any different than that specific ID?

please explain since I am at loss with this understanding. Thanks a lot.

4

In reply to somys:
You need to clearly write your requirements in English.
It sounds like what you want is that for every associated data_valid && src_port pair
data_valid==0 until ($rose(signal_sop) && src_port==id)[->1].

Is this what you want?
See if this will work:

 

 first_match(
     (!data_valid && src_port==id ##[0:$]src_port!=id) [*0:$] ##1 
      $rose(signal_sop) && src_port==id
             );

Ben Ben@systemverilog.us

5

In reply to ben@SystemVerilog.us:

Ben,
thanks again. Would you please explain me this statement?

(!data_valid && src_port==id ##[0:$]src_port!=id)

Does this mean data_valid=0 when src_port==id and then src_port!=id after that until signal_sop happens?
I just need data_valid=0 whenever src_port==id after the signal_eop. Other than that both data_valid and src_port can take any values until signal_sop.

Thanks.

6

In reply to somys:

 
The sequence (à ##[0:$]b) is same as
a or a ##1 b or a ##2 b or... a ##n b

Thus, 

 (!data_valid && src_port==id ##[0:$]src_port!=id) [*0:$] ##1 
      $rose(signal_sop) && src_port==id
Says
 (!data_valid && src_port==I'd) can be followed by 0 or cycles of 
     src_port!=id).  With the [*0:$] that sequence is repeated indefinitely until
      $rose(signal_sop) && src_port==id
Hope that clarifies things.  The first_match is not really needed, but it is needed if you follow it with another test condition; I. E. first_match(some_sequence) ##0 seq

Ben systemverilog.us