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.
