News and New Products

Formal verification goes interactive

Jim Lipman -- EDN, 6/6/1996

Chrysalis Symbolic Design's Design Explore, an interactive formal verification tool for debugging complex chip designs, complements the use of simulation for design evaluation and debugging but without requiring simulation vectors. Until now, you used batch-oriented formal analysis tools to prove the equivalence of a design at different levels of abstraction, such as before and after synthesis from a register-transfer to a gate level. Applying formal verification techniques interactively speeds design debugging over using traditional simulation methods alone. You need neither a simulation vector file nor a testbench to use formal verification. Interactive formal verification lets you interact with a design on a symbolic basis. This basis lets you see cause-and-effect relationships between a design's signals, regardless of the value of the signals. This technique helps you understand how a design behaves under all logical conditions.

You first employ Design Explore to compile a Verilog design into a Symbolic Logic file. You use this file to analyze the entire design or individual design modules or hierarchical subtrees. You then ask Design Explore for information about a design's signals, logic elements, or module instances. Signal names are the basis for most questions. When you ask about an output or state bit, for example, the tool responds in terms of signals that affect the value of the signal of interest. This approach tracks the cause of a problem from the point of observation to its origin. Design Explore's answers to your questions can be textual or graphical. Graphical format lets you visualize logic fan-in and -out and Boolean equations. Using the tcl (tool command language) scripting language, you can add your own combination of commands.

Design Explore runs on Hewlett-Packard, IBM, and Sun workstations, costs $35,000, and is free to owners of Design Verifyer, Chrysalis' formal equivalence-checking tool. The company plans VHDL support for this year.

—by Jim Lipman

Chrysalis Symbolic Design, North Billerica, MA. (508) 436-9909, (508) 436-9697, http://www.chrysalis.com.