SymbiYosys tutorial · Chapter 1 of 10 · 15 min
What is SymbiYosys, and how does a proof run?
This chapter defines SymbiYosys and follows one proof from a Verilog file to a verdict. It explains what each proof mode guarantees, which engines answer the question, which assertions the free tools accept, and how SymbiYosys compares with commercial formal tools. Chapter 2 installs it.
What is SymbiYosys?
SymbiYosys (sby) is “a front-end driver program for Yosys-based formal hardware verification flows”.
Every verification job therefore involves three programs:
- sby reads the job file (
.sby), creates a work folder for each task, runs the other two programs, and reports the result. - Yosys is “a framework for RTL synthesis tools”. It reads your Verilog and builds a formal model of the design: its state, its inputs, and the properties to check.
- A proof engine searches the model for a property violation, or for a proof that none exists. The default engine,
smtbmc, is the yosys-smtbmc program, which ships with Yosys. It turns each question into formulas and passes them to an SMT solver: a program that decides whether a logical formula over theories such as bit-vectors and arrays can be satisfied (SMT stands for satisfiability modulo theories). Its default solver is Yices 2, “a solver for Satisfiability Modulo Theories (SMT) problems” developed by SRI International.
Two practical consequences follow from this structure:
- An error message comes from one of the three programs. sby reports a mistake in the job file, Yosys reports a Verilog error, and the engine reports a timeout or an inconclusive result. Identifying which program wrote the message is the first step in fixing it.
- The three programs must come from matching releases. sby, Yosys and the solvers are separate projects. Chapter 2 installs all of them from one dated release, in which every tool is built from the same day's source code.
SymbiYosys and Yosys are free and open-source software, released under the ISC license.
How does a proof run, step by step?
Every task follows the same six steps. The figure names the file each step writes, so you can open each one after your first run in Chapter 3.
The steps of one task. Each box names what the step does and the file it writes in the task's work folder, for example counter_bmc/model/.- sby reads the job. For each task it creates a work folder named after the job and the task, such as
counter_bmc/, and copies the files listed under [files] into its src/ folder. - Yosys runs your script. The
[script] section contains Yosys commands. read -formal parses the Verilog with the macro FORMAL defined and turns assert, assume and cover statements into formal cells. prep -top names the top module and elaborates the design hierarchy. The result is saved as model/design.il. - sby prepares the model for proof. Two of its commands change how your design behaves in the proof. First,
async2sync converts asynchronous resets and latches to synchronous logic; with multiclock on in the job file, sby uses clk2fflogic instead, which models clocks and asynchronous events explicitly. Second, every wire that nothing drives becomes a free input, which the solver may set to any value in every cycle. A signal you forget to connect is therefore unconstrained, not zero. - Yosys exports the model for the engine, in the format that engine reads.
smtbmc reads the SMT-LIB language, the common input language of SMT solvers. abc and the aiger engines read AIGER, “a format, library and set of utilities for And-Inverter Graphs”: circuits built only from AND gates and inverters. The btor engines read BTOR2, “a word-level model checking format”, which keeps multi-bit values as words instead of single bits. - The engines run. When
[engines] lists more than one engine, sby starts them together and stops the others as soon as one returns a verdict. - sby reports. The last line of every task is a
DONE line with the verdict. A failure or a cover also leaves a waveform trace and a Verilog testbench that replays it.
What does each proof mode check?
The mode option sets the question that the engine answers. The three modes used in this tutorial are bmc, prove and cover. A PASS means something different in each, so read every PASS together with its mode.
What each mode searches: bmc examines a fixed number of cycles after reset, prove examines every reachable state, and cover looks for one path to a target condition.mode bmc (bounded model checking, BMC) examines the first depth cycles after reset and asks whether any assertion can fail within them. The default depth is 20. A PASS covers those cycles only.mode prove asks whether any assertion can fail in any cycle. With smtbmc the method is k-induction. Its base case checks that no assertion fails in the first k cycles after reset. Its induction step checks that k consecutive cycles in which every assertion holds cannot be followed by a cycle in which one fails. k-induction can end in a third verdict, UNKNOWN: the method found no failure but could not complete the proof. Chapter 3, Run 4 produces this verdict on a correct design and then completes the proof.mode cover asks whether the design can reach a condition. For each cover statement, the engine looks for a trace from reset that reaches it. A cover exposes an assertion that passes only because the design never does anything.
A fourth mode, live, checks liveness properties: properties stating that something must eventually happen. This tutorial does not use it.
Which proof engines does SymbiYosys run?
The [engines] section selects the algorithm. Each engine accepts only some modes; sby stops with an error if a job pairs an engine with a mode it does not support. Besides Yices, the engines use these solvers and model checkers from the suite:
- Bitwuzla is “a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations”. It succeeds Boolector, an SMT solver whose repository is archived and states that “Boolector was succeeded by Bitwuzla”.
- Z3 is “a theorem prover from Microsoft Research” that also works as an SMT solver. cvc5, an SMT solver led by Stanford University and the University of Iowa, is also in the suite.
- ABC is “a growing software system for synthesis and verification of binary sequential logic circuits”, from the Berkeley Logic Synthesis and Verification Group. Its
pdr command implements IC3/PDR: a method that proves a property without unrolling the design, by building an inductive strengthening of the property step by step, or finds a counterexample. Aaron Bradley published the method and named his implementation IC3; Eén, Mishchenko and Brayton named the method property-directed reachability (PDR). - rIC3 is a bit-level hardware model checker based mainly on IC3. Avy, by Arie Gurfinkel and Yakir Vizel, is an AIGER model checker that combines interpolation with property-directed reachability. super_prove, run by the
suprove engine, is a prover built on ABC. - Pono is an SMT-based model checker. btormc is a BTOR2 model checker that ships with Boolector.
The table lists the engines in the suite and the modes sby allows for each.
| Engine line | Algorithm | Modes | Notes |
|---|
smtbmc | BMC, k-induction and cover search over SMT | bmc, prove, cover | The default. Uses Yices unless you name another solver. |
smtbmc bitwuzla | The same, with another SMT solver | bmc, prove, cover | Also z3 and boolector. |
abc pdr | IC3/PDR | prove | Constructs the inductive invariant itself. |
aiger rIC3 | IC3 | bmc, prove | SymbiYosys supports rIC3 version 1.5.2, the version in the suite. |
aiger avy | Interpolation combined with PDR | prove | |
aiger suprove | super_prove, a prover built on ABC | prove, live | Not included in the Linux arm64 build of the suite. |
btor btormc | BMC over BTOR2 | bmc, cover | |
btor pono | BMC over BTOR2, with Pono | bmc | |
Changing the engine can turn an UNKNOWN into a PASS; Chapter 3, Run 6 shows this on the counter. To compare engines on a design, run sby --autotune job.sby. On the counter from Chapter 3, autotune tries 26 engine configurations, finds that all 24 smtbmc configurations end UNKNOWN, and ranks abc pdr first and aiger suprove second. Autotune ends with DONE (AUTOTUNED, rc=0): a recommendation, not a verdict. Put the recommended engine in the job file and run the job again.
What does the OSS CAD Suite contain?
The OSS CAD Suite is “a binary software distribution for a number of open source software used in digital logic design”: the tools come compiled and ready to run. YosysHQ, the company that maintains Yosys and related open-source EDA projects, builds the suite every night from the current source code of each tool and publishes each build as a release named after its date, such as 2026-10-22. Formal verification uses a small part of it. Besides sby, Yosys and the engines above, the suite contains these tools that this tutorial uses or names:
The table groups the tools by role and shows which ones this tutorial uses.
| Role | Tools in the suite | Used in this tutorial |
|---|
| Front ends | Yosys (read -formal), sv-elab (read_slang), the GHDL plugin for VHDL | read -formal |
| Formal drivers | sby; eqy for equivalence checking, mcy for mutation coverage, scy for sequences of covers | sby; eqy in Chapter 9 |
| Solvers and engines | Yices 2, Z3, Bitwuzla, Boolector, cvc5, ABC, rIC3, Avy, super_prove, Pono, btormc | All the engines above |
| Waveform viewers | GTKWave, Surfer | GTKWave |
| Simulation | Icarus Verilog, Verilator, cocotb | Icarus Verilog, to replay a trace |
| FPGA tools | nextpnr, Project IceStorm and others | None |
Which properties can the free tools check?
SymbiYosys is the verification tool of open-source projects such as ZipCPU's wb2axip bus components and YosysHQ's riscv-formal processor checks; Chapters 5 to 8 run both. The main limit of the free tools is the property language their front ends accept.
Which properties do the free tools support?
- Immediate
assert, assume and cover statements in clocked or combinational blocks. - The sampled-value functions
$past, $rose, $fell, $stable and $changed inside those blocks. - Solver-chosen values:
(* anyconst *) for a value fixed for the whole trace, (* anyseq *) for a value that can change every cycle. - Bounded proofs, unbounded proofs by k-induction or IC3/PDR, and cover traces.
Which SystemVerilog assertions do the free front ends reject?
SystemVerilog Assertions (SVA) are usually written as concurrent assertions: a clock, followed by sequence operators such as |-> and ##. In Yosys 0.70, the built-in front end and the sv-elab front end handle these forms as follows:
| Property | read -formal | read_slang |
|---|
always @(posedge clk) assert (q == $past(d)); | Accepted | Accepted |
assert property (@(posedge clk) disable iff (rst) q == $past(d)); | Syntax error | Accepted, correct verdict |
assert property (@(posedge clk) req |-> ##1 gnt); | Syntax error | Unsupported SVA feature |
… req |=> gnt, ##[1:3], req[*2], $rose(req) |=> … | Syntax error | Unsupported SVA feature |
… req |-> s_eventually gnt | Syntax error | Unsupported SVA feature |
With the free tools, write each property as an immediate assertion in a clocked block and use $past for earlier cycles, as every example in this tutorial does. Express a sequence such as req |-> ##[1:3] gnt with a small counter or shift register in the formal code. Full SVA requires the commercial front end described in the next section.
What do the free tools not include?
- Ready-made applications for specific checks, such as connectivity, X-propagation or register checking, which commercial tools sell as "formal apps". The suite includes
eqy for equivalence checking and mcy for mutation coverage. - An integrated debugger. You read traces in a waveform viewer.
- Vendor support. Help comes from the documentation and the projects' issue trackers.
What does Tabby CAD Suite add?
YosysHQ sells Tabby CAD Suite, a commercial extension of the OSS CAD Suite. Its principal addition is the Verific front end, which the OSS CAD Suite README describes as supporting industry-standard SystemVerilog, VHDL and SVA. A job then reads the design with verific -sv instead of read -formal.
- Supported SVA. The SymbiYosys documentation lists the supported subset, including
##[N:M], [*N], |->, |=> and disable iff. It states that the support is still in development and that properties spanning more than one clock domain are not supported. - The same tools otherwise. The OSS CAD Suite is a component of Tabby CAD Suite, so the sby, Yosys, engines and solvers in this tutorial are the same.
- Licensing. YosysHQ publishes no list prices; its pricing page refers to an online calculator and to support credits. The OSS CAD Suite README offers a free evaluation license through
contact@yosyshq.com. - Not the same as a Verific license. The SymbiYosys documentation states that these features come with Tabby CAD Suite's Verific front end, not with a separate Verific license used with open-source Yosys.
How does SymbiYosys compare with commercial formal tools?
The three large EDA vendors each sell a formal verification platform: Cadence Jasper, Synopsys VC Formal and Siemens Questa One SFV. Each is organized as a set of apps, one per kind of check. The table compares them with SymbiYosys by capability, as each vendor describes its product. None of the three publishes prices.
| Capability | OSS CAD Suite | Tabby CAD Suite | Jasper, VC Formal, Questa One SFV |
|---|
| Cost | Free (ISC license) | Paid; free evaluation | Paid; prices not published |
| Concurrent SVA with sequences | Not supported (see the table above) | Supported, through Verific | Supported |
| Proof engines | BMC, k-induction, IC3/PDR and others | The same engines | Each vendor's own engines |
| Ready-made apps | Equivalence (eqy), mutation coverage (mcy) | The same | Connectivity, X-propagation, registers, security, sequential equivalence, coverage and others |
| Debugging | Waveform viewer and a replay testbench | The same | Integrated debuggers: Jasper Visualize, Synopsys Verdi |
| Support | Documentation and issue trackers | YosysHQ | The vendor |
Each vendor lists these apps under its own names:
- Cadence Jasper: Formal Property Verification (FPV), Sequential Equivalence Checking (SEC), Security Path Verification (SPV), Connectivity Verification (CONN), and the static Superlint and CDC/RDC apps.
- Synopsys VC Formal: FPV, Automatic Extracted Properties (AEP), Formal Coverage Analyzer (FCA), Formal X-Propagation (FXP), Connectivity Checking (CC), Formal Register Verification (FRV), Sequential Equivalence Checking (SEQ), Security Verification (FSV), Formal Low Power (FLP), Formal Testbench Analyzer (FTA), Datapath Validation (DPV) and Functional Safety (FuSa).
- Siemens Questa One SFV: Property Verification, Connectivity Analysis, Register Analysis, Security Analysis, RTL Equivalence, X-Sensitivity Analysis, Gap Free Analysis, ISA Compliance, FPU Compliance, Fault Protection Analysis and Formal VIP for AMBA, among others.
Which tool should you use?
- To learn formal verification, or to verify blocks and open-source IP you write: SymbiYosys. It runs the same algorithms, its job files are plain text that fits in version control, and it needs no license server.
- To verify existing SVA or VHDL code without rewriting it: Tabby CAD Suite, which keeps the same flow and adds the Verific front end.
- For sign-off on large designs, or for checks that a commercial app automates, such as connectivity or X-propagation: a commercial platform.
The concepts transfer between all of them: what a bounded PASS guarantees, why a true property can fail an induction step, and how to read a counterexample. The syntax and the user interface differ.