OVL: The Free, Open Assertion Library You Can Use To Jump Start Your Formal Testbench

You’ve watched all the Verification Academy videos on getting started with formal verification, and even tried some of the examples included in the product documentation, but you are still struggling to build-up an effective “formal testbench” of assertions. If this sounds familiar, I have good news for you: there is a library of commonly needed assertions that has been compiled and optimized by a team of experts and that you can easily tailor to your needs – it is the free, efficient, standardized, Open Verification Language (OVL) library of assertions published by the Accellera Systems Initiative. Here is how you can take advantage of this gem of a resource:

First, the library is publicly available for download here:

http://www.accellera.org/downloads/standards/ovl

But chances are you already have it on your system – Mentor includes a copy of the library with the Questa PropCheck installation, so to confirm your IT/CAD/SysAdmin installed it go to $(INSTALL)/share/assertion_lib/OVL/std_ovl to confirm it’s there.

where the value of the INSTALL environment variable can be found via the Linux command line:

% qverify -install_path

 

But before digging into the code and how you can use it, some background: from the OVL project website, “The OVL library of assertion checkers is intended to be used by design, integration, and verification engineers to check for good/bad behavior in simulation, emulation, and formal verification.” Version 1.0 was published back in 2005, and it’s been continuously improved since – 2.8.1 is the latest version as of this writing, with 55 Verilog and 33 VHDL checkers. The overarching philosophy of the project was to provide an open, vendor-independent interface for functional verification using static and dynamic formal verification (and simulation engines too).

Getting Started

The number of available checkers in OVL may be overwhelming at first, so begin by considering the following guidelines. Remember, checkers can be used to ensure correct behavior and to seek out bugs.

• Add a checker “where” you want to verify. For example, where you expect a signal will be available for at least N-clock cycles, instantiate the ‘ovl_hold_value’ checker. To make sure that when one event happens then another will happen, use the ‘ovl_implication’ checkers.
• Add checkers to finite state machines (FSM) to check for illegal transitions (‘ovl_no_transition’), illegal states, and that you do not stay in a state longer than expected (‘ovl_change’). Use the coverage information obtained by the checker to ensure that all states of the FSM have been covered during simulation.
• Add the ‘ovl_range’ checker to check for legal ranges of addresses to memory structures and similar checks. You can use ‘ovl_underflow’ and ‘ovl_overflow’ for counters that are not allowed to wrap around.
• For memory structures, FIFOs are always a good target for adding checkers, because many bugs tend to creep in to them. For example, ‘ovl_fifo_index’ can be used to ensure that a FIFO pointer should never underflow or overflow.
• Add checkers like ‘ovl_handshake’ to interfaces to ensure the correct exchange of information. For example, if you send a request, you should receive a grant within a given number of cycles or that the ‘I am done’ signal must assert within a given set of cycles after the leader signal was raised.

Now let’s dive into an example …

Like properties you would write by hand, OVL assertion checkers include the property syntax itself, supplemented by code for issuing a message if the property “fires”, a severity level associated with the firing, and coverage element. Consider the following OVL “assert_never” property:

ovl_never #(
/* severity_level */     `OVL_ERROR,
/* property_type */    `OVL_ASSERT,
/* msg */                          “Register A < Register B”,
/* coverage_level */   `OVL_COVER_ALL) valid_checker_inst(
/* clock */                       clk,
/* reset */                       reset_n,
/* test_expr */              regA < regB );

This assertion checks that the ‘test_expr’ test expression does not evaluate to TRUE at each rising edge of a clock ‘clk’. In cases where the test expression contains unknowns, the checker can flag this situation as well.

The parameters in this simple ‘assert_never’ example illustrate the control an OVL user has over the individual assertions. For example, it is often the case that you want to guard and verify correct input and output behavior, and by using the ‘severity_level’, you can report the importance of the check. You could even stop the run, if desired, by setting the ‘severity_level’ to `OVL_FATAL.

