Hi,
I would like to run SVA for the following requirement, which I referenced from https://verificationacademy.com/verification-horizons/march-2018-volume-14-issue-1/sva-alternative-for-complex-assertions:
Requirements:
The requirements for this model, as demonstrated in the figure below, are:
Upon a rose of go, data is sent on a data bus
Data is only valid when the vld signal is true
The checksum chksum is on the data bus and is asserted upon the fall of go
Following the initialization of the checker sum, a running sum with overflow is computed at every cycle vld is true
In the chksum cycle, the checker sum must be compared against the chksum that appeared on the data bus.
Here is the code for the property:
int v_chk_sum;
function add_sum(BITS_4 _data);
v_chk_sum = (v_chk_sum==-1)? _data : v_chk_sum + _data;
$display(“*** %0t v_chk_sum=0x%0x”,$time, v_chk_sum);
endfunction
function reset_sum();
v_chk_sum = -1;
$display(“%0t-reset_sum:v_chk_sum=0”,$time);
endfunction
property p_check_sum;
@(posedge clk) ($rose(go), reset_sum()) |-> first_match((vld[->1],add_sum(data))[] ##1 (vld==0)[] ##1 $fell(go)) ##0 (v_chk_sum == -1 || v_chk_sum==data);
endproperty
When I run simulation using mti, the simulation log is:
*** 30000 v_chk_sum=0x5
30000-reset_sum:v_chk_sum=0
At 30000ns, the vld and go signal are triggered at the same time. As I expect, the reset_sum function should be called at first because this function is at antecedent. But the function add_sum is called at first.
Is this the tool’s issue or my faults?
Regards,
Nguyen Ton