Formal Verification through ARV-Formal™

Introduction

As the ASICs are getting larger and more complex, the netlist simulation is becoming a veritably time-consuming process, and it isn’t worth running weeks of netlist simulations corresponding to a veritably small change in RTL just to make sure that the netlist is good. Formal verification provides a solution to overcome this issue. Formal verification is a fashion used in different stages in the ASIC design life cycle in frontal-end verification, Logic Synthesis, Post Routing Checks, and for ECOs. The formal verification ways used for RTLs behavior validation are unique and more important than other verification techniques.

ARV-Formal™ is a tool developed by Agnisys Inc. for verifying RTLs without running simulation again and again after any minor changes in the RTL. There are different formal techniques such as “Formal Equivalence Checking” and “Formal Property Checking”. ARV-Formal focuses on the “Property Checking” technique as highlighted in below diagram:

ARV-Formal™ has the capability to quickly validate the behavior of the design by generating assertions automatically corresponding to the specification of IP and provides bounded validation proof too, in some cases where it may be difficult to prove property. It also allows users to have automatic parameterized formal checks that focus on specific problems with targeted assertions, aiming to reduce debugging time. A formal block-level verification as a replacement for simulation of a block-level IP aims to prove the correctness of the system architecture for specific requirements such as cache coherence or avoiding deadlock conditions. ARV-Formal hides much of the technological complexity of validation that underpins formal verification, so the user does not need to be even semi-expert in the validation technique itself.

With the ability to parse register specifications from different supported input formats like IP-XACT, System RDL, RALF, Custom CSV, IDS Word, and IDS Excel, and facilitate a methodology where multiple teams can align and work from a golden specification for auto-generating:

·       System Verilog properties and assertions to check the register access policies.

·       Top-level file to bind DUT.

·       Verification plan to verify formal results.

·       Executable scripts.

ARV-Formal™ is developed to provide the types of assertions that are now widely used accompaniments to simulation. Designers bind assertions into their code to represent how a block is used and find violations of particular conditions. For example, an assertion may check that an acknowledgment signal follows a request after no more than ten clock cycles. Although the assertions create a learning environment, they are still easier to capture and use than bared mathematical expressions.

Focused Formal Verification

Below are examples where formal verification techniques work for a better verification process in the Verification domain.

Clock domain crossing (CDC) is one of the applications of formal techniques that has been with us for a long time, but the proliferation of clocks in today’s SoCs has seen it rise from a low to a high-priority issue. RTL designs having a few clocks might have been addressed in simulation while those that now have hundreds of clocks are best verified in this respect beforehand. Formal model checking is run to verify the auto-generated synchronizer protocol assertions by ARV-Formal™, using the generated formal verification setup and script. The CDC protocol generation utility generates the formal compile and runs scripts. Automated formal setup significantly reduces the effort required to set up the design for formal analysis and avoids the debug effort to resolve incomplete or incorrect setup issues.

X-propagation is another application of formal verification techniques and suitable data that presents design issues for simulation. More complex RTL designs have a tendency to throw out more unknown states, this leads to miss bugs being identified. Linting tools to detect some of these issues. Agnisys Inc. is working on a combination of formal techniques that can be used to exhaustively prove whether Xs in the design are unreachable or will not have an impact on the correct operation of the logic. Techniques vary in so many flavors but in the unique and main, they get separated into automatic property checking methods to prove and validate the absence of X in the RTL design, or there is no registering with the X in it.

Summary

ARV-Formal™ is a complete solution that takes the register specification and RTL design as input and performs formal proof to ensure all register operations conform to the specification. ARV-Formal is powered by an embedded version of (Jasper™ FPV App by Cadence Design System) to provide a one-button seamless process flow leveraging the power of modern formal verification tools. ARV-Formal automatically generates assertions directly from the specification therefore completely automating the setup and ensuring a very rapid return on investment.