0-In Formal Verification

Despite tremendous advances in constraint-random stimulus generation and coverage-based verification, simulation-based verification cannot effectively find all the potential issues within today’s complex chips. This is the main reason that designers complement their simulation-based verification methodology with formal verification.

Formal verification has a different approach than simulation to verify the behavior of designs. Using assertions (see the Assertion-based Verification methodology section) formal verification does not rely on stimulus, so it does not require a testbench, and uses advanced mathematical analysis techniques to prove that these assertions about the behavior of the design are true or not. In many cases, formal verification can formally prove assertions to be true, thus verifying that the design is behaving correctly.

The 0-In® Formal verification solution offers the highest capacity and performance available to help you find your most complex bugs. With an extensive assertion library of monitors and assertions and close integration with your simulation environment, 0-In Formal represents the leading edge in formal verification, allowing you to not only improve overall verification quality but also find the most critical bugs in your design.

Since no testbench is needed, 0-In Formal can be used as soon as RTL code is available. Typically assertions are added from a rich library of assertions or are written by the engineer in either SystemVerilog or PSL. These assertions capture design properties as well as constraints on the interfaces of the RTL block. Through a rich debug environment designers can either prove design properties or find root causes for functional issues that are discovered by 0-In Formal.

Formal verification is complementary to simulation, and, in the Mentor solution, both the results of formal verification and simulation are recorded in the Unified Coverage Database (UCDB), which offers a rich set of verification management capabilities.