In the realm of integrated circuit (IC) design, formal verification stands as a cornerstone for ensuring design correctness. This blog delves into advanced formal verification techniques, shedding light on gate modeling, state transitions, and the pivotal role of properties.
Formal Verification Environment
Formal verification involves translating RTL into a netlist representing an electric circuit composed of digital gates like AND, OR, flip-flops, and latches. These gates are modeled to match their real-world counterparts' behavior but are optimized for formal verification.
Figure 1. Formal Verification Environment
Gate Modeling and Propagation Delay
In formal verification, gates are simplified models:
Real Gate: Includes propagation delay and voltage/impedance ranges.
Formal Model: Ignores propagation delay and operates on a simplified truth table.
Propagation delay is disregarded in formal models, meaning input changes result in immediate output changes. This simplification makes it easier to analyze the netlist over time, focusing on how inputs change over cycles rather than precise timing.
Cycle-Based Timing
Formal verification measures time in cycles rather than conventional units like microseconds or nanoseconds. Inputs change at the beginning of cycles, ensuring the netlist's stability during each cycle. This approach simplifies the timing analysis by treating the clock signal as a square wave with periods measured in cycles.
Properties: Asserts, Covers, and Assumptions
Properties are central to formal verification. They monitor signals in the netlist and determine if specific behaviors occur.
Asserts: Ensure behaviors that should never occur.
Covers: Confirm behaviors that must occur.
Assumes: Define invalid behaviors, guiding the formal tools' analysis.
Figure 2. properties: asserts, covers, and assumptions
Asserts and Covers in Depth
Asserts are crucial for identifying bugs. If an assertion evaluates to false, a counter-example is generated, highlighting the violation. Conversely, if an assertion holds true across all scenarios, it is proven.
Covers ensure that desirable behaviors can occur. Formal tools attempt to find scenarios where the cover property is true. If none exist, the cover is deemed unreachable, indicating a potential design flaw.
States and Free Nets
The state of a netlist is determined by signal values at a specific cycle. If signals are binary, the total number of states is 2N, (N is number of signals). However, logic constraints reduce the number of reachable states.
Free Nets are signals without driving logic. They can independently be 0 or 1. Introducing logic constraints, such as AND gates, reduces the number of reachable states by eliminating invalid combinations.
Adding Logic and Assumptions
Adding logic constraints simplifies the state space by removing unreachable states. Similarly, assumptions guide formal tools by eliminating invalid states, making the verification process more efficient.
Abstractions and Simplifications
Abstractions are modifications that simplify the design for formal verification. For instance, abstracting counters, which typically create large state spaces, can streamline analysis by replacing them with simpler models. While abstractions expedite verification, they might produce invalid counter-examples due to added behavior.
Figure 3. Abstractions and Simplifications
State Transitions and Initial States
State transitions occur at each cycle, dictated by the netlist's current state and input changes. Initial states, often set by reset conditions, further constrain the state space by defining starting values for registers. This ensures certain states are unreachable from the initial configuration.
Conclusion
Formal verification is an indispensable tool in IC design, ensuring that digital circuits operate correctly under all possible scenarios. By leveraging techniques like gate modeling, cycle-based timing, properties, and abstractions, engineers can comprehensively verify their designs, catching bugs early and ensuring robust functionality.
Formal Verification Environment
Formal verification involves translating RTL into a netlist representing an electric circuit composed of digital gates like AND, OR, flip-flops, and latches. These gates are modeled to match their real-world counterparts' behavior but are optimized for formal verification.
Figure 1. Formal Verification Environment
Gate Modeling and Propagation Delay
In formal verification, gates are simplified models:
Real Gate: Includes propagation delay and voltage/impedance ranges.
Formal Model: Ignores propagation delay and operates on a simplified truth table.
Propagation delay is disregarded in formal models, meaning input changes result in immediate output changes. This simplification makes it easier to analyze the netlist over time, focusing on how inputs change over cycles rather than precise timing.
Cycle-Based Timing
Formal verification measures time in cycles rather than conventional units like microseconds or nanoseconds. Inputs change at the beginning of cycles, ensuring the netlist's stability during each cycle. This approach simplifies the timing analysis by treating the clock signal as a square wave with periods measured in cycles.
Properties: Asserts, Covers, and Assumptions
Properties are central to formal verification. They monitor signals in the netlist and determine if specific behaviors occur.
Asserts: Ensure behaviors that should never occur.
Covers: Confirm behaviors that must occur.
Assumes: Define invalid behaviors, guiding the formal tools' analysis.
Figure 2. properties: asserts, covers, and assumptions
Asserts and Covers in Depth
Asserts are crucial for identifying bugs. If an assertion evaluates to false, a counter-example is generated, highlighting the violation. Conversely, if an assertion holds true across all scenarios, it is proven.
Covers ensure that desirable behaviors can occur. Formal tools attempt to find scenarios where the cover property is true. If none exist, the cover is deemed unreachable, indicating a potential design flaw.
States and Free Nets
The state of a netlist is determined by signal values at a specific cycle. If signals are binary, the total number of states is 2N, (N is number of signals). However, logic constraints reduce the number of reachable states.
Free Nets are signals without driving logic. They can independently be 0 or 1. Introducing logic constraints, such as AND gates, reduces the number of reachable states by eliminating invalid combinations.
Adding Logic and Assumptions
Adding logic constraints simplifies the state space by removing unreachable states. Similarly, assumptions guide formal tools by eliminating invalid states, making the verification process more efficient.
Abstractions and Simplifications
Abstractions are modifications that simplify the design for formal verification. For instance, abstracting counters, which typically create large state spaces, can streamline analysis by replacing them with simpler models. While abstractions expedite verification, they might produce invalid counter-examples due to added behavior.
Figure 3. Abstractions and Simplifications
State Transitions and Initial States
State transitions occur at each cycle, dictated by the netlist's current state and input changes. Initial states, often set by reset conditions, further constrain the state space by defining starting values for registers. This ensures certain states are unreachable from the initial configuration.
Conclusion
Formal verification is an indispensable tool in IC design, ensuring that digital circuits operate correctly under all possible scenarios. By leveraging techniques like gate modeling, cycle-based timing, properties, and abstractions, engineers can comprehensively verify their designs, catching bugs early and ensuring robust functionality.
