{"id":13058,"date":"2018-03-26T10:13:07","date_gmt":"2018-03-26T17:13:07","guid":{"rendered":"https:\/\/blogs.mentor.com\/verificationhorizons\/?p=13058"},"modified":"2026-03-27T08:38:40","modified_gmt":"2026-03-27T12:38:40","slug":"ovl-the-free-open-assertion-library-you-can-use-to-jump-start-your-formal-testbench","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2018\/03\/26\/ovl-the-free-open-assertion-library-you-can-use-to-jump-start-your-formal-testbench\/","title":{"rendered":"OVL: The Free, Open Assertion Library You Can Use To Jump Start Your Formal Testbench"},"content":{"rendered":"<p><a href=\"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2018\/03\/Accellera-Standard-OVL.gif\"><img loading=\"lazy\" decoding=\"async\" class=\"alignright wp-image-13057\" src=\"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2018\/03\/Accellera-Standard-OVL-520x301.gif\" alt=\"Accellera Standard OVL\" width=\"264\" height=\"159\" \/><\/a>You\u2019ve watched <a href=\"https:\/\/verificationacademy.com\/courses\/Formal-Assertion-Based-Verification\" target=\"_blank\" rel=\"noopener\">all the Verification Academy videos on getting started with formal verification<\/a>, and even tried some of the examples included in the product documentation, but you are still struggling to build-up an effective \u201cformal testbench\u201d 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 \u2013 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:<\/p>\n<p>First, the library is publicly available for download here:<\/p>\n<p><a href=\"http:\/\/www.accellera.org\/downloads\/standards\/ovl\" target=\"_blank\" rel=\"noopener\">http:\/\/www.accellera.org\/downloads\/standards\/ovl<\/a><\/p>\n<p>But chances are you already have it on your system \u2013 Mentor includes a copy of the library with the <a href=\"https:\/\/www.mentor.com\/products\/fv\/questa-property-checking\" target=\"_blank\" rel=\"noopener\">Questa PropCheck<\/a> installation, so to confirm your IT\/CAD\/SysAdmin installed it go to <strong>$(INSTALL)\/share\/assertion_lib\/OVL\/std_ovl<\/strong> to confirm it\u2019s there.<\/p>\n<p>where the value of the INSTALL environment variable can be found via the Linux command line:<\/p>\n<p><strong>% qverify -install_path<\/strong><\/p>\n<p>&nbsp;<\/p>\n<p>But before digging into the code and how you can use it, some background: from the OVL project website, \u201c<em>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.<\/em>\u201d Version 1.0 was published back in 2005, and it\u2019s been continuously improved since \u2013 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).<\/p>\n<p><strong><u>Getting Started <\/u><\/strong><\/p>\n<p>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.<\/p>\n<ul>\n<li>Add a checker &#8220;where&#8221; you want to verify. For example, where you expect a signal will be available for at least N-clock cycles, instantiate the \u2018ovl_hold_value\u2019 checker. To make sure that when one event happens then another will happen, use the \u2018ovl_implication\u2019 checkers.<\/li>\n<li>Add checkers to finite state machines (FSM) to check for illegal transitions (\u2018ovl_no_transition\u2019), illegal states, and that you do not stay in a state longer than expected (\u2018ovl_change\u2019). Use the coverage information obtained by the checker to ensure that all states of the FSM have been covered during simulation.<\/li>\n<li>Add the \u2018ovl_range\u2019 checker to check for legal ranges of addresses to memory structures and similar checks. You can use \u2018ovl_underflow\u2019 and \u2018ovl_overflow\u2019 for counters that are not allowed to wrap around.<\/li>\n<li>For memory structures, FIFOs are always a good target for adding checkers, because many bugs tend to creep in to them. For example, \u2018ovl_fifo_index\u2019 can be used to ensure that a FIFO pointer should never underflow or overflow.<\/li>\n<li>Add checkers like \u2018ovl_handshake\u2019 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 \u2018I am done\u2019 signal must assert within a given set of cycles after the leader signal was raised.<\/li>\n<\/ul>\n<p><strong><u>Now let\u2019s dive into an example \u2026<\/u><\/strong><\/p>\n<p>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 \u201cfires\u201d, a severity level associated with the firing, and coverage element. Consider the following OVL \u201cassert_never\u201d property:<\/p>\n<p><strong>ovl_never #(<br \/>\n\/* severity_level *\/\u00a0 \u00a0 \u00a0`OVL_ERROR,<br \/>\n\/* property_type *\/ \u00a0\u00a0 `OVL_ASSERT,<br \/>\n\/* msg *\/\u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u201cRegister A &lt; Register B\u201d,<br \/>\n\/* coverage_level *\/ \u00a0 `OVL_COVER_ALL) valid_checker_inst(<br \/>\n\/* clock *\/\u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0clk,<br \/>\n\/* reset *\/\u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0reset_n,<br \/>\n\/* test_expr *\/\u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 \u00a0 regA &lt; regB );<\/strong><\/p>\n<p>This assertion checks that the \u2018test_expr\u2019 test expression does not evaluate to TRUE at each rising edge of a clock \u2018clk\u2019. In cases where the test expression contains unknowns, the checker can flag this situation as well.<\/p>\n<p>The parameters in this simple \u2018assert_never\u2019 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 \u2018severity_level\u2019, you can report the importance of the check. You could even stop the run, if desired, by setting the \u2018severity_level\u2019 to `OVL_FATAL.<\/p>\n<p>The \u2018property_type\u2019 determines whether to use the assertion checker as an assert property or an assume property. Setting the \u2018property_ type\u2019 to OVL_ASSUME tells the verification engines that the OVL checker is a constraint that should not be checked but assumed to be true.<\/p>\n<p>By default OVL checker firings are reported as a \u201cVIOLATION\u201d, but by using the \u2018msg\u2019 parameter you can specify that a more meaningful message is reported.\u00a0 Regardless, if Questa PropCheck\u2019s formal algorithms find a way that this property can be violated, PropCheck will show you a \u201ccounter example\u201d waveform (nick-named a \u201cCEX\u201d) that shows exactly how your DUT can do something other than what\u2019s specified by the property. Generally, this waveform is pointing you right to a bug \u2013 a true time saver vs. debugging a failed simulation test!<\/p>\n<p>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 \u2018coverage_level\u2019 parameter. This is a little more obvious in the following example of the \u201covl_one_hot\u201d OVL checker:<\/p>\n<p><strong># OVL_COVER_POINT : ASSERT_ONE_HOT :<\/strong><\/p>\n<p><strong>test_expr_change covered : time 1300 : DUT.<\/strong><\/p>\n<p><strong>check_fsm_is_onehot.ovl_cover_t<\/strong><\/p>\n<p>This cover point reports if the \u2018test_expression\u2019 actually changed, providing insight into how well the test environment exercises the circuit and whether any coverage holes exist.<\/p>\n<p>&nbsp;<\/p>\n<p><strong><u>Usage Logistics<\/u><\/strong><\/p>\n<p>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:<\/p>\n<p><strong>c_ovl compile_ovl:<\/strong><\/p>\n<p><strong>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 $(VLOG) -sv -mfcu -cuname ovl_bind \\<\/strong><\/p>\n<p><strong>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 properties\/ovl\/ovl_apb_access_arb.sv \\<\/strong><\/p>\n<p><strong>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 properties\/ovl\/ovl_dp_fifo.sv \\<\/strong><\/p>\n<p><strong>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 -y $(INSTALL)\/share\/assertion_lib\/OVL\/std_ovl +libext+.v \\<\/strong><\/p>\n<p><strong>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 +incdir+$(INSTALL)\/share\/assertion_lib\/OVL\/std_ovl \\<\/strong><\/p>\n<p><strong>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 +define+OVL_SVA+OVL_ASSERT_ON+OVL_COVER_ON+OVL_XCHECK_OFF<\/strong><\/p>\n<p>&nbsp;<\/p>\n<p>Then, run Questa PropCheck from the Linux command line:<\/p>\n<p><strong>% rm -rf log<\/strong><\/p>\n<p><strong>% qverify -c -od log -do qft_files\/run_pc.do<\/strong><\/p>\n<p>&nbsp;<\/p>\n<p>Note that it\u2019s ok if you don\u2019t have the permissions to modify the files in the OVL directory &#8212; you will just be using the library elements as-is. This is perfectly fine; and quite popular.<\/p>\n<p>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&amp;paste the necessary OVL assertions into a separate library of your own creation before tailoring them.<\/p>\n<p>&nbsp;<\/p>\n<p><strong><u>Summary<\/u><\/strong><\/p>\n<p>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:<\/p>\n<p><a href=\"https:\/\/verificationacademy.com\/sessions\/introduction-open-verification-library\" target=\"_blank\" rel=\"noopener\">https:\/\/verificationacademy.com\/sessions\/introduction-open-verification-library<\/a><\/p>\n<p>In general, reusing the OVL library code is a great way to combat \u201cblank sheet of paper paralysis\u201d and jump start your formal testbench because it\u2019s 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&amp;paste the necessary OVL assertions into a separate library of your own creation before tailoring them.)<\/p>\n<p>It\u2019s already there for you to try \u2013 just navigate to: <strong>$(INSTALL)\/share\/assertion_lib\/OVL\/std_ovl<\/strong><\/p>\n<p>What are you waiting for?<\/p>\n<p>Joe Hupcey III and Jin Hou,<br \/>\nfor the Questa Formal Team<\/p>\n<p>&nbsp;<\/p>\n<p>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 <strong>$(INSTALL)\/share\/QFL\/checkers<\/strong>.\u00a0 <u>Pro Tip:<\/u> 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 \u201cformal friendly\u201d than the OVL version which was written to support both simulation and formal.<\/p>\n<p>&nbsp;<\/p>\n<p><strong>Reference links:<\/strong><\/p>\n<p><em>Adopting Assertion-Based Verification with Accellera Standard Open Verification Library<\/em>; Verification Horizons, Q4 2005; Kenneth Larsen, Dennis Brophy; Mentor, A Siemens Business<\/p>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>You\u2019ve watched all the Verification Academy videos on getting started with formal verification, and even tried some of the examples&#8230;<\/p>\n","protected":false},"author":71594,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"spanish_translation":"","french_translation":"","german_translation":"","italian_translation":"","polish_translation":"","japanese_translation":"","chinese_translation":"","footnotes":""},"categories":[1],"tags":[324,492,493,622,656,665],"industry":[],"product":[],"coauthors":[],"class_list":["post-13058","post","type-post","status-publish","format-standard","hentry","category-news","tag-accelera","tag-formal-property-checking","tag-formal-verification","tag-ovl","tag-qfl","tag-questa-propcheck"],"_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/13058","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/users\/71594"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/comments?post=13058"}],"version-history":[{"count":1,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/13058\/revisions"}],"predecessor-version":[{"id":19855,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/13058\/revisions\/19855"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=13058"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=13058"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=13058"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=13058"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=13058"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=13058"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}