MOUTAIN VIEW, Calif. Verisity Design Inc. has added temporal language support to its Specman test-bench development software, embracing a new methodology it calls "spec-based verification." The company's Specman Elite brings some of the advantages of formal model checking into a familiar simulation environment.
In time, Specman Elite will replace today's Specman tool. Like its predecessor, the new offering lets users develop tests in the high-level "e" language, then runs interactively with VHDL or Verilog simulators, communicating through standard programming-language interfaces.
Temporal language constructs let users describe temporal assertions, which define behavior occurring over periods of time. For example, a temporal assertion might state that an "acknowledge" should follow in three to five cycles whenever a "request" is received. Because users can now set up such assertions, Verisity said, it's possible to capture the rules embedded in a spec in an executable form.
"Checking that temporal behavior is correct in VHDL or Verilog is very difficult," said Francine Ferguson, director of product marketing at Verisity, based here. "It's either done in a non-automated fashion with C, or in an extremely procedural way." With Specman Elite, she said, "you capture the rule exactly as it was in the spec, in a declarative way."
Specification-based verification is important, Ferguson said, because it minimizes errors due to ambiguity or miscommunication. It's particularly appropriate for designs using intellectual property (IP) blocks, she said. "Anybody who designs with individual blocks that are brought together for integration will care about this a lot," she said.
Formal model checking is another way to verify assertions in a spec. Unlike simulation, that approach can provide an exhaustive proof-but it takes a new methodology, and it may not be easy to define the properties that need checking. "We allow you to take an easy way of making rules executable, and then applying them to a simulation-based approach," said Ferguson.
Besides letting users describe multicycle scenarios and protocols, Specman Elite's temporal capabilities improve functional coverage and test generation. By using temporal expressions in functional-coverage analysis, Ferguson said, the product learns whether a given sequence of events has been covered.
In test generation, Specman Elite adds what's called "look-ahead constraint solving." The existing Specman product offers constraint-driven test generation, but the constraints are based on data dependencies. The new capability adds the ability to look at dependencies over time.