News and New Products

EDA startup brings formal analysis to the system level

By Michael Santarini, Senior Editor -- EDN, 4/25/2005

Newcomer Calypto Design Systems hopes to accelerate the adoption of system-level design methodologies with this week's release of a block-level equivalence-checking technology that brings formal analysis to the system level.

Devedas Varma, Calypto's CEO, said the company is attempting to dismantle one of the biggest roadblocks standing in the way of more widespread adoption of system-level methodologies: Designers create system-level models in C, C++, SystemC, and SystemVerilog, but, because of a lack of mature behavioral-level synthesis, they are forced to manually recreate their design in RTL to run them through the traditional hardware design flow.

This manual process can introduce functional errors. And even if viable behavioral tools existed, design teams would need some independent method to ensure that their design intent was carrying over to RTL from system-level design. That verification is what Calypto believes it is introducing to the market with its Sequential Logic Equivalence Checker (SLEC) product family.

The first tool, SLEC System, is for proving the functional equivalence of blocks modeled in system languages such as C, C++, SystemVerilog, and SystemC against blocks implemented in RTL. The tool also verifies functional equivalence across levels of sequential and data abstraction, comparing equivalence of untimed to timed and word-level to bit-level domains.

The second tool, SLEC RTL, is for ensuring that changes in the Verilog or VHDL RTL microarchitecture, to adjust timing, power, and area, don't introduce new functional errors.

Today's generation of equivalence checkers uses combinational equivalence checking engines, which perform one-to-one flip-flop matching between gate-level blocks under test and the previous version of the gate-level design, according to Mitch Dale, Calypto's director of product marketing. Because those engines do not account for changes across sequential and data abstraction, they can't be used at the system level, Dale said.

"Whenever you encounter things like resource sharing or have major temporal changes to the design and interfaces, traditional tools break down," he said.

SLEC gets past this because it uses a hybrid engine that combines simulation with formal analysis, Dale said. The tool uses a word-level solver that allows it to work at different levels of abstraction. "It allows us to take something that is in bits and equate to something at the word level," Dale said.

The tool has a hardware-intent-extraction engine that looks at a design and infers hardware intent to perform sequential abstraction, Dale said. Finally, the tool uses induction-based proofs or a set of heuristics that allows them to prove designs are functionally equivalent.

"The tools run some cycles of simulation to determine setup and initial conditions, and from there it lets the formal engines pick up the design and do formal analysis," Dale said. "You may encounter a bug, and the tool will show you a difference and generate a counterexample."

When the SLEC tools find a difference, they will create a VCD file or a 3- to 5-simulation-cycle test bench so that designers can locate problems quickly in simulation.

The SLEC tools currently have a capacity of 50,000 to 200,000 gates, but Varma said the company is working on increasing their capacity. Calypto is also creating a hierarchical version of the tool that would more efficiently handle full chip verification. In the meantime, users can blackbox areas of their designs as they are verified.

Each SLEC tool starts at $175,000 for an annual license.