SV care-abouts with disable iff construct

During our SystemVerilog Assertions handbook writing, we identified a set of guidelines for effective coding of complex, scalabe properties.



Some of them have to deal with handling abort conditions during a property evaluation. In any practical protocol used to transfer data across, typical transfers occur over several clock cycles. There are situations where-in an abort condition triggers and ongoing evaluations needs to be aborted/terminated. IEEE 1800 SystemVerilog provides disable iff construct to model this. A sample code:

<br />property p_mstr_xfer;<br /> @(posedge clk) mstr_sel & sl_rdy |=> [1:20] mstr_start;<br />endproperty : p_mstr_xfer<br />a_p_mstr_xfer : assert property (disable iff (mstr_abort) p_mstr_xfer);<br /> <br />


Now consider the case that the aborting condition is not a simple signal, rather a temporal sequence. One might think of adding a sequence inside disable iff but that's illegal as per LRM. You typically get errors like:

// Tool errors out
// See: http://www.verificationguild.com/modules.php?name=Forums&file=viewtopic&t=2889

Sequence or property instance used in a non-temporal context
//

So how do you model an abort sequence then? Consider a temporal behavior being verified as shown below:



Now consider an abort sequence as in:




So how do you model this? SystemVerilog allows sequence.triggered inside disable iff. So you can do:

a_p_mstr_xfer : assert property (disable iff (mstr_abort_seq.triggered) p_mstr_xfer);

Enjoy SystemVerilog!

Ajeetha, CVC
www.noveldv.com