Graham is VP of Marketing at Real Intent. He has over 20 years experience in the design automation industry. He has founded startups, brought Nassda to an IPO and previously was Sales and Marketing Director at Internet Business Systems, a web portal company. Graham has a Bachelor of Computer … More »
Informal, Unformal, or Appformal? …and new FormalWorld.org
March 10th, 2016 by Graham Bell
Around the Design and Verification Conference in San Jose at the beginning of the March, a lot of activity was happening in the online world in preparation for the big meetup of the verification community.
First, the DeepChip.com web-site published a set of five (5) articles that surveyed the world of formal verification in EDA, written by Jim Hogan, of Vista Ventures, a Silicon Valley investment firm. Jim is currently on the Board of OneSpin, a formal tools company. Knowing Jim, he did his homework before getting involved with them. If you read the articles, which total 12,000 words, you will have to agree with me there is a lot of great content here. If a technical writer charged for producing this, you would be looking at a bill close to $20,000.
These days you have to two general ways to verify the functionality of your RTL with formal. You either write your own properties and then feed them and the RTL to a formal property verifier (FPV) tool, OR you have an application-focused formal tool automatically read and apply properties to your design.
In the early days of Real Intent we had our own FPV tool. However, by the late 2000’s we realized that designers needed specific solutions to verification problems. And so instead of attacking the general verification market, we focused on clock-domain crossing verification, and automatic code-checks for common RTL problems with FSMs, dead-code, etc. This lead to our existing suite of Meridian and Ascent products which cover five (5) different categories.
In the fourth article by Jim, “16 Formal Apps that make Formal easy for us non-Formal engineers“, Jim uses the “apps” moniker to identify this category. Our CTO, Pranav Ashar, takes exception to this term. In his view, “app” has been subverted to convey a pejorative sense as in “It is just an app!” It has become something to download to your phone to use without a second thought, and with a corresponding low value.
Our Meridian clock-domain crossing sign-off tool fits into the CDC app category, but there is a substantial amount of software technology under-the-hood to make it effective for a wide-range of designs. If CDC is an “app” so is static timing analysis (STA). But nobody calls STA an “app”!
Perhaps this new category of problem-focused formal applications, which are easy to use, need a different label. Since these new formal tools are targeted to ordinary engineers and not PhD’s, perhaps we could call these solutions “informal”, “unformal” or even “appformal”.
What do you think?
Second, a new web-site called FormalWorld.org has just been launched. It is an open and free community, and anyone interested in Formal Verification is invited to post relevant and useful information, or write a blog. It is intended to make it easy to explore and learn about formal, as well as to share experience and research with others. It is sponsored by OneSpin but has pointers and content for all the formal verification suppliers, including Real Intent. OneSpin “will take a hands-off role in its management.”
The site is managed by Jan Kuster, an independent consultant. Contact Jan Kuster with content suggestions or ideas at ContactUs@FormalWorld.org.
I looked around the site and I guarantee you will see something that will interest you.
I did read the blog post by Elchanan Rappaport of Gila Logic. Titled “Formal Evaluations, or the Fine Art of Shooting Yourself in the Foot” it gives a real world experience of introducing a FPV tool to a company and what trouble can arise. A great balance to Jim’s articles, I recommend everyone considering a FPV tool to read it and learn from other’s experience.
One Response to “Informal, Unformal, or Appformal? …and new FormalWorld.org”