Formal verification enables Agile RTL developmentSergio Marchese at TechDesignForum
Agile development started in the software domain but the methodology shows promise for SoC verification. Formal verification techniques can help implement an Agile flow. The aim of this article is to share two experiences where a novel approach was used to develop register transfer level (RTL) modules. System Verilog Assertions (SVAs) were developed in parallel with RTL code using OneSpin Solutions’ 360-DV (Design Verification).
Read the full artile at TechDesignForum.
Using Formal Verification for HW/SW Co-Verification of an FPGA IP CoreProf. Dr.-Ing. Markus Wedler; Berlin Institute of Technology, Eric Crabill; IP Design Engineer; Xilinx, Inc., Graham Schelle; Senior Staff Research Engineer; Xilinx, Inc. and Patrick Lysaght; Senior Director; Xilinx, Inc. at Xilinx Xcell Magazine.
A new formal-verification technique allowed a group of academic and industry researchers to holistically verify tightly coupled hardware and firmware within a Xilinx soft core.
The University of Kaiserslautern and Xilinx researchers recently undertook an investigation into how to apply formal techniques to the holistic verification of a Xilinx® soft IP core that contains both embedded firmware and hardware components. We found that it was possible to capture the firmware and hardware interaction in a scalable formal-verification environment.
Download Xilinx Xcell Journal issue 79, pg. 56.
Are we done yet?Bryon Moyer at EEJournal
It’s all well and good to verify a design, but how do you know when you’re done? Simulation has coverage metrics, so, whether or not you agree with their value, by that definition, you can know when you’re done (or as close as you’re going to get). It’s not so easy with formal analysis. OneSpin is addressing this with their new Quantify MDV product (MDV standing for “Metrics-Driven Verification”).
How formal MDV can eliminate IP integration uncertaintyRaik Brinkmann at EE Times
This article outlines how the latest formal metric-driven verification (MDV) methodology and technologies can eliminate integration uncertainty through the automatic generation of Accellera-defined coverage metrics, without the assistance of simulation. This formal MDV methodology measures not only the usual control coverage, but also observation coverage – a serious missing link in many other MDV approaches. The methodology is easily integrated into existing MDV flows or can be used stand-alone.
Hunting that elusive bugRoland Syba, Melexis GmbH at EE Times
This article discusses the non-trivial challenge of detecting and correcting the – often elusive – functional defects that unavoidably arise in the design of complex system-on-chip (SoC) devices. How do we mitigate the conflict between the dramatic increase in SoC design complexity and the need to deliver the design in a shorter time with the same or better design quality?
OneSpin automates formal assertion/RTL debugBill Murray for SCD Source
What do you do when an assertion fails? How do you determine the cause of the failure? Is the assertion code incorrect? Is there an illegal input scenario that the constraints failed to exclude? Or is there a bug in the RTL code? Or is it a combination thereof?
Without highly automated debug support, it requires significant manual effort to answer these questions. This manual effort can put a serious dent in the team’s productivity, even in the case of relatively simple assertions that verify local RTL behavior.
OneSpin has solved this problem by automating the most effort-intensive steps in SVA analysis and RTL debug.
Formal methods: Rocket science or mainstream technology? A deeper lookMichael Siegel, OneSpin Solutions for SCDsource
Is formal verification only for experts? This is probably one of the most debated questions in functional RTL verification in recent years. The answer to this question is critical to anyone considering adopting formal verification because it determines the necessary investment in skills and technology – and the return on investment (ROI) that companies can expect.
Timing Diagrams Ease Formal Property DevelopmentMichael Siegel and Jörg Bormann, OneSpin Solutions at ChipDesignMag
Here, we describe a systematic formal verification approach that uses the testbench perspective – that of the module-level operations – to verify a module, or any part thereof. Starting from familiar and intuitive timing diagrams that describe the intended behavior of module-level operations, the approach bridges the perspective gap between the testbench and formal verification.
To simplify the capture of timing diagrams as SVA properties, we have developed theTiming Diagram Assertion Library for SVA, called "TIDAL." The library reduces or eliminates transposition errors when developing SVA properties from timing diagrams – reducing both initial effort and rework effort.
Automated formal method verifies highly-configurable HW/SW interfaceJoachim Knaeblein and Hans Sahm, Alcatel-Lucent at SCDsource
Alcatel-Lucent's Joachim Knaeblein and Hans Sahm describe how they used both automated assertion generation and automated formal methods to verify a complex HW/SW interface in a large SDH/SONET chip – and slashed verification time and effort by 70 percent.
Mixing Formal and Dynamic VerificationBill Murry at SCDsource
Over the last few years, there has been a noticeable uptick in the use of formal verification to augment dynamic verification. Given that both techniques leverage assertions, one would assume that there would be a great deal of collaboration between dynamic testbenches and formal property checking, the user teams and the tools.
In this STR, we dig down to the use case level to determine how formal is being used, and how it augments dynamic verification.
Formal Verification Goes MainstreamMike Donlin at SOCcentral
Formal verification is a term that's been kicking around the EDA industry for years, but only recently has seen some success in helping designers verify their complex SOC's, processors and ASICs. When it was first introduced, formal verification usually referred to a methodology that compared versions of a design as it went through simulation and optimization, to ensure that the evolving system still met the original specifications. While many designers still think of formal verification in those terms, the more recent and widely accepted technology is formal functional verification, which uses assertions to find corner case bugs that might be missed by traditional verification techniques.
Formal verification expands its use model by Bill MurrayBill Murray for SCDsource
Holger Busch, senior staff engineer for verification in the automotive, industrial and multi-market group at Infineon Technologies, described an XML-assisted aggregate property checking methodology that performs a “vast” number of checks simultaneously to verify the special function registers in a control unit. The functionality of such registers constitutes a significant proportion of the control unit’s specification. Consequently, simultaneous checking using aggregate properties can verify the complex functionality of modules with considerably less effort than individual property checking or simulation. In addition, the methodology’s completeness checking identifies gaps in the property set, which can then be filled by the verification team.
Formal property checking – what the users sayRichard Goering for SCDsource
Formal property checking and "bug hunting" tools promise to find tough corner-case bugs and provide exhaustive proofs. But what's the reality? In the first part of this two-part report, engineers at IBM, Infineon, D. E. Shaw Research, MIPS Technologies, and Sun Microsystems discuss the advantages and limitations of existing formal tools.
Formal property checking – what the vendors sayRichard Goering for SCDsource
Users profiled in the first part of this report said that formal property checking tools have significant value, but require expertise and have capacity limits. In this conclusion, vendors of formal tools give their perspectives on these challenges and discuss what sets their tools apart.
Now we turn to the providers of formal property checking tools to get their views on such questions as ease of use, capacity, and dynamic versus static property checking.
Achieving Highest, Certified IP Quality EfficientlyLorenzo di Gregorio, Infineon Technologies AG; Carlo del Giglio, Michael Siegel, OneSpin Solutions GmbH
The article describes from the perspective of an IP provider the verification of a configurable network processor – called PPv2 – using OneSpin's 360 MV. It explains the details of this verification project and how the following results were achieved: error-free functional operation of the PPv2 across all possible configuration, a verification report that certifies the achieved IP quality and enables rapid IP quality assessment, a complete description of integration conditions for the IP, a considerably improved specification, no IP revision or redesign has been necessary since release, and a total verification effort of 4 engineer-months, about 40% less than that in the simulation-based verification of PPv1.
Complete Formal Verification of TriCore2 and Other ProcessorsTim Blackmore, Fabio Bruno, Infineon Technologies AG; Jörg Bormann, Sven Beyer, Adriana Maggiore, Michael Siegel, Sebastian Skalberg, OneSpin Solutions GmbH
This paper describes the application of OneSpin's 360 MV to the verification of the TriCore2 processor, Infineon's next generation high-end processor for embedded and safety-critical applications. Unlike other formal approaches, the employed methodology is a self-contained approach to hardware verification, independent of simulation. It systematically eliminates all gaps in the verification plan and in the property set and thus ensures that the IP is free of functional errors – the highest possible quality.
Achieving Completeness in IP Functional VerificationWolfram Buettner and Michael Siegel, OneSpin Solutions at EEtimes
360 MV is the only complete functional verification solution. Verification is objectively 'complete' when all output signals of the design under verification have been verified to have their expected values at any point in time for any possible input scenario. This notion of completeness implies 100% input scenario coverage and 100% output behavior coverage, the highest possible coverage that any functional verification can achieve and the key to ensure error-free operation. It can only be achieved when transforming formal verification from the common bug-hunting and corner-case inspection approach into a full 'functional sign-off' approach. The details on complete functional verification compared to other functional verification approaches – be it simulation-based, assertion-based, or formal – is explained in the following EETimes article: