close By using this website, you agree to the use of cookies. Detailed information on the use of cookies on this website can be obtained on OneSpin's Privacy Policy. At this point you may also object to the use of cookies and adjust the browser settings accordingly.

Technical Articles

Read articles and application reports from customers and specialists

Integrating Results And Coverage From Simulation And Formal

Tom Anderson at Semiconductor Engineering

popularity Not so long ago, formal verification was considered an exotic technology used only by specialists for specific verification challenges such as cache coherency. As chips have grown ceaselessly in size and complexity, the traditional verification method of simulation could not keep pace. The task of generating and running enough tests consumed enormous resources in terms of engineers, simulation licenses, and servers. Yet even unlimited simulation capability provided no guarantee of functional correctness. Constrained-random simulation, by its very nature, is probabilistic and has little chance of exercising enough of the design to find deep, corner-case bugs.  

Read the full article at Semiconductor Engineering.

11 Myths About Formal Verification

Tom Anderson at Electronic Design

Formal verification is used by almost every chip development and verification group, though myths about it persist and may deter engineers who could benefit from its value.

Read the full article at Electronic Design.

AI Chips Must Get The Floating-Point Math Right

Sergio Marchese at Semiconductor Engineering

Most AI chips and hardware accelerators that power machine learning (ML) and deep learning (DL) applications include floating-point units (FPUs). Algorithms used in neural networks today are often based on operations that use multiplication and addition of floating-point values, which subsequently need to be scaled to different sizes and for different needs. Modern FPGAs such as Intel Arria-10 and Xilinx Everest include floating-point units in their DSP slices that can be leveraged to optimize classification, detection, and image recognition tasks. Convolutional neural networks (CNNs) are popular for computer vision applications and are demanding on compute power. The computational workload of a convolution layer may involve deeply nested loops.

Read the full article at Semiconductor Engineering.

Certifying the Certifier – OneSpin Talks About the Extra Burden of Proof

Bryon Moyer at EEJournal

This discussion stems from a conversation with OneSpin at this summer’s DAC. Seems like it was just about this time last year that we talked about how EDA and functional safety work together, but, based on some recent certification announcements, this year we have a view from a different stance.

Read more …

Functional Safety: Art Or Science?

Sergio Marchese at Semiconductor Engineering

Nowadays, most hardware development projects deploy functional verification flows that include UVM-based constrained-random testbenches and formal verification. High design complexity, tough budget constraints, and short time to market are the norm, not the exception. Advanced verification is a necessity for many engineering teams. In our increasingly connected world, where billions of IoT devices soon will be communicating to us and to each other, security rapidly is becoming a key concern.

Read the full article at Semiconductor Engineering.

IoT Verification is Harder than it Looks 

Tom Anderson at EE Catalog / Chip Design

As has been the case for at least 20 years, functional verification remains the bottleneck for semiconductor development. Many studies have shown that verification consumes 60-70% of a project’s time and resources. As more and more of the chip’s content comes from commercial intellectual property (IP) or reuse from previous generations, the ratio of effort tips even further toward verification.

Read the full article at EE Catalog.

The Skies Over EDA Are Finally Cloudy

Tom Anderson at Semiconductor Engineering

EDA companies have been talking for years about providing access to their tools in the cloud, including more articles than I can count with titles about the EDA forecast being cloudy, clouds on the horizon, and so forth. The title of this post continues the dubious tradition of cloud-based puns, but there’s no future tense involved. Recent announcements from several EDA companies make it appear that cloud support is finally here and poised to become a mainstream vehicle for design and verification.

Read the full article at Semiconductor Engineering.

Welcome Verification 3.0

Sergio Marchese at Semiconductor Engineering

When considering the future of verification, don’t forget the human factor.

Read the full article at Semiconductor Engineering.

Why Your FPGA Synthesis Flow Requires Verification

Tom Anderson at Semiconductor Engineering

Equivalence checking was key to making logic synthesis mainstream, but it’s more complex when it comes to FPGAs.

Read the full article at Semiconductor Engineering.

ISO 26262 and You

Jörg Grosse at Embedded Systems Engineering

Why Automotive electronics suppliers will make increasing use of formal tools to meet the standard’s strict requirements for verification and satisfy supply chain demand.

Read the full article at Embedded Systems Engineering.

Don’t Underestimate the Challenges of IoT

Tom Anderson on EE Catalog / Chip Design

Adhering to ISO 26262…avoiding repairs to IoT devices in hard-to-reach factory floor locations…dealing with the complexities of server-class chips with as many as eight CPU cores—developers will find no shortage of IoT hurdles to overcome

Read the full article on EE Catalog

Making Sense Of Safety Standards

Tom Anderson on Semiconductor Engineering

If you’re involved in the design or verification of safety-critical electronics, you’ve probably heard about some of the standards that apply to such development projects. If not, then you’re probably puzzled when you read about TÜV SÜD certifying that an EDA tool satisfies functional safety standards ISO 26262 (TCL3/ASIL D), IEC 61508 (T2/SIL 3) and EN 50128 (T2/SIL 3). The industry has quite an “alphabet soup” (more accurately, alphanumeric soup) of functional safety standards. In this post, we’ll try to sort it out.

Read the full article on Semiconductor Engineering…

Bridging the Gap Between Modern, Rigorous FPGA Development Flow and DO-254/ED-80

Sergio Marchese at Embedded Systems Engineering

Focusing on functional verification, this article introduces state-of-the-art formal equivalence checking solutions for field programmable gate arrays (FPGAs) and makes a case for their applicability to AEH development.

Read the full article at Embedded Systems Engineering.

Read more …

Formal verification enables Agile RTL development

Sergio 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.

Read more …

Strategies for verifying an FPGA design

Dave Kelf at Embedded Computing Design

The escalating cost, time, and risk associated with custom integrated circuit (IC) fabrication has driven increased field programmable gate array (FPGA) usage across electronics applications. FPGAs are larger, faster, and more power-efficient than ever, and bring a number of capabilities unavailable in custom silicon design, such as field updates, multi-function devices, and simplified prototyping, making them an attractive option.

Read the full article at Embedded Computing Design.

Read more …

Using Formal Verification for HW/SW Co-Verification of an FPGA IP Core

Prof. 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.

Read more …

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”).

Read more …

How formal MDV can eliminate IP integration uncertainty

Raik 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.

Read more …

Hunting that elusive bug

Roland 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?

Read more …

OneSpin automates formal assertion/RTL debug

Bill 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.

Read more …

Formal methods: Rocket science or mainstream technology? A deeper look

Michael 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.

Read more …

Timing Diagrams Ease Formal Property Development

Michael 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.

Read more …

Automated formal method verifies highly-configurable HW/SW interface

Joachim 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.

Read more …

Mixing Formal and Dynamic Verification

Bill 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.

Read more …

Formal Verification Goes Mainstream

Mike 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.

Read more …

Formal verification expands its use model by Bill Murray

Bill 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.

Read more …

Formal property checking – what the users say

Richard 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.

Read more …

Formal property checking – what the vendors say

Richard 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.

Read more …

Achieving Highest, Certified IP Quality Efficiently

Lorenzo 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.

Read more …

Complete Formal Verification of TriCore2 and Other Processors

Tim 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.

Read more …

Achieving Completeness in IP Functional Verification

Wolfram 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:

Read more …