January 21, 2009 -- Formal property-checking tools—EDA tools that mathematically determine the truth of a set of properties for a given design in order to prove that a design will do what the designer intended—are reaching out for a wider market. Two recent announcements, one by Jasper Design Automation and another by OneSpin Solutions, show the different ways in which vendors of these tools are striving to create more seats.

Initially seen as almost an academic curiosity by many verification engineers, formal tools have earned a valuable place in the verification flow for many design teams. The tools can state definitively, without using simulation or test vectors, whether a particular property is true — and if it is false what the counterexamples are — for a given block of digital RTL. Ideally, then, the design team would only have to establish a complete set of properties to cover the design requirements for a block and then use a formal tool to prove that the block meets the properties. This would be a sufficient proof of correctness for the entire block, and would eliminate the need for any further verification of the block, giving 100% functional coverage.

But limitations in the tools and the unfamiliarity of the theory have both hampered the widespread adoption of formal techniques. Early on, the tools, even when working correctly, presented such daunting user interfaces that it's only a slight exaggeration to say that the tool designers themselves were the only people who could use them effectively.

Tool suppliers have been working hard on the user interface, making it less dependent on a PhD in mathematical logic and more accommodating of the way digital designers think, even adding such utilities as waveform input.

By Ron Wilson, EDN Executive Editor