SVA assertion to check pin on module isn't tied off to a constant

SystemVerilog
1

Hello Everyone,

I’m trying to write a SVA to check that a pin on a module isn’t tied off to a constant 1 or 0. I’ve tried various incantations of $stable() and eventually combined with $rose() or $fell().

Is there some way of detecting input constants with SVA assertions?

This is not for simulation, but rather is going to be fed into a Formal tool such as Jasper which will try and falsify the assertion.

Stated another way, Is there some way of checking that an input is a free variable in SVA?

The assertion I came up with is simulated by the formal tool and it can’t prove it as the dynamic pins may never toggle.

Anyway… Thanks for whatever help you can give.

not_tieoff : assert property (@(posedge clk) s_eventually (not $stable(u_sm.b)));

2

@josh_verilog
Try this

bit sig; 
initial  begin
    assert property( @(posedge clk) strong( $changed(sig)[->1] ) ) $display("T:%0t Pass",$time); 
                                                              else $display("T:%0t Fails",$time);
end

One interesting case is when ‘sig’ is assigned ‘1’ on the last posedge of clk just before simulation ends

3

Have_A_Doubt – Thank you.

That assertion does ‘work’ in that it fails for constants and passes for dynamic pins. The failures are immediate, but the passing cases take 24 seconds to fail per pin in Jasper. With hundreds of module instances in the design it’s rather ‘heavy-weight’ to do the detection for all of them. I’m going to keep looking at this to see if there’s a more efficient way to detect them.

Thanks.