{"id":13236,"date":"2018-09-28T10:01:49","date_gmt":"2018-09-28T17:01:49","guid":{"rendered":"https:\/\/blogs.mentor.com\/verificationhorizons\/?p=13236"},"modified":"2026-03-27T08:48:28","modified_gmt":"2026-03-27T12:48:28","slug":"how-to-reduce-the-complexity-of-formal-analysis-part-4-counter-abstraction","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2018\/09\/28\/how-to-reduce-the-complexity-of-formal-analysis-part-4-counter-abstraction\/","title":{"rendered":"How to Reduce the Complexity of Formal Analysis – Part 4 \u2013 Counter Abstraction"},"content":{"rendered":"

When big counters and memories are in the active logic cone of an assertion that keeps coming up as \u201cinconclusive\u201d, they are probably the root cause for inconclusive result. Why? Because the math behind formal algorithms struggles to accommodate very large state spaces; and counters and memories both can introduce a lot of state bits and sequential depth for formal to try to swallow. Fortunately, there are techniques that can help: we can either reduce the size of these elements, or replace them with abstract models. This post will focus on handling counters effectively with formal (dealing with memories will be addressed in Part 5)<\/p>\n

For starters, when helping formal digest a counter, set the counter to an \u2018X\u2019 value for its initial state instead of \u20180\u2019, and let formal consider all potential values for initial state. This gives the formal algorithms the freedom of action they prefer when they form and solve their equations under-the-hood. Here is an example of how to set a counter\u2019s initial value to \u2018X\u2019 in Questa PropCheck<\/a>:<\/p>\n

\"\"<\/a><\/p>\n

Note that this tool command will electronically overwrite the RTL reset value without changing your RTL code.<\/p>\n

The best part of this technique from an end-user perspective is that when the given property is proven, the proof is valid for the original counter value, and for all time. Conversely, if a counter example (CEX) is found for the property, the CEX would probably be much shorter and easier to interpret than if you used the original counter initialization value. The caveat is that while the \u201cfiring\u201d may be not be a design bug, per se \u2013 the design might require the counter to always start from \u20180\u2019. Again, if this the case, this \u2018X\u2019 method is not useful and other techniques need to be tried.<\/p>\n

Another popular and effective way to handle big counters is to replace them with a small state machine model that only considers the critical values of the counter that would trigger interesting design actions. For example, suppose value \u2018m\u2019, \u2018n-1\u2019 and \u2018n\u2019 of the counter are critical. Consider the following state machine as a replacement:<\/p>\n

\"\"<\/a>
Figure 1: Abstracting a large counter (that\u2019s very hard for formal to digest because of its big state space) with a small state machine (that\u2019s much easier for formal to handle because the state space is much smaller)<\/strong><\/figcaption><\/figure>\n

To replace the original counter with this abstract model, we first temporarily bypass\/disable the real design\u2019s driving logic \u2013 without altering the source RTL in any way \u2013 by electronically \u201ccutting\u201d the original counter signal with the tool command \u201cnetlist cutpoint\u201d to make it a free variable and then add constraints to it. Since this abstracted counter has only 4 states — much less than the original — the formal engines will be able to reach interesting design states much faster!<\/p>\n

Here is an example.<\/p>\n

\"\"<\/a><\/p>\n

The Makefile to run the test is as follows. The \u201cabs_cnt.do\u201d contains the TCL commands to define the abstract counter for \u201ccnt\u201d in the design. The assertion \u201cassert_action3\u201d should be fired due to the error in RTL that drives \u201caction\u201d to be 2\u2019d2 when \u201ccnt==8\u2019hf1\u201d.<\/p>\n

\"\"<\/a><\/p>\n

The \u201cabs_cnt.do\u201d file is as follows.<\/p>\n

\"\"<\/a><\/p>\n

The error trace from using abstract counter is as follows. The firing happened at cycle 4 that is short and easy for debugging the problem.<\/p>\n

\"\"<\/a><\/p>\n

If we remove \u201cdo abs_cnt.do\u201d from \u201cMakefile\u201d and rerun the test by using original \u201ccnt\u201d defined in the RTL, we will get error trace similar to the following one. We can see the firing happened at cycle 242 that is much longer than the one using abstract version of \u201ccnt\u201d. In real big designs, it may be impossible to formal to converge for big counters without abstraction.<\/p>\n

\"\"<\/a><\/p>\n

Note that this strategy should mainly be used for bug-hunting \u2013 a full proof from this approach is not going to be valid if the rest of design relies on a particular number of cycles in between counter values. Again, as noted above, any CEX\u2019s must be carefully reviewed to confirm the firing is being caused by design bug and not an overly-abstracted counter model.<\/p>\n

Now that all your counters have been tamed, the next beasts to deal with are all the memories.  We will show you how in Part 5 \u2026<\/p>\n

Until then, may your state spaces be shallow, and your analyses be exhaustive!<\/p>\n

Jin Hou and Joe Hupcey III
\nfor The Questa Formal Team<\/p>\n

Reference Links:<\/p>\n

Part 1: Finding Where Formal Got Stuck and Some Initial Corrective Steps to Take<\/a><\/p>\n

Part 2: Reducing the Complexity of Your Assumptions<\/a><\/p>\n

Part 3: Assertion Decomposition<\/a><\/p>\n

Verification Academy: Handling Inconclusive Assertions in Formal Verification<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

When big counters and memories are in the active logic cone of an assertion that keeps coming up as \u201cinconclusive\u201d,…<\/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":[1000,1,10],"tags":[400,487,493,665,733,734],"industry":[],"product":[],"coauthors":[931],"class_list":["post-13236","post","type-post","status-publish","format-standard","hentry","category-formal-analysis","category-news","category-tips-tricks","tag-counter-abstraction","tag-formal-analysis","tag-formal-verification","tag-questa-propcheck","tag-state-machine","tag-state-space"],"_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/13236","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=13236"}],"version-history":[{"count":3,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/13236\/revisions"}],"predecessor-version":[{"id":16931,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/13236\/revisions\/16931"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=13236"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=13236"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=13236"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=13236"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=13236"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=13236"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}