Rigorous coverage-driven functional verification from block to chip, leveraging formal technology
OneSpin provides a complete formal-based solution for the verification of RTL designs from the IP and block level to complete systems-on-chip (SoCs), as well as verification of implementation in FPGA devices. This solution focuses on five key verification tasks:
- Agile design with early, automated design code verification for rapid design iterations
- Comprehensive assertion-based verification with unique model-based mutation coverage
- Scalable integration verification and functional analysis using automated apps
- Verification of FPGA implementations with advanced optimizations
- Easy bug detection and functional verification of SystemC/C++ code prior to high-level synthesis
Agile Hardware Design
The early elimination of bugs in an IC development process saves time and energy. This places pressure on component designers to perform more verification. However, given traditional simulation-based verification techniques, the ultimate result of this trend is designers spending more time creating stimulus and getting involved with overall verification, and less on creative design.
OneSpin’s DV-Inspect™ design evaluation solution enables closed-loop agile hardware design iterations without the need to write test stimuli, removing burdensome aspects of verification from the designers. The agile development movement suggests an interactive model where designers create, quickly test, and integrate small, valuable code sections. These ideas translate well into the IC hardware design process in general but require new thinking in terms of verification techniques.
OneSpin provides a verification solution with low setup and usage overhead that demonstrates design operation without stimulus creation, automatically tracks real design issues without pages of false negative results, and allows code optimizations to be checked at the push of a button.
Using formal technology as an enabler, OneSpin’s DV-Inspect provides:
- The ability to witness and observe design operation with no or little stimulus, graphical manipulation or scenario setup. This allows a designer to see what is going on in the code, quickly and effortlessly. Test creation is automated for later simulation, if necessary.
- Static design inspection to check for a number of issues at a formal level, examining code operation for real problems rather than just code syntax for possible issues. This saves hours of log file analysis while detecting tougher bugs.
- Automated apps to ensure correct protocol usage, X state elimination after reset, etc. This simplifies specific time-consuming tasks.
A thorough and complete test of all blocks in an IC is essential. A single bug in a production IC is expensive to fix and can cause catastrophic product failure in the field. Block-level verification has traditionally made use of complex test benches, employed across multiple batch-mode simulation runs. Even with this verification horsepower, it often proves hard to achieve verification closure, especially when based on simulation code coverage metrics.
With formal verification, assertions are used to express functional properties to be either proven or disproven, and in this manner the most complex design scenarios are fully investigated. In order to execute a variety of scenarios in a reasonable timescale, and to contain the entire block under test, a superior level of formal technology is required. OneSpin’s 360 DV-Verify™ builds a highly optimized formal model and leverages a broad range of formal algorithms to ensure that the design is verified as quickly and efficiently as possible. In addition, the solution contains advanced debug and ease-of-use features that simplifies tracking and debugging problems.
To enable a closed loop, metric-driven verification solution, OneSpin’s Quantify™ provides the precise model-based mutation coverage mechanism. This analyzes the design code to ensure that any change will trigger at least one assertion, providing both an overall measure of coverage, as well as guidance to particular coverage holes.
The integration of IP into larger blocks and sub-systems continues to require greater degrees of verification resources. Hierarchical bus and network structures, intricate power control and clocking schemes, and security functionality are all commonplace on these devices, making their verification complex and multi-faceted. Formal techniques can be applied effectively at this level to provide much of the integration and functional analysis required, and many verification tasks may be automated.
OneSpin’s block integration verification solution leverages formal technology using a range of automated apps that are particularly effective for the integration task, as well as for other phases of the development flow. The framework for these blocks might be created right at the beginning of the design process, where the designers fill in components and the verification team builds tests and assertions to verify it over nightly regression runs. Alternatively, a complete SoC, including a processor sub-system, might come together later in the design process.
Either way, IP and block integration requires both integration and functional checks of the combined modules. These checks are traditionally performed using simulation, but given the scale of these subsystems, setting up simulation runs to exhaustively test these areas has become difficult. OneSpin’s formal apps save significant effort on otherwise time-consuming and error-prone tasks. It is possible to automatically check a number of standard integration requirements, including the connectivity of key signals, the addressing and operation of registers, and the use of standard communication protocols.
OneSpin provides a range of automated apps that are particularly effective for the integration task, as well as for other phases of the development flow. These may be used to reduce simulation and/or emulation effort:
- Structural Analysis: Focused formal-based structural code analysis
- Safety Checks: Operational checks for standard coding problems
- Activation Checks: Ensuring that code segments can be activated
- Score Boarding: Ensuring functional communication channel integrity
- Protocol Compliance: Validating the implementation of bus protocols
- Register Checks: Comparing registers to an IP-XACT address map
- Connectivity Checking: Ensuring key connectivity through device structures
- X-Propagation Checking: Power-up and potential instability checks
More applications solving integration tasks are available from partner companies. These apps have been developed by domain experts using the OneSpin 360 LaunchPad™ capability that allows the integration of the OneSpin formal platform into the third party products:
FPGA Implementation Verification
FPGAs make use of a static hardware matrix, where the ratio of registers to inter-register logic is somewhat fixed. To drive the highest quality designs, state-of-the-art automated design flows leveraging aggressive optimizations are employed. The combination of these optimizations on a varied range of RTL code styles can lead to the introduction of “systematic” errors. These errors can occur in unexpected ways, are often time consuming to detect, and potentially destructive.
OneSpin’s EC-FPGA™ prevents these problems by applying formal verification to FPGA synthesis. This allows for the highest confidence in design operation, while also improving the development schedule and quality of results (QoR). This is far superior to heavy regression testing on the FPGA itself, which requires many days of stimulus creation and execution, with no guarantee of RTL to gate equivalence.
In addition, if an issue is identified, it is hard to pinpoint the root cause of the problem, due to limited debug visibility in the FPGA device. Finally, after eliminating the problem, the process has to start again, involving time-consuming re-synthesis, and the same heavy regression testing. For large FPGA devices, or when safety-critical applications are targeted, this can lead to an unbearable burden on the design schedule.
EC-FPGA formally verifies the RTL netlist against the RTL source. EC-FPGA has the unique ability to handle retimed FPGA designs, making it an effective tool to track down systematic errors in the synthesis and place-and-route (P&R) design flow. Since these advanced optimizations often change state elements, EC-FPGA uses sequential equivalence checking to handle the mapping between the RTL and netlist. This solution is being used by the largest FPGA vendors to test their own synthesis tools and support major FPGA synthesis flows.
Applying OneSpin’s EC-FPGA provides the following benefits:
- Confidence that all systematic issues have been eliminated, accelerating test and debug
- Elimination of complex test creation or the need to predict systematic errors
- Confidence that no corner-case bugs exist in the final design, increasing reliability
- Leveraging the most aggressive optimizations available, leading to power, speed, and utilization improvements
High-level synthesis (HLS) transforms algorithmic and potentially untimed design models, often written in SystemC and C++, to fully timed RTL design blocks. HLS tools are particularly popular as a method to rapidly generate design components with varying microarchitectures, while optimizing algorithm processing datapaths rapidly and effectively. This provides substantial benefits in terms of flexibility and time-to-market. Consequently, HLS is now in use at many large semiconductor and electronic systems companies. However, the verification options for SystemC and C++ designs have not kept pace with the synthesis technology.
Due to the limited availability of SystemC tools, much of the verification task is performed on the resulting synthesized RTL code, introducing a level of indirection that makes correcting issues at the SystemC/C++ level complex and time consuming. In addition, artifacts of the SystemC standard, including the lack of an unknown, or X, state and potential race conditions between threads, result in further ambiguity that must be eliminated before synthesis. Specific issues related to this abstract design level may be easily tackled with the right verification methods, improving final design quality.
OneSpin’s SystemC/C++ design verification solution provides a formal verification environment allowing for easy bug detection and functional verification of SystemC/C++ code prior to high-level synthesis. A broad range of formal verification techniques can be applied to SystemC and C++ components with varying levels of timing and code abstraction.
Hardware issues, such as the detection of uninitialized value propagation, or the effects of undefined operations (e.g., array out-of-bounds) may be effectively detected using OneSpin’s automated apps at the SystemC/C++ level. A SystemC-specific automated arithmetic overflow check has been added to DV-Verify™, allowing for the inspection of number precision across algorithmic datapaths.
Full assertion-based formal verification is also supported, allowing comprehensive, temporal SystemVerilog assertions or C asserts to be tested against SystemC/C++ design code. This provides a rich verification capability that makes use of a common assertion mechanism that can also be applied to post-synthesis HDL code.
OneSpin 360 DV-Inspect™ takes designer’s pain away and automatically and exhaustively analysis RTL source code prior to functional verification and synthesis, eliminating hard to find implementation errors early in the design process.»Learn more about DV-Inspect™…
OneSpin 360 DV-Verify™ goes beyond that by providing a unified, coverage-driven assertion-based verification flow, and including a full verification app library, as well as means for easy design exploration, all in one tool.»Learn more about 360 DV-Verify™…
OneSpin 360 EC-RTL is an easy to use Sequential Equivalency Checking tool that to ensures functional equivalence between RTL design revisions.»Learn more about 360 EC-RTL…
360 EC-FPGA is an automatic sequential equivalence checking tool that provides a fast and efficient method to ensure that aggressive synthesis optimizations have not introduced systematic errors that could disrupt the final design.»Learn more about 360 EC-FPGA…
OneSpin provides a complete set of formal apps as part of OneSpin 360 DV. On top of that, additional innovative capabilities are available, targeting for example safety critical design, or hardware security as special apps and from third party providers.»Learn more about our DV Apps Library…
OneSpin 360 DV-Verify™ goes beyond that by providing a unified, coverage-driven assertion-based verification flow, and including a full verification app library, as well as means for easy design exploration, all in one tool.»Learn more about the Quantify Coverage App…
The OneSpin 360 Design Verification (DV) product line leverages the most advanced, high-performance formal technology as the basis for a range of verification solutions, from automated design analysis to advanced property checking.»Download the flyer…
The OneSpin 360 EC-FPGA solution ensures that advanced FPGA synthesis optimizations, used to achieve competitive functionality, performance, power consumption, and cost targets, do not introduce functional errors.»Download the flyer…
OneSpin 360 DV-Verify extends the DV- Inspect platform with coverage-driven Assertion-Based Verification (ABV). Many entry-level formal apps allow for assertion generation for specific problems without a need for deep formal knowledge.»Download the data sheet…
360 DV-Inspect automatically inspects the RTL code once it has been compiled, without the need for any testbench setup.»Download the data sheet…
The OneSpin 360 EC-FPGA™ solution ensures that advanced FPGA synthesis optimizations, used to achieve competitive functionality, performance, power consumption, and cost targets, do not introduce synthesis and optimization errors.»Download the data sheet…
OneSpin® 360 EC-FPGATM is an automatic sequential equivalence checker that prevents field programmable gate array (FPGA) design flows from introducing synthesis, place-and-route and other implementation errors.»Download the data sheet…
This white paper presents an implementation signoff flow proving that the final FPGA netlist is functionally equivalent to the RTL model. Based on FPGA-specific, mature formal verification technology, the solution is exhaustive and efficient, catching many issues before synthesis starts.»Download the white paper…
"We had a positive experience in adopting formal verification within a RTL development process that implemented Agile-recommended practices in a localized, low-risk fashion. This approach appears to be an effective and pragmatic way to improve the RTL development process by harnessing some of the benefits of Agile." Sergio Marchese, Verification consultant at TeraStatic.»Read the full article on Tech Design Forum…
"The incremental approach allows for feedback between teams far, far sooner than would typically happen using a waterfall approach. The feedback exchanged between teams that are working toward the same goals simultaneously gives many more opportunities to clarify design intent and holds far less potential for long schedule slips." Neil Johnson, Principal Consultant – XtremeEDA Corp., Bryan Morris, VP Engineering – XtremeEDA Corp.»Read the full article on AgileSoc.com…
"Agile development techniques are now sweeping through the software community transforming the way we develop software. But apart from a few isolated reports the hardware community has been largely untouched by this revolution." François Cerisier and Mike Bartley, Test and Verification Solutions.»Read the full article on Design & Reuse…
"While there are obvious differences between software development and hardware development, there are also significant similarities. The key for hardware developers is to resist getting caught up with the differences and to instead focus on the similarities. Doing so makes it hard to argue that the values of the agile manifesto and agile practices could not be used to achieve the same benefits that software developers have been realizing for years." Neil Johnson, Principal Consultant at XtremeEDA Corp.»Read the full article on EE Times…
We are uncovering better ways of developing software by doing it and helping others do it. Through this work we have come to value:»Read the complete Agile Manifesto…
Muhammad Haque Khan, product specialist for Synthesis Verification, is speaking about our FPGA-specific, mature formal verification technology, that is exhaustive and efficient, catching many issues before synthesis starts.»Watch the video now…