“All sounds great, but what is 'implied intent' exactly? And how do you actually know what the designer's implied intent is without talking to him?”
Well, the idea is actually quite simple. Say a person wants to jog. The thought of jogging is an expressed intention. To achieve that, all the parts of her body have to cooperate and move synergistically together. Though she never expresses a clear intention of moving her legs, arms and body in a certain way, the intention for how each part of her body should move is implied from the expressed intention of jogging.
For RTL designs, a piece of RTL code might be to implement an arbiter (arbiters are electronic circuits that allocate access to shared resources) so that's the expressed intent of the design. To achieve that, each part of the RTL code has to work together in the right way. If there is dead code in the design, or if a state in the state machine (a state machine is a behavior model composed of a number of states, transitions between those states, and actions) is unreachable, then the design may not function correctly as an arbiter or whatever else the design is intended to be.
So what Verix does is to analyze the RTL design to make sure that each part of the RTL constructs, such as definitions, assignments, blocks of code, state machines, and pragmas (a pragma is a directive communicating additional implementation-specific information), etc., exhibit certain desired behavior in order for all these parts to work together to implement a meaningful functionality.
“If Verix examines each language construct, how is it different from Lint?” (Lint is a type of EDA tool that performs simple checking on RTL designs to catch potential coding errors).
The 'use model' of Verix is indeed very similar to a Lint tool, since only design files are needed to run Verix, which made its adoption easy. The differences lie in the types of behavior analyzed, the underlying technology used, and the depth of analysis.
Lint typically performs simple checks on the design to look for coding issues, sort of like spelling/grammar checker in MS Word. It's a much simpler technology and it can usually be developed in a 6 to 9 month time frame.
Verix, sometimes referred to by its customers as 'Formal Lint' or 'Smart Lint,' goes way beyond that. It employs formal technology and performs deep sequential analysis to detect bugs that will not be detected by Lint tools.
For example, the following piece of RTL code will pass a 'linter' cleanly; however, Verix reports a dead code on Line 8, which is clearly not what the designer intended it to be. The dead code revealed a coding error which would be much harder to detect using other techniques, such as simulation, since only after exhaustively simulating all possible vectors can dead code be confirmed. Verix detects this easily because of the benefit of the underlying exhaustive formal technology. In that sense, Verix is like an editor, looking for complex grammatical errors, rather than merely identifying simple spelling errors in an article.
The founders of Real Intent were justifiably proud of this early work because they were the first to apply formal property checking techniques automatically. Formal property checking used to require truly expert users spending a lot of time writing assertions in order to use the tools. With Verix, everyday users could and do take advantage of the power of formal property checking (exhaustive proof & counter example generation) without the need to spend any extra effort setting things up to run the tool, and/or even fully understanding how it works under the hood. Verix brought out significant productivity gains in the design & verification flow, so much so that automatic assertion generation and verification have since become part of the offerings from other companies, such as Mentor 0-In Formal Verification, Cadence IFV and Synopsys Magellan.
For Dr. Narain and Mr. Kumar, it was no small achievement to pioneer the field of automatic formal verification and set the standard for the industry to follow. It was also therefore no surprise that Verix was awarded the “2000 Product of the Year” by the Electronics Product Magazine (Footnote [1])
Product of the Year Aware by Electronics Product Magazine
“Formal techniques have long held the promise of revolutionizing RTL verification of large complex ICs. However, two problems have withheld the realization of the dramatic benefits of these techniques - ease of use and capacity. Real Intent has made key advances on both fronts", so said Real Intent President and CEO Prakash Narain at award time. "Our latest improvements remove the biggest hurdles in realizing the benefit of formal RTL verification. Our breakthrough allows our customers to continue to leverage their investment in Verix as design complexity increases."
And customers agreed. According to Eric Demers, Engineering Manager at ATI (ATI merged with AMD in 2006), “Verix has been invaluable to us as the first verification tool that we run on our RTL designs. It easily catches a host of design bugs that have traditionally been hard to find in simulation or have taken significant verification cycles to detect. Verix has allowed us to shorten our simulation time by eliminating most common bugs one encounters with new RTL. We are pleased that Real Intent has built a great formal ABV product, and we have come to reply upon it for our graphics projects."
Ads Used for “Got Verix” Marketing Campaign (2001)
Verix 2000 was Only the Beginning
Real Intent kept on developing the technology and expanding its applications in Verix in the following years. Here are just some of the highlights:
- On March 12, 2001, Verix added VHDL support (VHDL stands for VHSIC Hardware Description Language, where VHSIC stands for Very High Speed Integrated Circuit) (Footnote [2]). This enabled Verix's adoption by design houses using VHDL language for RTL designs.
- On May 21, 2001, a hierarchical formal methodology that automatically combines the formal results of lower blocks to formally verify higher blocks, was introduced (Footnote [3]). This was an important breakthrough because traditional formal technology, due to its exhaustive nature, can only be applied to block level designs. The hierarchical formal methodology engineered by
Real Intent enabled scalable formal RTL verification at higher level of the design hierarchy, thereby enhancing the ability of the tool to catch more complex and deeper bugs in the design.
Hierarchical Formal Methodology
- On May 28, 2002,
Real Intent added formal
Clock Intent Verification (CIV) to Verix (Footnote [4]). Recognizing the ever increasing complexity of clock distribution networks in the IC designs,
Real Intent was the first company to target Clock Domain Crossing (CDC) verification using automatic formal technology.
With the knowledge built to understand a design's implied intent, Verix CIV is built to understand the clock intent by automatically identifying the clock domains within the design and the signals crossing the clock domains. It also identifies the absence or presence of synchronizers at the clock domain boundaries, and determines assertions that can exhaustively verify the data transfer stability across the clock domain boundaries.
Verix CIV started off on solid ground with the experiences Real Intent gained with Verix Implied Intent. This in turn built a great foundation for Real Intent's later success of Meridian CDC as the acknowledged best product in the industry performing CDC verification.
- While
Real Intent has created a core competency in automating formal property verification and making it easy to use for mass design and verification engineers, it has also cooperated with and leveraged the expertise developed by
other EDA companies to provide end users with the best overall products. For example, technologies from Verific Design Automation (
www.verific.com ) and SpringSoft (then Novas) (
www.springsoft.com ) have been incorporated into
Real Intent 's tool suites to provide front-end Verilog and VHDL language parser and back-end debugger.
-
Real Intent has also been keen on making its products easier to fit into existing chip design and verification flows, by interpolating with tools from other entities. This philosophy is manifested in many decisions made by the Company, as can been seen from some of the following developments.
Cooperation with Others
By 2005, Verix had been adopted by over 35 companies such as NEC, ATI, SiCortex, and Micronas.
The year 2005 was also a critical point in Real Intent's corporate history. The company raised $6.5 million in financing (Footnote [5]) and added several new executives to the team, including Dr. Pranav Ashar as the CTO of Real Intent (Footnote [6]).
Dr. Ashar
The additional funding also allowed more resources to be added to the team on many other fronts and enabled further development of its Implied Intent, Clock Intent and Expressed Intent technologies .
Verix 5.0 , released on December 12, 2005, achieved even greater performance & capacity breakthroughs with its new formal Convergence Engine (Footnote [7]).
You can find the full EDACafe.com event calendar here.
To read more news, click here.
-- Russ Henke, EDACafe.com Contributing Editor.
