I was of course delighted to hear this news. I almost rushed out to buy my mother a license for her Mother's Day surprise. I would have been even more delighted if I'd had the faintest idea what a "property" was and why anyone would feel the urge to check one dynamically, so Tom proceeded to elucidate (don't worry, he's a professional and it didn't hurt at all). Well, I was so excited by what I heard that you could have put me in a dress and called me "Laura"!

Representing the design's intent
Before we plunge into the fray, let's make sure we're all marching to the same set of drums. It's generally accepted that verifying one of today's high-end designs typically consumes 70% or more of total development time and resources, so anything that can be done to make this process more efficient has got to be a good thing.

The art of verification is comparing what you've got with what you wanted - that is, comparing the design you've actually created with some representation of what you originally intended to create. But how can we capture the design's intent?

One commonly used technique is to create a testbench that describes stimulus to drive the design's inputs and checks the responses from the design's outputs. This testbench allows us to check whether the design behaved the way we expected it to, so we can view it as being one representation of the design's intent.

Another technique is to create a golden reference model - perhaps as a C/C++ function call - and then build this model into the testbench, use it to generate the expected responses, and compare these responses with what's coming out of the Verilog/VHDL design.

Another approach is to surround the design under test (DUT) with sophisticated bus functional models (BFMs) representing other elements in the system. The term "transaction" refers to a high-level bus event such as performing a read or write cycle. The verification environment can instruct a BFM to perform a specific transaction, and the BFM then generates the complex low-level signal interactions on the bus driving the DUT's interface.

Yet another route is to use "checkers" (or "monitors") that are built into the design code itself or hung off the busses driving the design. As the code is simulated, these checkers will fire off warning and/or error messages if an event occurs that violates the interface protocol. Checkers are stripped out prior to physical implementation

All of the above techniques may, in one way or another, be considered to provide different approaches to representing the design's intent in such a way that it can be evaluated against your implementation. Compared to these techniques, the new kid on the block is the concept of "properties." A very simple property might be along the lines of "Signals A and B should never be active (low) at the same time." But properties can also extend to extremely complex transaction level constructs, such as "When a PCI write command is received, then a memory write command of type xxxx must be issued within 5 to 36 clock cycles."

Thus, properties allow you to describe the behavior of a time-based system in a formal and rigorous manner that provides an unambiguous and universal representation of the design's intent (try saying that quickly). Furthermore, properties can be used to describe both expected and prohibited behavior. They are human and machine-readable, thereby forming an executable specification.

Formal property checking
As is common in the EDA industry, there is some ambiguity to the term "formal verification." The end result is that it means different things to different people. To some it implies the comparison of an RTL version of the design to its gate-level equivalent, or the comparison of two gate-level netlists. But other folks would argue that formal verification really refers to property checking. In reality, both of these tasks use formal techniques to perform their magic, so I'll differentiate between them by referring to the former as formal verification (equivalence checking) and the latter as formal verification (property checking).

There are a number of formal property checkers available. These accept the RTL for a design block and a set of properties associated with that block (for instance, "Signals A and B must never be low at the same time" and "Whenever the request signal goes high, the acknowledge signal should also go high within three clock cycles). The formal property checker then exhaustively analyzes the design to check if these properties are true in every possible case.

With this technique there are no corner cases, because the formal property checker examines 100% of the state space without having to simulate anything. However, this does mean that formal property checking is typically used for small portions of the design only, because the state space increases exponentially with complex properties and you can quickly run into a "state space explosion."

This is where things start to get really cool
The problem thus far has been that properties have only really been used with formal and semi-formal property checkers (where semi-formal combines elements of formal property checking with elements of simulation). But then you have to leap across a chasm into the simulation world. This is where TransEDA's dynamic property checker comes into play, because it can accept the same properties that were used by the formal property checker and verify these properties during simulation.

At the moment there's still a gap between the verification output from formal property checkers and TransEDA's dynamic property checker, but the dream is to move to an environment that supports unified verification metrics, as shown in the figure below.

A unified verification environment

So the idea is that you have a collection of properties that span the design from block to system level. Some of these properties will be developed in-house, but others will come from commercial sources. For example, when you purchase in IP core, it will come with its own set of properties. Then you use formal property checking at the block level, semi-formal property checking at the module level, and dynamic property checking at the system level.

The dream is that once you've checked something at one level -- say using the formal property checker to ensure that two signals can never be active at the same time -- then you really don't have to check that aspect of the design again at a higher level. That is, once you've performed formal property checking on a small "chunk" of the design, you can consider those aspects of that chunk to be fully verified. If these results are fed forward, then when you're working on a larger "chunk" you don't have to spend time re-verifying things that are "known good." This obviously increases the efficiency of the verification process.

But wait, there's more
High-end simulation environments currently provide "code coverage" (what proportion of the RTL has been exercised) and "functional coverage" (which transaction-level events and specific combinations and permutations of these events have been exercised). Augmenting the simulation environment with a dynamic property checker now allows the system to provide "property coverage" (which properties have been dynamically verified and in what circumstances).

If you go back ten or fifteen years when IC designs were entered as gate-level schematics, the industry ran into a major design productivity gap - the number of transistors we could build on a chip started to outstrip the designers' ability to use them. The result was a period of rapid change. We transitioned to using language-driven design based on the combination of hardware description languages and logic synthesis. This was followed by the concept of design reuse and the availability of third-party IP. Both of these concepts resulted in a tremendous leap in designer productivity.

Similarly, today we're running into a verification productivity gap, and the concept of properties has us poised on the verge of a new verification paradigm. For example, today there is very little in the way of verification reuse. If you purchase an IP core it will typically come equipped with a testbench, but this testbench focuses on the I/O signals at the core's boundary. When you integrate the core into the middle of your design, its testbench is essentially useless to you.

Now consider purchasing an IP core that comes equipped with a suite of pre-defined properties, like "Signal A should never exhibit a rising transition within three clocks of Signal B going active." These properties provide an excellent mechanism for communicating interface assumptions from the IP developer to downstream IP integrators. Furthermore, these properties remain true and can still be tested for by the verification environment, even when this IP core is integrated into your design.

And there's yet more, because test automation applications can be enhanced to read properties and use them to automatically create testbenches, and ... the list goes on. In fact, I strongly believe there are tools and ideas that we haven't even conceived of yet. I think that we may be poised on the brink of seeing a flurry of development activity and the emergence of a grab bag of shiny new tools with "go-faster" stripes.

Standards are great ... everyone should have one!
The advent of language driven design saw a plethora of hardware description languages appearing on the scene. Eventually Verilog started to gain ground (but it was proprietary), then VHDL entered the fray and started to capture market share, so Verilog was made open. Then we lived through the "HDL Wars" with proponents of VHDL and Verilog singing their praises (in four-part harmony) and predicting the early demise of the opposition.

Of course, as we all know, we ended up with the worst possible scenario - both languages in widespread use. As today's high-end designs typically make use of large amounts of third-party IP (and may have different portions created in diverse locations within the same company), we end up with mixed-language designs. This requires tools like synthesis and simulation to have mixed-language capability, which has consumed huge amounts of effort and resources.

Just imagine if only Verilog or VHDL had emerged as the victor (I really don't care which one) - in this case the EDA industry could have focused its efforts on creating way better versions of much simpler tools (and we poor design engineers wouldn't have had to learn multiple languages).

But what about properties? How would you like four or five competing standards? If like me your reaction is "Please, not again!" then you'll have been as delighted as I was by the April 22 news announcement from the Accellera Formal Verification Technical Committee. After months of careful deliberation and debate by members of the committee, which represents a wide variety of electronics and EDA companies, they selected the Sugar formal property language from IBM.

Only three days later, on April 25, a bevy of some of the most influential EDA companies on the planet issues press releases rallying behind the language. These include 0-In Design Automation, Inc.; @HDL, Inc.; Cadence Design Systems, Inc.; Co-Design Automation, Inc.; Galileo Technology - a Marvell Company; IBM; Infineon Technologies; Mellanox Technologies, Ltd.; Mentor Graphics Corporation; NoBug Consulting; Novas Software, Inc.; Real Intent; Structured Design Verification Inc.; TNI-Valiosys; TransEDA PLC; Veritable Inc.; Verplex Systems Inc.; and Zoran Corporation. With this much support, you can bet that others will be jumping on the bandwagon before long.

For my part, I think the entire concept of properties is tremendously exciting, especially the prospect of design environments that include formal, semi-formal, and dynamic property checking combined with unified property verification metrics. Ten years from now, I think there's a good chance we'll all be looking back on this period as a pivotal point in verification technology, which has to be worth an official "Cool Beans!" Until next time, have a good one!

Clive (Max) Maxfield is president of Techbites Interactive, a marketing consultancy firm specializing in high-tech. Author of Bebop to the Boolean Boogie (An Unconventional Guide to Electronics) and co-author of EDA: Where Electronics Begins, Max was once referred to as a "semiconductor design expert" by someone famous who wasn't prompted, coerced, or remunerated in any way.