Commercial vs Open-Source Tools

This tutorial used SymbiYosys, the open-source formal tool behind ChipVerify Lab. In industry, most formal work runs on commercial tools from the three large EDA vendors. The concepts are the same everywhere: properties, assumptions, covers, bounded checks, induction, counterexamples. What differs is the language support, the engines, the apps, the debug environment and the capacity. This article compares them, so you know what to expect when you move from the lab to a project.

7 min read | Beginner to Intermediate

What You'll Learn

• Name the main commercial and open-source formal tools
• Explain what full SVA support adds compared with the lab form
• Describe the extra engines, apps and debug features of commercial tools
• Choose a tool setup for learning, for open-source projects and for industrial sign-off

The Tools

• Cadence Jasper (JasperGold): a formal platform with many apps, widely used for property checking, connectivity, security and sequential equivalence.
• Synopsys VC Formal: property checking and apps, integrated with the Synopsys simulation and debug environment.
• Siemens Questa Formal: property checking and apps, integrated with the Questa simulation flow.
• Equivalence checkers: Cadence Conformal and Synopsys Formality are the standard tools for RTL-to-netlist equivalence in ASIC flows.
• SymbiYosys with Yosys: open source, used in ChipVerify Lab, in many open hardware projects and in teaching. YosysHQ also offers a commercial edition that adds a full SystemVerilog front end.

Language Support

The biggest practical difference for a learner is SVA. Commercial tools read full SystemVerilog Assertions: assert property with clocking, disable iff, sequences with ## and [*], local variables, s_eventually and bind. The open-source Yosys front end reads the immediate form used in the lab sections of this tutorial, $past and friends, and the Yosys attributes anyconst and anyseq.

Everything in this tutorial can be expressed in both forms, as the "Running It in ChipVerify Lab" sections showed. The SVA form is shorter and is what you will write in a commercial flow.

Engines

A formal tool runs several engines, each good at different problems: bounded model checking, k-induction, PDR (IC3), interpolation, BDD-based methods, and specialized engines for liveness and for arithmetic. Commercial tools run many of them in parallel and pick the first result, often with automatic helper generation. SymbiYosys offers BMC, k-induction with SMT solvers, and the ABC engines including PDR, as the proofs in practice article used.

Apps, Debug and Capacity

• Apps: connectivity, X-propagation, unreachable coverage, register checks, security, sequential equivalence, all generated from tables or coverage databases.
• Debug: waveform viewers linked to the source, "why" analysis that explains each value in a counterexample, property-driven schematic views.
• Coverage: cone of influence and proof-core coverage, merged with simulation coverage.
• Capacity: abstraction techniques and engine tuning for much larger designs, and server farms for parallel runs.

Choosing a Setup

Running It in ChipVerify Lab

The lab gives you the open-source engine with no installation, with BMC up to depth 10 on the free tier and 100 with PRO, three SMT solvers, and waveform counterexamples. The tutorial's lab examples remain the quickest way to try an idea before writing it in full SVA for another tool.

Common Mistakes

m_hold3:  assume property (@(posedge clk) disable iff (rst) req[3] && !gnt[3] |=> req[3]);
a_onehot: assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
a_valid:  assert property (@(posedge clk) disable iff (rst) ##1 (gnt & ~$past(req)) == 4'b0000);
a_fair3:  assert property (@(posedge clk) disable iff (rst) req[3] |-> ##[0:4] gnt[3]);