ARV™ FORMAL Verification

Formal verification is a crucial aspect of ensuring the reliability and safety of systems. ARV stands for Automatic Register Verification. As the name indicates it verifies the register specifications automatically by generating assertions. While traditional verification engineers manually write assertions, the ARV™-FORMAL tool automates this process for all required specifications. 

Popular specification standards such as IP-XACT, SystemRDL, and CSV have grown to such an extent to automatically generate any number of register models, RTL designs, firmware, and verification code. The whole verification process can be further upgraded by automating code for formally verifying IPs with a slave interface since it helps in reducing simulation effort and the overhead involved in creating and maintaining block/chip level testbenches. Even by using both directed and constrained random test cases we may miss out on corner cases, which can only be verified formally.

Verification Challenges

Complexity:

• Design complexity increases corresponding to the addition of functionality in the specification
• Verification complexity is a function of design complexity

Time Consumption:

• Verification time is the function of an increase in the number of logic gates
• Verification consumes 70% of the design development cycle and resources

Verification Bottleneck:

• The verification bottleneck happens due to an increase in the design abstraction level
• The verification bottleneck doubles due to the functional complexity and its verification scope and efforts

Major Challenges:

• Dealing with state space size at a large scale
• Dealing with the design’s expected behavior and specification
• Fundamental cause of logic bugs:
  • Lack of reference model
  • Lack of comprehensive functional coverage metric

Some Key Verification Trends:

• Greater complexity of designs
  • Need for systematic verification planning and execution
• Resource crunch
  • Time to market pressures
  • Shortage of verification Engineers
• Requirement for advanced verification techniques
  • SystemVerilog/UVM
  • Assertion based verification

Incorporating formal verification

Formal techniques prove all the possible inputs and ensure a lack of faults in the system. This is a faster and more comprehensive approach than simulation to test the design functionality, with availability of abstract structures for complex and abstract designs. Formal techniques work effectively on data paths.

ARV-Formal™ is a tool developed for verifying RTL designs using formal techniques without running simulations. It can quickly validate the behavior of the design by generating automatic assertions corresponding to the register specification of an IP.

Automatic Generation of:

ARVFormal generates the complete formal verification environment according to the input specification. The following are generated in the output:

• SystemVerilog properties and assertions to check the register access policies, special registers i.e. lock, write pulse, counters and CDC domains.
• Top-level file to bind the design RTL as well as third-party design IP with the assertions
• Makefile or Tcl command scripts
• A verification plan with the ability to back-annotate these formal results so that engineers can analyze the results

Automatically generate from the Specification

1. Register Specification
   1. Special Registers
   2. Properties
2. Connectivity Specification
   1. Bus Connection

What type of assertions are generated

ARV-Formal automatically generates assertions for diverse aspects of RTL designs, including register accesses, external RTL interfaces, and special registers. It ensures compliance with functional safety standards and provides system-level assertions for comprehensive verification. The tool validates RTL port connections, topology, and multi-master designs, offering a streamlined approach to formal verification. Its automated generation of a wide range of assertions enhances the efficiency and effectiveness of the verification process.

Listed below are different types of assertions are generated which includes

• Register accesses
• External RTL interface
• Special registers
• Special IDS-associated UDPs
• Functional safety RTL design
• System level assertions
  • Assertions to check RTL port connections
  • Topology assertions
  • Multi-master design assertions

Assertions for SoC Designs:

In IDS-Integrate, users are allowed to provide input through TCL or Python commands to seamlessly give instructions, on which the tool generates assertions with a focus on connectivity aspects, including ad-hoc connections, bus aggregations, bridge connections, and beyond. The tool facilitates a designated output support named “arv_formal” empowering users to generate assertions intricately tied to the integrated circuit.

For instance, here is an example of assertions crafted for bus aggregation logic connectivity within the context of an integrated circuit. In this scenario, the driving bus is an APB situated at the top or wrapper block, transmitting signals to four distinct child blocks. This approach ensures that the bus aggregation logic functions as intended within the integrated circuit design. Users can adapt and extend these assertions based on the intricacies of their specific SoC design.

Benefits of Adopting ARV Formal

• A faster and comprehensive approach to test the design functionality as it does not require any testbench
• Allowing the bounded proof mechanism to quantify the quantity of formal analysis performed removes redundant efforts
• Allowing abstract structures to run formal analysis more efficiently on complex and abstract designs
• Formal covers all possible scenarios, which simulation practically cannot
• Interactive viewing of assertion pass/fail results
• Debugging with a counter-example

ARV-Formal is developed to provide the types of assertions that are now widely used as complementary to simulation.

ARV-Formal in Collaboration with Jasper™ FPV

The Cadence Jasper Formal Verification Platform consists of formal verification apps at the C/C++ and RTL level. They use smart proof technology and machine learning to find and fix bugs and improve verification productivity early in the design cycle.

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

With the collaboration of ARV-Formal™ and Jasper™ FPV, 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

Summary

ARV-Formal, an Automatic Register Verification tool, streamlines the verification of register specifications by automating assertion generation. It effectively addresses challenges like design and verification complexity, time consumption, and bottlenecks. ARV-Formal aligns with key verification trends, offering a faster, more comprehensive approach than simulations. It automatically generates a formal verification environment, covering SystemVerilog properties, assertions, and makefiles. The tool caters to various assertion types, ensuring comprehensive coverage for different RTL behaviours and system-level specifications. Collaborating with Jasper™ FPV enhances verification with assertion-based validation and module connectivity proofs. ARV-Formal stands out for its efficiency in handling complex designs, providing a counter-example for debugging, and offering an interactive view of assertion results. This tool plays a crucial role in ensuring the reliability, safety, and early bug detection in system designs, making it a valuable asset in the domain of formal verification.