Enhancing Assertion-Based Verification with Agnisys EDA Tools

Introduction

Assertion-based verification (ABV) is a powerful methodology used in modern hardware design verification. By embedding assertions within the design, ABV enables early detection of bugs and ensures design correctness throughout the development process. This article explores the methods and tools used in assertion-based verification, providing insights into its importance, implementation strategies, and the available tools that facilitate this verification technique.

What Is Assertion-Based Verification?

Assertions are properties or conditions that must hold true at specific points in a hardware design. They are typically written using formal languages such as SystemVerilog Assertions (SVA). In assertion-based verification, these assertions are embedded in the design code or the testbenches to monitor the behavior of the design during simulation and formal verification.

Importance of Assertion-Based Verification

1. Early Bug Detection: Assertions can catch errors early in the design cycle, reducing the cost and effort required for debugging later stages.
2. Design Documentation: Assertions serve as executable specifications, providing clear documentation of the design’s intended behavior.
3. Improved Coverage: ABV helps in identifying corner cases and scenarios that might be missed by traditional simulation-based verification.
4. Automation: Many EDA tools offer automated assertion generation and checking, enhancing the efficiency of the verification process.

Types of Assertions:

1. Immediate Assertions:

Immediate assertions check conditions instantly during simulation. They ensure that specific criteria are met at the exact moment they’re evaluated. For example, an immediate assertion might verify that a signal equals a certain value during a simulation cycle. These assertions provide immediate feedback on the design’s behavior as it runs.

2. Concurrent Assertions:

Concurrent assertions monitor events over time during simulation. They check for sequences or patterns of behavior across multiple simulation cycles. For instance, a concurrent assertion could confirm that a “request” signal is followed by an “acknowledge” signal within a specified time frame. These assertions help ensure that complex timing and sequencing requirements are met throughout the simulation process.

How ARV-Formal helps in Formal Verification

Agnisys ARV-Formal transforms automatic register verification by automating assertion generation, tackling design complexities, and streamlining the verification process. It surpasses simulations with its faster and more comprehensive approach, by creating a formal verification environment that includes SVA properties. ARV-Formal excels in managing complex designs, providing counter-examples for debugging, and offering an interactive view of assertion results, making it an essential tool for ensuring reliability and early bug detection in system designs. Additionally, ARV-Formal’s automated approach reduces manual effort, minimizing human error and enhancing productivity. It facilitates easier integration into existing verification workflows, allowing teams to quickly adopt its advanced features. The tool’s user-friendly interface and detailed reporting provide clear insights into the verification status, helping engineers make any required changes in their design. By offering robust support for complex verification scenarios, ARV-Formal empowers engineers to meet design requirements and deliver high-quality products on time. Its comprehensive coverage and precision in detecting potential issues early in the design cycle contribute to improved design reliability and reduced time-to-market, making it a pivotal component in modern hardware design and verification.

SW Read Checks generated by IDS-Verify:

1. Verify that the data read from the bus corresponds to the selected field.
2. Ensure that writing to a read-only field results in an error response.

SW Write Checks generated by IDS-Verify:

1. Verify that the data written from the bus is actually being written to the selected field.
2. Ensure that attempting to read from a write-only field results in an error response.

 

How iSpec.ai by Agnisys helps in Assertion-Based Verification

iSpec.ai from Agnisys represents a breakthrough in hardware design verification, leveraging artificial intelligence (AI) and machine learning to automate the translation of natural language specifications into SystemVerilog Assertions. This advanced technology streamlines the creation of precise verification checks directly from English statements of design intent, bridging the gap between natural language descriptions and rigorous hardware verification processes.

Benefits of using ISpec.ai:

1. Automated Assertion Generation: Simplifies the complex task of creating SystemVerilog Assertions from natural language, reducing the reliance on manual coding and enhancing productivity
2. Accelerated Verification Process: Automates the generation and validation of assertions, speeding up the verification cycle and enabling faster time-to-market for electronic designs
3. Enhanced Accuracy and Consistency: Ensures that assertions accurately reflect the intended design behavior, minimizing human error and improving verification robustness
4. Accessibility and Ease of Use: Makes hardware verification simple and easy by making it accessible to engineers with varying levels of expertise, facilitating collaboration across multidisciplinary teams

Some Examples generated by ISpec.ai:

Conclusion

SystemVerilog Assertions are crucial for verifying hardware designs, ensuring they meet specified requirements. ISpec.ai, developed by Agnisys, revolutionizes this process by using AI and machine learning to automatically translate natural English language into SVA and vice-versa. This innovative tool bridges the gap between design intent and formal verification. By automating this critical step required in the verification process, ISpec.ai enhances efficiency, boosts accuracy, and effectively manages complex design challenges. Additionally, ARV-Formal, part of the Agnisys IDS-Verify tool, further strengthens formal verification by automating assertion generation; this is a powerful solution designed to verify RTLs without needing repetitive simulation runs after small changes. It emphasizes the “Property Checking” technique, automatically generating assertions based on IP specifications. This method significantly cuts down the time and effort required for verification, providing a more efficient and reliable alternative to traditional methods addressing design complexity, and streamlining the entire verification process. Together, ISpec.ai and ARV-Formal provide a comprehensive solution that significantly improves the accuracy and efficiency of hardware design verification.