The ‘property_type’ determines whether to use the assertion checker as an assert property or an assume property. Setting the ‘property_ type’ to OVL_ASSUME tells the verification engines that the OVL checker is a constraint that should not be checked but assumed to be true.

By default OVL checker firings are reported as a “VIOLATION”, but by using the ‘msg’ parameter you can specify that a more meaningful message is reported.  Regardless, if Questa PropCheck’s formal algorithms find a way that this property can be violated, PropCheck will show you a “counter example” waveform (nick-named a “CEX”) that shows exactly how your DUT can do something other than what’s specified by the property. Generally, this waveform is pointing you right to a bug – a true time saver vs. debugging a failed simulation test!

Finally, regarding the functional coverage aspect of this and all OVL properties: the capture of cover points is built into OVL checkers as per the ‘coverage_level’ parameter. This is a little more obvious in the following example of the “ovl_one_hot” OVL checker:

# OVL_COVER_POINT : ASSERT_ONE_HOT :

test_expr_change covered : time 1300 : DUT.

check_fsm_is_onehot.ovl_cover_t

This cover point reports if the ‘test_expression’ actually changed, providing insight into how well the test environment exercises the circuit and whether any coverage holes exist.

 

Usage Logistics

As noted above, users need to define the path to find the checkers; and the checker file is effectively treated the same as your own RTL file. The following is an example running OVL with PropCheck, starting with the make file compilation code:

c_ovl compile_ovl:

        $(VLOG) -sv -mfcu -cuname ovl_bind \

        properties/ovl/ovl_apb_access_arb.sv \

        properties/ovl/ovl_dp_fifo.sv \

        -y $(INSTALL)/share/assertion_lib/OVL/std_ovl +libext+.v \

        +incdir+$(INSTALL)/share/assertion_lib/OVL/std_ovl \

        +define+OVL_SVA+OVL_ASSERT_ON+OVL_COVER_ON+OVL_XCHECK_OFF

 

Then, run Questa PropCheck from the Linux command line:

% rm -rf log

% qverify -c -od log -do qft_files/run_pc.do

 

Note that it’s ok if you don’t have the permissions to modify the files in the OVL directory — you will just be using the library elements as-is. This is perfectly fine; and quite popular.

Of course, if you have the right to modify the library files under installation tree, you could hack the library code itself. Suffice to say this could lead trouble, so rather than modify it directly it is strongly recommend you cut&paste the necessary OVL assertions into a separate library of your own creation before tailoring them.

 

Summary

Hopefully the above has whet your appetite to learn more about using the OVL library. To get a deeper dive right now, there is a [free with registration] Verification Academy video presentation on this:

https://verificationacademy.com/sessions/introduction-open-verification-library

In general, reusing the OVL library code is a great way to combat “blank sheet of paper paralysis” and jump start your formal testbench because it’s always quicker to modify pre-verified checkers than create and debug new code. (Again, to preserve the integrity of the standardized library code, rather than modify it directly we recommend you cut&paste the necessary OVL assertions into a separate library of your own creation before tailoring them.)

It’s already there for you to try – just navigate to: $(INSTALL)/share/assertion_lib/OVL/std_ovl

What are you waiting for?

Joe Hupcey III and Jin Hou,
for the Questa Formal Team

 

P.S. Mentor enthusiastically supports the OVL principle of giving people a running start with their formal verification via the Questa Formal Library (QFL) of optimized checkers we include for free with Questa PropCheck. You can find this library at $(INSTALL)/share/QFL/checkers.  Pro Tip: if you are verifying FIFOs, strongly consider using the QFL FIFO checkers instead of the OVL FIFO ones, as the QFL code has been optimized to be more “formal friendly” than the OVL version which was written to support both simulation and formal.

 

Reference links:

Adopting Assertion-Based Verification with Accellera Standard Open Verification Library; Verification Horizons, Q4 2005; Kenneth Larsen, Dennis Brophy; Mentor, A Siemens Business