Blog: Assertions in Aldec Riviera-PRO

Following up on a previous blog, where I emphasised the necessity of using formal methods (i.e. assertions in our verification flow), I would like to explain how easy it is to use them in Aldec Riviera-PRO, with a practical example.

Those of you who have already used assertions will (hopefully) agree with me that they can be very useful in protocol checking and clock domain crossing. For those of you who are not familiar with assertions, I would strongly recommend you also read the earlier blogs by my colleague, Ian Gibbins; An Introduction to Assertion-Based Verification-Part 1 and Part 2.

Once ready to write assertions, your first question will likely be “where do I write them?”; Should they be in the RTL Model, or they should be part of the verification package? Let’s investigate the answer.

With the introduction of the “bind” construct, the assertions can be written in a separate file and can be bound to either the Verilog design or the VHDL design, providing more flexibility in where to place the assertions. It could also be included in the RTL Model, or can be written as a separate module and become part of the verification package as well.

That wasn’t a typo above, you can use SystemVerilog Assertions in VHDL design as well! If the assertions use internal signals of the design, then you can use “external” names in VHDL, or even an alias if you need to use the same external name many times, as supported in VHDL 2008.

The example that follows here uses the signal_agent feature, which Aldec supports.

You can understand more about the feature here. The assertions used in this example are testing the integrity of the clock domain crossing.

To check the integrity of NDFF synchroniser used to synchronise the asynchronous arst signal the following assertions have been used:

To check the integrity of Mux and Enable synchroniser used to synchronise the signal going from one domain to another, the following assertions have been used:

If the assertion module uses the same signal names as the target module then the bind-instantiation can be done using the SystemVerilog (.*) implicit port connections as shown below:

Running the simulations with debug option on and assertions enabled, the assertions are reported in a separate tab and can be added to the waveform if desired.

In case the assertions fails, then the failures are indicated in red and their fail count will indicate the number of failures.

It is easier to debug them by dragging in the waveform window as shown below:

Although this example was written in SVA, PSL assertions can also be simulated and debugged with similar ease.

I hope this brief overview of assertions has piqued your interest. If you’d like to try it out yourself, please don’t hesitate to contact FirstEDA to discuss your requirements and arrange an Aldec Riviera-PRO license for evaluation.

Interested in finding out more? Please contact us using the form here. We will be delighted to discuss your requirements and arrange a demonstration.