8.2. Key Formal Methods Applied to RTL Verification

8.2.1 Equivalence Checking

Equivalence checking is the process of verifying that two representations of a design (typically RTL and gate-level netlist) are functionally equivalent. This is a crucial verification technique, especially after synthesis, where a design’s RTL code is transformed into a gate-level netlist.

• Application: After synthesis, equivalence checking is used to compare the RTL code (e.g., written in Verilog or VHDL) with the gate-level netlist generated by the synthesis tool.

• How it Works:

  • The equivalence checking tool compares the original RTL description and the synthesized gate-level netlist and checks if the logic behavior remains the same after synthesis.
  • The tool ensures that no functional changes have occurred during the synthesis process, such as changes in control logic or incorrect optimizations.

• Tools: Synopsys Formality, Cadence Conformal, and Mentor Graphics Questa Formal are widely used for equivalence checking.

Example:

• After synthesizing an RTL design, equivalence checking tools like Formality can compare the RTL model of a multiplexer (MUX) with the synthesized gate-level model to ensure both behave identically under all conditions.

Equivalence checking is essential in ensuring that the logic output remains consistent during the translation from the RTL code to its gate-level representation. It involves comparing two versions of the design: one written in a high-level description language (e.g., Verilog or VHDL) and another that is a more detailed, implementable gate-level version created by synthesis tools. This ensures that no errors have been introduced during the design transformation process. If the tool identifies that the two models behave the same under all possible inputs and situations, we can conclude that the synthesis process worked correctly.

Think of equivalence checking like translating a book from one language to another. An equivalence checking tool ensures that the translated book conveys the exact same story as the original. If certain sentences change meaning or context due to poor translation, the equivalence checking would highlight these discrepancies.

8.2.2 Property Checking

Property checking involves verifying that certain properties or assertions, which describe the expected behavior of a design, hold true for all possible inputs. These properties are generally specified using temporal logic such as Linear Temporal Logic (LTL) or Computation Tree Logic (CTL).

• Application: Property checking is commonly used for verifying complex designs, ensuring that safety and liveness properties are met in an RTL design. For example, it can be used to check that a counter never overflows or that a signal is always stable within a certain time window.

• How it Works:

  • Designers specify properties such as "always A implies B" or "eventually X will happen."
  • Formal tools exhaustively check if these properties hold for all possible input combinations and timing scenarios.

• Tools: Cadence JasperGold, Mentor Graphics Questa Formal, Synopsys Formality are used for property checking.

Example:

• For a design involving a FIFO (First-In-First-Out) queue, a property might state that "when the FIFO is not empty, the data output should always be valid." Formal tools can verify this property across all possible states of the FIFO design.

Property checking is a technique that helps verify that specific assertions about a design are always true. It employs formal logic to describe these assertions, which are expectations about how the design should behave in certain conditions. For example, you might want to check that a counter always resets after reaching its maximum value or that certain signals have stable values at designated times. The tool methodically verifies these expectations against the design's functionality across all potential scenarios, ensuring that the design adheres to its specifications at all times.

Imagine a traffic light system where property checking would verify that the red light is on whenever the green light is off. This is much like having rules to ensure that traffic operates safely; property checking enforces those rules at all times, preventing collision or confusion at intersections.

8.2.3 Model Checking

Model checking is a formal method used to exhaustively explore the state space of a design and verify that the design satisfies a set of properties. It is particularly useful in detecting bugs or design flaws that may arise due to unexpected interactions between components in a complex system.

• Application: Model checking is used in verifying both safety properties (e.g., ensuring that no invalid states occur) and liveness properties (e.g., ensuring that the system eventually reaches a desired state).

• How it Works:

  • The tool systematically explores all possible states of the design and checks if it satisfies the properties at every step.
  • If a property violation is detected, model checking can pinpoint the exact sequence of events leading to the violation.

• Tools: Cadence JasperGold, Mentor Graphics Questa Formal, and Synopsys Formality support model checking.

Example:

• For a traffic light controller, a model-checking tool could verify that the system will never enter an invalid state, such as both the red and green lights being on simultaneously.

Model checking is a thorough verification technique that involves examining every possible state within a design to ensure it meets specified properties. It does this by simulating the operation of the design step-by-step, testing every scenario against the defined safety and liveness properties to confirm that the design will not produce undesired states. For instance, it can verify that a traffic light controller does not end up with both red and green lights activated at the same time, which would create a dangerous situation.

Consider a school control system that checks if students meet specific criteria for graduation. Model checking is like reviewing each student's complete academic year to ensure they meet all required subjects and grades before they can graduate. Just as the control system aims to avoid mistakenly declaring someone graduated without meeting the requirements, model checking prevents the design from reaching invalid operational states.

8.2.4 Bounded Model Checking (BMC)

Bounded Model Checking (BMC) is a formal verification technique that searches for violations of properties within a bounded time frame. It is particularly useful for detecting corner cases in the design.

• Application: BMC is used to find design bugs within a limited scope of time, often during early stages of design or for designs with known temporal properties. It can be applied to verify properties such as "A should always be true within N cycles."

• How it Works:

  • BMC explores a limited number of clock cycles and checks if the specified properties hold within this time window.
  • If a property violation is found within the bounds, the tool generates a counterexample (sequence of events that led to the violation).

• Tools: Cadence JasperGold and Mentor Graphics Questa Formal provide BMC capabilities.

Example:

• BMC can be used to verify that a finite state machine (FSM) never enters a state where the output is invalid, within a specific number of clock cycles.

Bounded Model Checking (BMC) focuses on verifying design properties within a restricted number of time frames, making it a practical method for identifying issues that might occur quickly during operation or under specific conditions. By limiting the time period under review — such as checking how a design behaves over the next few clock cycles — BMC efficiently searches for corner cases or potential faults. If violations of the properties are found during this review period, a counterexample is produced, which illustrates how the flaw can be triggered.

Think of BMC as a safety check in a fast-food restaurant's kitchen, where only the last few orders are examined to ensure they comply with quality standards. If an order fails to meet the standards within this limited check, the staff can immediately correct it before serving the customer. BMC identifies potential failures in scenarios that operate over narrow time windows, allowing for quick corrections.

--