Skip to content

Reusable ASIC Designs (RAD) – Formal

Overview

The Reusable ASIC Designs (RAD) environment includes a formal verification flow built with open‑source tools. Formal verification works together with RAD's linting, synthesis, and DV flows. It uses math to prove that key safety properties are correct in each design.

The RAD Design flow checks structure and synthesis. The RAD Formal flow checks logic for all possible input sequences.

The RAD Formal methodology focuses on:

  • Practical properties that match the implementation
  • Small, focused proof harnesses
  • Reusable SBY templates
  • Repeatable Make‑based automation

This document describes a flow that fits naturally after initial RTL and design‑side checks and before DV simulation.

Audience

  • ASIC RTL designers adding formal checks to RAD IP
  • Verification engineers using formal together with simulation
  • Architects checking safety and corner‑case behavior

Purpose

  • Check that key safety properties work correctly for all legal inputs
  • Find corner‑case bugs earlier than simulation
  • Provide automated, repeatable proofs that work with Make
  • Use the same structure for formal files across all RAD designs

Key Features

  • SymbiYosys‑based flow (prove and cover)
  • Reusable SBY templates for each design
  • Standard formal testbench structure
  • Open‑source SMT solvers (Boolector recommended)
  • Make‑based automation for proofs and coverage
  • Same directory structure for each rad_<design> design

Getting Started

Set Up and Install the Environment

See ABE Python Development for Python environment setup details.

make py-venv-all
source .venv/bin/activate
make py-install-all

Install Required Tools

make deps

This shows any missing tools. Installation steps depend on your platform and are not covered in this document.

Run Examples

make DESIGN=rad_async_fifo formal
make DESIGN=rad_async_fifo formal-cover

Examine Outputs

  • out_formal/<design>
  • out_formal/<design>_cover

Explore Relevant Directory Layout

.
├── mk
│   ├── 00-vars.mk
│   ├── 10-helpers.mk
│   ├── 20-python.mk
│   ├── 50-formal.mk
├── src
│   └── abe
│       ├── rad
│       │   ├── rad_async_fifo
│       │   │   ├── rtl
│       │   │   │   ├── rad_async_fifo_mem.sv
│       │   │   │   ├── rad_async_fifo_rptr.sv
│       │   │   │   ├── rad_async_fifo_sync.sv
│       │   │   │   ├── rad_async_fifo_wptr.sv
│       │   │   │   ├── rad_async_fifo.sv
│       │   │   │   └── srclist.f
│       │   │   ├── formal
│       │   │   │   ├── rad_async_fifo_cover.sby
│       │   │   │   ├── rad_async_fifo_formal_top.sv
│       │   │   │   └── rad_async_fifo.sby
│       │   ├── shared
│       │   │   ├── rtl
│       │   │   │   ├── rad_pulse_gen.sv
│       │   │   │   └── rad_timescale.svh
├── Makefile

Makefiles

Makefiles are in directory mk.

  • Common flags come from 00-vars.mk.
  • Formal commands are in 50-formal.mk.

Common commands:

make formal-help

Initial Steps

  1. It's helpful to complete design‑side checks first:
  2. rtl-format
  3. rtl-lint-verible
  4. rtl-lint-verilator
  5. synth
  6. Create: src/abe/rad/rad_<design>/formal
  7. Templates from proven designs like rad_async_fifo can serve as a starting point.
  8. Review existing formal collateral for examples.

See also: Formal Verification Flow and Formal Coverage Flow.

Formal Verification Flow

Formal Testbench: <design>_formal_top.sv

Main parts:

  • Clock generation using $global_clock and (* gclk *) (see FAQ #6).
  • Reset sequence for each domain.
  • (* anyseq *) for free inputs.
  • assume for legal input conditions (see FAQ #7).
  • assert for invariants and safety properties.
  • $past() protected by past_valid.

Reference:

src/abe/rad/rad_async_fifo/formal/rad_async_fifo_formal_top.sv

See also: SymbiYosys Configuration.

SymbiYosys Configuration: <design>.sby

Sections:

Section Purpose
[options] Mode (prove), depth, multiclock
[engines] Solver selection (see FAQ #4)
[script] Yosys steps
[files] RTL + formal top

Reference:

rad_async_fifo/formal/rad_async_fifo.sby

See also: Running Proofs and Formal Coverage Flow.

Running Proofs

make DESIGN=<design> formal

Examine the Output Directory: out_formal/<design>

File/Directory Description
PASS Status marker file containing verification statistics and elapsed time
config.sby Copy of the .sby configuration file used for this run
engine_0/ Engine-specific outputs including trace files (.vcd, .yw) for counterexamples
logfile.txt Complete SymbiYosys log showing all steps, solver progress, and results
model/ Intermediate Yosys files including the SMT2 model and design elaboration logs
<design>.xml JUnit-style XML report of verification results
src/ Copies of all source files used in verification for reproducibility (see FAQ #8)
status Human-readable summary of verification status (basecase/induction results)
status.sqlite SQLite database with detailed status information

See also: FAQ #2 and FAQ #3.

Formal Coverage Flow

Create the Coverage Configuration: <design>_cover.sby

The coverage .sby file is almost the same as the verification configuration. The main difference is in the [options] section: use mode cover instead of mode prove (see FAQ #5). Coverage mode finds traces that meet the cover statements in your formal testbench. This is useful for:

  • Creating traces.
  • Checking reachability.
  • Finding over‑constrained assumptions.

Run:

make DESIGN=<design> formal-cover

Reference:

src/abe/rad/rad_async_fifo/formal/rad_async_fifo_cover.sby

FAQ

Why use formal if simulation passes?

Formal checks all legal input sequences. It works together with simulation testing. It can help find:

  • Underflow/overflow.
  • Race conditions.
  • Reset bugs.
  • Multi‑clock hazards.
  • Illegal input patterns.

These issues are hard to find with only simulation.

What depth should I use?

Here are some starting values:

  • Small modules: 16–40
  • FIFOs & CDC logic: 40–80
  • Handshakes: 20–50

Increase the depth if induction does not work at first.

Why doesn't induction work?

Check these common causes:

  • Reset not modeled correctly.
  • Missing assumptions.
  • $past() guard missing.
  • Real bug in the design.
  • Long initialization sequences.

Making assumptions simpler or stronger can often fix induction problems.

Which solvers should I use?

  • Boolector (recommended to start).
  • Yices or Z3 can help if Boolector does not support something.

Difference between formal and formal-cover?

Mode Meaning
prove Property must hold always
cover Scenario must be reachable

Why $global_clock?

It enables:

  • Correct multi‑clock modeling.
  • Correct SMT scheduling.
  • No need for manual clock generation.

How many assumptions are too many?

Here is a helpful guide:

Use assumptions for legal inputs, not for internal design behavior.

Why does SymbiYosys copy source files?

To make results repeatable. Each run includes everything:

  • RTL.
  • formal tops.
  • logs.
  • SMT model.

References

Licensing

See the LICENSES directory at the repository root.