Breaking News
Comments
Newest First | Oldest First | Threaded View
Graham Bell
User Rank
Author
Application-Specific Static Formal Verification Making an Impact
Graham Bell   9/16/2013 5:32:08 PM
NO RATINGS
At DVCon 2013, the Wednesday morning panel, "Where Does Design End and Verification Begin?", included panelists from ARM, Mentor Graphics, Intel, Gary Smith EDA, and Real Intent. Several panelists mentioned that an application-oriented verification approach resulted in static techniques having a much more significant impact than in the past. They said it is becoming possible for designers to provide meaningful closure (sign-off) on a number of concerns before the design is handed over to the verification team. The biggest takeaway I heard from the audience was an appreciation of the amount of verification possible prior to simulation.

The idea of application-specific verification gives the EDA community the opportunity to develop tools that provide complete solutions to the well-defined verification concerns, rather than just tools that provide raw technologies that the user must then figure out how to apply. These complete solutions are, in fact, a synthesis of various technologies that have been around for many years, but their synthesis is enabled by the narrow scope of the verification concern being addressed. For example, structural analysis and formal analysis work very well together in addressing the clock-domain crossing (CDC) verification problem.

Smart structural analysis provides a baseline analysis of the design in the context of the narrow circuit idioms used to implement clock-domain crossings and creates a formal specification for the formal analysis tools to work on. The narrow scope of each verification concern along with the bringing together of multiple technologies in the solution allows many of these verification tasks to be completed pre-simulation (i.e. statically). This is an important, but not widely acknowledged, enhancement to existing design and verification processes.

 


Terry.Bollinger
User Rank
Author
Hardware needs to learn from software, not vice-versa
Terry.Bollinger   9/16/2013 1:07:51 PM
NO RATINGS
The difficulty in extending the chip-design variant of formal methods to software is simple, yet it tends to get overlooked in discussions like this: Software changes at rates that are orders of magnitude faster than chip designs. This causes one of two things to happen rather quickly: Either the verification falls to pieces, or the verified set of software becomes pretty much useless due to its inability to compete. Because chip design generally addresses only a very narrow sliver of the full formal verification problem, I would respectfully suggest that more useful lessons might be learned by chip designers looking more closely at how formal methods are used (and not used) in nuclear reactors and commercial autopilot systems than vice-versa. Verification in systems subject to rapid change is a very, very hard topic, yet it is also one that more formalists need to recognize as the real problem they should be tackling.



Radio
LATEST ARCHIVED BROADCAST

What are the engineering and design challenges in creating successful IoT devices? These devices are usually small, resource-constrained electronics designed to sense, collect, send, and/or interpret data. Some of the devices need to be smart enough to act upon data in real time, 24/7. Specifically the guests will discuss sensors, security, and lessons from IoT deployments.

Brought to you by:

Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)
Like Us on Facebook
Special Video Section
With design sizes expected to increase by 5X through 2020, ...
01:48
Linear Technology’s LT8330 and LT8331, two Low Quiescent ...
The quality and reliability of Mill-Max's two-piece ...
LED lighting is an important feature in today’s and future ...
05:27
The LT8602 has two high voltage buck regulators with an ...
05:18
Silego Technology’s highly versatile Mixed-signal GreenPAK ...
The quality and reliability of Mill-Max's two-piece ...
01:34
Why the multicopter? It has every thing in it. 58 of ...
Security is important in all parts of the IoT chain, ...
Infineon explains their philosophy and why the multicopter ...
The LTC4282 Hot SwapTM controller allows a board to be ...
This video highlights the Zynq® UltraScale+™ MPSoC, and sho...
Homeowners may soon be able to store the energy generated ...
The LTC®6363 is a low power, low noise, fully differential ...
See the Virtex® UltraScale+™ FPGA with 32.75G backplane ...
Vincent Ching, applications engineer at Avago Technologies, ...
The LT®6375 is a unity-gain difference amplifier which ...
The LTC®4015 is a complete synchronous buck controller/ ...
10:35
The LTC®2983 measures a wide variety of temperature sensors ...
The LTC®3886 is a dual PolyPhase DC/DC synchronous ...