Formal Verification through ARV™-Formal

In the dynamic landscape of Very Large Scale Integration (VLSI) design, the ever-growing complexity of Application-Specific Integrated Circuits (ASICs) has posed significant challenges to the traditional netlist simulation process. As ASICs become larger and more intricate, the time-consuming nature of netlist simulations for even minor changes in RTL (Register Transfer Level) has become a bottleneck. This is where formal verification steps in as a game-changer. This article explores the transformative role of formal verification, with a spotlight on ARV-Formal™, a cutting-edge tool developed by Agnisys, Inc.

The unique methods employed for RTL behavior validation through formal verification are considered more essential than other verification techniques due to their effectiveness in handling the increasing complexity of modern ASICs.

ARV-Formal™, developed by Agnisys, Inc., emerges as a powerful tool tailored to verify RTLs without the need for repetitive simulation runs after minor changes. The tool focuses on the “Property Checking” technique, with a particular emphasis on generating assertions automatically corresponding to IP specifications. This approach significantly reduces the time and effort spent on verification, offering a more efficient and reliable alternative to traditional methods.

ARV-Formal™ also provides bounded validation proof in some cases where it may be difficult to prove a property. It also allows users to have automatic parameterized formal checks that focus on specific problems with targeted assertions aiming to reduce debug timings. A formal IP level verification, as a replacement for simulation for a block level IP, aims to prove the correctness of 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 even a 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.

Assertions generated by the tool:

ARV-Formal™ is distinguished by its automatic generation of a comprehensive suite of assertions, ensuring a meticulous verification process for RTL designs. The tool adeptly addresses critical facets, including validation of register accesses for data transfer integrity and correctness. It scrutinizes external RTL interfaces, confirming proper interaction and adherence to communication protocols with external components. Special registers undergo dedicated checks, guaranteeing their functionality aligns with design specifications. Furthermore, ARV-Formal extends its verification scope to Special IDS-associated User-Defined Primitives (UDPs), validating their correct usage and seamless integration.

Incorporating assertions aligned with functional safety standards, ARV-Formal ensures compliance with stringent safety protocols, adding a layer of reliability to the design. The tool doesn’t stop at individual components; it provides holistic system-level assertions, evaluating the overall behavior and functionality of the RTL design. Specific assertions for RTL port connections ensure a rigorous examination of communication correctness, while topology assertions verify the hierarchical organization of design components. This automated assertion generation significantly enhances verification efficiency, making ARV-Formal an invaluable asset in the complex realm of VLSI design verification.

Assertions for SoC Designs:

In IDS-Integrate, users seamlessly input instructions using TCL or Python commands. The tool then generates assertions, emphasizing connectivity aspects like ad-hoc connections, bus aggregations, bridge connections, and more. This tool provides a specialized output support named “arv_formal,” enabling users to intricately formulate assertions associated with the integrated circuit.

As an illustration, contemplate assertions explicitly tailored for the connectivity of bus aggregation logic within an integrated circuit framework. In this case, the initiating bus is an APB situated at the top or wrapper block, directing signals to four distinct child blocks. This methodology guarantees the proper functioning of the bus aggregation logic within the integrated circuit design. Users can customize and expand these assertions based on the unique intricacies of their SoC design.

ARV-Formal in Collaboration with Onespin™ 360 DV

Onespin 360 DV features witness creation that further eases the understanding of issues. On detection of a problem, the formal platform will create a signal time trace that demonstrates a sequence of events that leads to the problem. This ease of use feature makes the formal process easy to understand by leveraging a familiar waveform approach to visualize issues.

ARV-Formal™ generates automatic SystemVerilog Assertions based on the input specification. These assertions are bound by the RTL design generated by IDesignSpec and validated using Onespin™ 360 DV App.

With the collaboration of ARV-Formal™ and Onespin™ 360 DV, the following is possible:

1. Assertion-based verification of block-level register RTL
2. SoC-level module connectivity proofs
3. End-to-end aggregation logic proof

Conclusion:

ARV-Formal™ revolutionizes Automatic Register Verification by automating assertion generation, addressing design complexities, and streamlining the verification process. It outpaces simulations with its faster and comprehensive approach, generating a formal verification environment covering SystemVerilog properties. Collaborating with Onespin™ 360 DV enhances its capabilities, introducing assertion-based validation. ARV-Formal’s efficiency in handling complex designs, providing counter-examples for debugging, and offering an interactive view of assertion results positions it as a vital tool in ensuring reliability and early bug detection in system designs.