Ensuring that the design under verification simulates all the possible scenarios is a challenging task. However, achieving this guarantees the completeness and correctness of the design. The state space of a design is the representation of all possible states that a design can go through during execution. Nondeterminism is one of the most important techniques to investigate this state space. To know more about it, check out our latest blog post at:
What is a Nondeterministic Signal?
With formal verification it is possible to exhaustively test the design with all possible inputs, exploring its full state space. However, this process can be computationally intensive and time-consuming. Nondeterministic signals, also known as symbolic signals, are open wires that the formal tool can drive to any value. These signals can be constrained to suit the formal verification engineer’s needs. These signals not only play a major role in discovering edge cases and faulty behavior but also can accelerate the convergence time. The assignment of these signals allows the verification process to go through divergent paths more quickly to explore the state space faster.
How can it be used?
For further illustration, we will use a cache to explain how symbolic variables can be used for verification.
Cache setup:
- The cache has 16 cache-lines and 4 sets. Each set represents 4 cache-lines
- Each cache line stores 32 -bit words
- The cache is indexed with 16-bit address space. It uses the typical tag, index and offset.
Tracking the cache-line:
1) Symbolic signal declaration
Now let’s declare a nondeterministic signal that represents a cache address. This signal is an open wire that can take any value from 0x0000 to 0xFFFF. Let’s assume that the address assigned to the nondeterministic signal is 0xBFCD.
2) Nondeterministic address matching the input address
The verification engine will start injecting inputs randomly. Once the engine chooses an input that matches with the nondeterministic address which is 0xBFCD, the formal verification test bench starts monitoring its behavior to ensure proper handling of hits, misses, and data retrieval.
Dependence of the formal verification testbench on the nondeterministic signal that can take any address value is much more efficient and easier to model, as the tracking is focused on a single signal rather than managing multiple input scenarios. Additionally, this can help to improve the convergence time and resources consumption for the reason of verifying a single address per formal proof instance instead of exhaustively checking all addresses.
3) Tracking the Cache-line:
- State Monitoring: The cache can be valid, invalid or in a dirty state.
- Read/Write accessing: During the process of accessing that certain cache-line. The formal verification test bench tracks the cache response. Whether it’s cache-hit or cache-miss.
- Eviction and replacement: If the cache-line gets evicted or replaced due to new data being loaded into the set, the tracking will capture this event, ensuring that the eviction follows the cache replacement policy.
Why should you use nondeterministic signals?
Simplifying the formal verification model:
One of the main advantages of using nondeterministic signals is that the complexity of your code significantly decreases. Instead of managing each specific input produced by the formal tool, you only need to focus on handling the nondeterministic signal that matches input.
Reducing convergence time and resource consumption:
In formal verification, the formal tool exhaustively investigates all the variations of inputs to test the design. Using the approach of nondeterministic that matches the input can drastically reduce the convergence time and the resource consumption because each proof instance relies only on one input.
Early Bug Detection:
Symbolic variables allow the reveal of unexpected interactions and corner cases in an early stage of the verification process by simulating a wider range of inputs and different scenarios.
Consistency in Testing:
A stable nondeterministic signal maintains a consistent value throughout a property. This feature allows for reliable verification since the signal is easy to track and can be validated against the design’s output behavior.
Conclusion
In conclusion, Nondeterminism is a crucial method in formal verification. Allowing powerful and scalable approaches to model and verify complex design. Investigating all possible scenarios, ensuring completeness, early detection of bugs and efficient resource utilization.
At LUBIS EDA, this method is employed regularly to ensure that there is not one single scenario that could be missed. This approach gives us an edge over conventional simulation verification to catch bugs early in the verification process, including unintended behavior and corner case bugs.