I am trying to simplify a property to make my sva shorter and more readable.
I simply want to assert an error if (‘signals 1’ != ‘signals 2’). I also have a parameter ‘DELAY’ which means I want to compare ‘signals 1’ to ‘signals 2’ after ‘DELAY’.
The following code is what I currently have. But I want to simplify it to use one property:
module my_sva
#(
DELAY,
AWIDTH,
BWIDTH
)(
input [AWIDTH-1:0] a1,
input [AWIDTH-1:0] a2,
input [BWIDTH-1:0] b1,
input [BWIDTH-1:0] b2,
// ... Many more signal pairs with different and multi-dimensional widths
);
property prop_delay (s1, s2);
@(posedge clk)
always ##DELAY s2 != $past(s1,DELAY) |-> error;
endproperty
property prop_no_delay (s1, s2);
@(posedge clk)
s1 != s2 |-> error;
endproperty
generate
if (DELAY != 0)
begin :
assert property (prop_delay(a1,a2));
assert property (prop_delay(b1,b2));
end else begin
assert property (prop_no_delay(a1,a2));
assert property (prop_no_delay(b1,b2));
end
The problem is $past doesn’t accept DELAY=0, which is why I wrote the separate property.
With the two properties and the generate statement. A lot of code would end up repeated, which would be unreadable with hundreds of signal pairs.
Other solutions I’ve found look worse.
Is there a way to simplify this to one property that can use zero and non-zero delays?