Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Delving into the Core Concepts for formal verification

1719212849334.png
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.

1719212849334.png
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.

1719212877840.png
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.

1719212909809.png
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.
About author
Peng Yu
With a wealth of experience in formal verification projects, I specialize in two critical solutions: formal signoff with full proof and formal signoff with coverage. Throughout my career, I have successfully tackled a diverse range of designs, including Instruction units, Standard interfaces, User-defined interfaces, Bus matrices, Caches, MMUs, Schedulers, DMA controllers, Memory controllers, Interrupt controllers, Power management units, and various specific functional modules.

Drawing on this extensive project experience and a deep understanding of various design types, I have developed a unique formal verification methodology. This methodology has been honed through practical application and has proven highly effective in ensuring design correctness and efficiency.

One of my key achievements has been the independent creation of a comprehensive formal verification IP library. This library comprises nearly 200 units, encompassing basic, common, VIP, and flow libraries. These resources, combined with my methodology, have been successfully deployed in the product development workflows of numerous leading chip companies. The results speak for themselves, with significant improvements in verification effectiveness and performance observed across the board.

My goal is to share this expertise with students at EDA Academy, providing them with practical insights and industry best practices that they can apply directly to their own projects. By imparting this knowledge, I aim to empower learners to achieve their verification goals with confidence and efficiency.

EDA Academy:https://www.eda-academy.com
Explore our current Formal Verification courses:
  1. Introduction to Formal Verification
  2. Formal Verification: SVA Coding
  3. Formal Verification: PSL Coding

Comments

There are no comments to display.

Part and Inventory Search

Blog entry information

Author
Peng Yu
Read time
3 min read
Views
305
Last update

More entries in Uncategorized

More entries from Peng Yu

Share this entry

Back
Top