How to Reduce the Complexity of Formal Analysis – Part 5 – Memory Abstraction
When big counters and memories are in the active logic cone of an assertion that keeps coming up as “inconclusive”, they are probably the root cause of the problem. Why? Because the math behind the formal algorithms struggles to accommodate very large state spaces; and counters and memories both can introduce a lot of state bits and large sequential depth for formal to try to swallow. Fortunately, there are techniques that can help: we can reduce the size of these elements, or replace them with abstract models. This post will focus on handling memories effectively with formal (counters were addressed in Part 4)
The easiest way is to address a memory-related inconclusive is to black box the memory model or instance. After the black boxing is applied, the element’s outputs become free inputs. Proof results will be valid, but firings need further investigation to determine if they are valid or caused by the black boxing. The commands to black box module/instance are as follows.
Another easy technique to reduce the size of memory for a formal analysis is to change the data width and address depth parameters (if the design uses parameters for them). With carefully selected values, the complexity of the formal analysis can be reduced substantially without affecting the correctness of the result. Even better: to change the parameters, we don’t need to touch the original RTL — we can just use a tool command to electronically overwrite them. Here is an example:
Another approach is to only keep the memory entries that influence the property, and abstract the remaining memory entries as free inputs. In this case, a proof will be valid but a firing/CEX will need further investigation to determine its validity. Here is an example where the property is only checking the memory entry at address 100.
Suppose the memory has 128 entries and the data width is 64 bits. We can abstract the memory entries whose addresses are not 100 using the netlist cutpoint command:
After the memory is abstracted, the number of state bits is reduced from 8192 to 64! This will substantially improve the formal run’s performance.
Another method is to replace the memory with a cache of N entries to remember the last N writes, and abstract the rest as free inputs. Again, proofs will be valid but firings/CEXs maybe false. The following cache example only remembers the 2 most recent writes, and returns free data on a read miss.
Note that if you are dealing with a ROM, you can replace the ROM with a lookup table (case statement) and a register. Here is an example of abstracted ROM with a lookup table. We can see that the look up table is a case statement of address signal “addr”. For a specific address, the corresponding case item is executed and the read data “sram_data” is assigned by the value that should be stored in the specific address. Since the control logic is not changed at all, both proofs and firings will be valid. The case statement is combo logic and doesn’t introduce any states to the state space. The original ROM has a huge number of state bits equal to DEPTH x WIDTH, but the remodeled one only has the number of state bits equal to the WIDTH that reduces a lot of formal complexity.
Now that all your assumptions, assertions, counters, and memories have been refactored, there are two more easy-to-apply, yet very powerful, principals of formal analysis that you can use to expedite the formal analysis even more. In Part 6, we will introduce how to leverage “Data Independence” and “Non-Determinism”.
Until then, may your state spaces be shallow, and your analyses be exhaustive!
Jin Hou and Joe Hupcey III
for the Questa Formal Team
Reference Links:
Part 1: Finding Where Formal Got Stuck and Some Initial Corrective Steps to Take
Part 2: Reducing the Complexity of Your Assumptions
Part 3: Assertion Decomposition
Verification Academy: Handling Inconclusive Assertions in Formal Verification
Comments