Learning from the problems of the past to build versatile formal apps.
For those of us involved with EDA tools in the late ’80s and early ’90s, the word “frameworks” brings back memories of rigid methodology and use models, coupled with CAD complexity.
Cadence and Mentor, among others, proposed the EDA framework as a mechanism to provide design revision management coupled with tool flow control (I can already imagine your eyes glazing over). For some situations these were actually quite useful, but engineers working with tools such as Verilog-XL for simulation and Design Compiler (DC) for synthesis under, say, the Cadence Amadeus Framework experienced a loss of freedom just discovered with these new breed of Hardware Description Language (HDL) tools.
The flexibility and ease of use of Verilog-XL in the interactive mode where, as a designer, typing Verilog code on a command line to quickly build up tests and check out RTL blocks seemed lost to the “flow folks” within some EDA companies. Cadence’s Verilog –XL simulator was a powerful tool in expert hands, and it wasn’t that hard to get up to speed with it after getting over the HDL hump. Verilog-XL and DC, together with UNIX CVS for revision control and some helpful scripting was all that we needed.
So let’s fast forward to today and have a look at the emergence of apps in formal verification. The idea of apps for executing a specific verification task using the power of a formal platform, without having to get entwined in assertion writing or understanding the tool, is extremely powerful. It is the use of apps that has propelled formal from a tool for specialists to general engineering teams, effectively introducing the approach into accelerated mainstream development processes.
However, while these apps are very useful, there is a slightly darker side to them. What if you are using a standard Register Checking App, the app that compares a register address map and checks the actual implementation of the corresponding registers in a code block? Maybe you would like to also check that each register can be accessed correctly using a specific scheme to the block, or through a standard bus protocol. A slight tweak to the app code could accomplish this. However, most of these apps are binaries where the underlying code cannot be viewed or modify. So now you are back to writing the whole test out as assertions from scratch.
The use of the word app suggests an application on a smartphone, and in some cases that’s a pretty good analogy. However, as we all know, designing semiconductor IP requires a little more complexity and versatility in the tools that are used, and we have to find a happy medium between complete, rigid automation and the full flexibility, and complexity, of the formal tool.
This is where frameworks fell down. A framework never quite seemed to have the versatility required for HDL design. If an engineer was whipping up a gate level schematic, doing a quick rule check, simulating it, and then passing the netlist to a P&R tool, the framework was fine. Also, using the HDL tools with their full complexity and raw UNIX capabilities worked well as long as you learned the tools, which we all did eventually. However, most engineers needed some level of flexibility and customization in a simpler fashion and had a hard time getting this out of the framework for various reasons.
Formal apps need to be accessible. I like the concept of Flex-Apps. The source code, or at least some of it, needs to be available for those wanting to add some specialized detail, without requiring a return to the drawing board. Indeed, open and available apps actually aid the learning process. If you can see those assertions and use them as base examples, it is becomes more obvious how the formal tool works, and puts engineers on the path of full access to this powerful verification technology. OneSpin’s policy has been to provide visible code apps with our formal tools (no surprise).
Maybe we can take this a stage further. If the creation of flexible apps is made easier, then why make app creation only available to the formal companies? Clearly there is a need for custom apps to meet individual company needs. OneSpin provides our formal platform to other companies so they can ship it with their own apps. In this day and age would you expect Apple to provide every app that comes with the iPhone?
In today’s development flows, where code openness and design communities are becoming more prevalent, a Flex-App approach for formal could propel a whole new level of customized verification tooling. Remembering the lessons of the framework era is key in this development.