Technical Articles and Videos Upon Request
Formal Verification of Power-Aware Designs Using JasperGold(R) Low Power Verification App
Power reduction and management methods are now all-pervasive in system-on-chip (SoC) designs. They are used in SoCs targeted at power-critical applications ranging from mobile appliances with limited battery life to big-box electronics that consume large amounts of increasingly expensive power. Power reduction methods are now applied throughout the chip design flow from architectural design, through RTL implementation to physical design.
This white paper addresses the verification challenges posed by power-aware chip design, and how the JasperGold® Low Power Verification App works with other JasperGold Apps to overcome those challenges. It covers:
- Power-aware verification challenges
- Power-aware verification requirements
- The limitations of traditional power-aware verification
- Meeting power-aware verification requirements with JasperGold Apps
A Formal Approach to Low Power Verification Presentation
The imperative for reducing power consumption now pervades application spaces ranging from mobile appliances with limited battery life to big-box electronics that consume large amounts of increasingly expensive power. Consequently, power reduction and management methods are now used extensively throughout the chip design flow from architectural design, through RTL implementation to physical design. This presentation outlines how ST Microelectronics has used Jasper Formal technology and Apps to achieve their low power goals.
Verifying Security Aspects of SoC Designs with JasperGold App
This paper presents Jasper technology and methodology to verify the robustness of secure data access and the absence of functional paths touching secure areas of a design. Recently, we have seen an increasing demand in industrial hardware design to verify security information. Complex system-on-chips, such as those for cell phones, game consoles, and servers contain secure information. And it is likely that the presence of this information makes providers vulnerable to unauthorized access to secure data. The potential business loss, direct and indirect, is large, and verifying whether the secure information can be leaked is hard to achieve with conventional RTL validation methods. The security requirements are not easily expressible by regular SVA assertions; therefore, it is not practical to achieve validation with standard formal verification tools. Jasper’s Security Path Verification App (SPV) is part of a wide spectrum of apps we provide for design and verification domains. SPV provides a comprehensive solution to the security path verification problem. With SPV, it is convenient to specify the security paths and perform an exhaustive verification based on our special path sensitization technology, automatic connectivity abstraction, path divide-and-conquer search, and by leveraging the comprehensive core formal engines and usability features of the JasperGold platform. Jasper security path verification has been successfully used by various customers in the SoC domain, confirming the impact of Jasper’s solution and technology roadmap.
Jasper Security Path Verification Presentation
Security path verification is the ability to verify the lack of existence of functional paths touching secure areas of a design. The Jasper security verification technology used in security path verification is based on path sensitization technology, which is used to find paths propagating data to and from secure areas. The Jasper technology can be used to verify requirements that are not expressible by regular SVA assertions, therefore not possible with standard formal verification tools. The Jasper security path verification technology uses special black-boxing to allow scalability to bigger designs and provides for easy debug with special highlighting in the waveform. Download the security verification presentation to learn more.
JasperGold Apps - Property Synthesis Throughout the Design Flow for Application in Formal Verification, Simulation, and Emulation
This white paper describes the JasperGold® Property Synthesis Apps, members of a family of interoperable, application-specific formal verification solutions that addresses verification challenges throughout the design flow [1, 2]. The Apps synthesize both behavioral and structural properties — also known as assertions — for use in formal verification, simulation and emulation. They significantly increase verification coverage while simultaneously boosting property generation productivity by more than an order of magnitude.
Before discussing the JasperGold Property Synthesis Apps in detail, we must first address the need for such solutions, together with their most important characteristics, as identified by property synthesis tool users.
JasperGold Apps - Interoperable Application-Specific Solutions for Formal Verification Throughout the Design Flow
This white paper describes JasperGold® Apps, a family of interoperable formal verification solutions — each of which is targeted at an individual verification application — that addresses formal verification challenges throughout the design flow. The JasperGold Apps approach not only eliminates much of the learning effort historically involved in the adoption and early-stage use of formal verification, but also provides an efficient method for deploying formal across the design team(s) .
Post-Silicon Validation Using Formal Analysis
Verifying the current generation of complex SoCs requires the best methodology and tools, including the application of high-capacity formal verification technologies throughout the design flow, from architectural exploration to post-silicon debug. We see this last area, post-silicon debug, as an important value delivered by formal technology for design and verification teams who have not employed formal earlier in the process to get the design right the first time. As the case studies presented in this article demonstrate, the use of formal to find, fix, and verify the fix adds tremendous value in the post-silicon lab.
Where Should I Use Formal Functional Verification?
With innovations in formal technologies and methodology, the benefits of formal functional verification apply in many more areas. Although a generic awareness of where formal functional verification applies is useful, understanding the "what" and the "why" leads to greater success. Clearly, if we understand the characteristics of areas with high formal applicability, we can identify not only which blocks are good candidates, but also what portions or functionalities of the blocks will give the greatest return on the time and effort invested. In recent years, we have come to realize that although we can apply formal to entire blocks, it can be more valuable to apply formal partially within blocks by choosing the functions that have the highest return. This paper will aid the reader in understanding where, why and how to apply formal for the highest return.
Structured Verification Planning
Integrated circuit verification today has many pitfalls. One of the most significant yet avoidable is the lack of a solid verification plan at the beginning of the process. Effective verification planning adds predictability into the verification flow by specifying exactly what needs to be tested. Planning also provides the necessary structure to identify key areas where complementary verification technologies, such as simulation and formal verification, can each be applied effectively. In this paper, we introduce a methodology of easy, structured verification planning. By providing structure early in the verification process, we show how verification teams can easily implement solid plans to guide their work, seamlessly integrate formal verification and simulation together, and provide solid measurements of verification progress throughout the development cycle.
Modeling and Verifying Cache-Coherent Protocols, VIP, and Designs: Jasper Design Automation and ARM Collaborate to Bolster ACE™ Protocol Deliverables.
This paper describes a novel method for modeling and verifying cache-coherent protocols using Jasper ActiveModel™ technology. The methodology and benefits of using ActiveModel technology to model and verify the ARM AMBA® AXI Coherency Extensions (ACE™) protocol are outlined. In addition, it describes how an ActiveModel protocol model becomes a valuable piece of system-level verification intellectual property (VIP) used to verify RTL designs. Finally, the collaboration between ARM and Jasper that resulted in the development of the interface-level VIP needed to verify RTL designs supporting the ACE protocol are detailed.