RtlScorr - RTL Signal Correspondence Yosys Plugin

A Yosys plugin for formal verification of signal equivalences using SMT-based k-induction with incremental solving.

Overview

RtlScorr proves that signals in RTL designs are constant or equivalent under given constraints. It reads simulation-based equivalence candidates (from CoreSim) and formally verifies them using:

• K-induction - Unbounded verification (not just bounded model checking)
• Circuit unrolling - Converts sequential to combinational for k steps
• Z3 C++ API - Incremental SMT solving with learned clauses
• Cone extraction - Reduces model size by 95%+ for scalability
• Assumption-aware - Respects DSL constraints during verification

Installation

Prerequisites

# Synlig (SystemVerilog frontend for Yosys)
# Build from: https://github.com/chipsalliance/synlig

# Z3 SMT Solver (development libraries)
sudo apt install libz3-dev

# C++17 compiler
sudo apt install g++

Build Plugin

cd yosys_plugin
make synlig  # For Synlig with SystemVerilog support
# or
make         # For standard Yosys

This creates write_smt2_assumptions_synlig.so (or write_smt2_assumptions.so)

Usage

With CoreSim-Generated JSONs

# 1. Generate VCDs and JSONs with CoreSim
cd ../CoreSim
./run_ibex_random.sh testbenches/ibex/dsls/my_spec.dsl --constants-only

# 2. Run RtlScorr verification
cd ../RtlScorr
synlig -p "
  plugin -i yosys_plugin/write_smt2_assumptions_synlig.so
  read_systemverilog design.sv
  hierarchy -top my_module
  proc; async2sync; dffunmap; flatten

  rtl_scorr ../CoreSim/output/signal_correspondences_constants.json \\
            ../CoreSim/output/initial_state.json \\
            -k 2 -output report.txt
"

Command-Line Options

rtl_scorr <equiv_classes.json> <initial_state.json> [OPTIONS]

Required:
  equiv_classes.json   - Equivalence candidates (from CoreSim)
  initial_state.json   - Initial register values (from CoreSim)

Options:
  -k N                 - K-induction depth (default: 2, match pipeline depth)
  -smt-timeout N       - Timeout per query in seconds (default: 30)
  -max-cone N          - Skip if cone > N cells (default: 10000)
  -apply-opt           - Apply proven equivalences to design
  -output FILE         - Write results to file
  -v                   - Verbose output
  -report-only         - Only generate report, don't modify design

Project Structure

RtlScorr/
├── yosys_plugin/
│   ├── src/                    # C++ source code
│   │   ├── rtl_scorr.cc       # Main plugin logic
│   │   ├── smt_verifier.cc    # Z3-based verification
│   │   ├── incremental_solver_z3.cc
│   │   └── signal_correspondence_worker.cc
│   ├── examples/              # Example workflows
│   │   └── *.sh              # Demo scripts
│   ├── Makefile
│   └── README.md
├── inputs/                    # Example JSON files for testing
│   ├── signal_correspondences_constants.json
│   └── initial_state.json
└── requirements.txt

Example Workflow

# Complete flow from DSL to proven equivalences:

# 1. Create DSL specification
cd ../PdatDsl
pdat-dsl parse my_spec.dsl

# 2. Run constrained-random simulation
cd ../CoreSim
./run_ibex_random.sh testbenches/ibex/dsls/my_spec.dsl --constants-only

# 3. Formal verification with RtlScorr
cd ../RtlScorr
./yosys_plugin/test_json_loading.sh 2  # k=2 for 2-stage pipeline

# Results in output/report showing PROVEN/DISPROVEN for each signal

Dependencies

External Projects

• PdatDsl - For DSL examples (optional)
• CoreSim - Generates input JSONs for verification
• ScorrPdat - Synthesis tools (optional)

System Requirements

• Synlig or Yosys - RTL frontend
• Z3 - SMT solver (C++ library)
• GCC/Clang - C++17 compiler

Key Features

Incremental SMT Solving

• Reuses Z3 solver context across multiple queries
• Learns from previous proofs
• 10-100x speedup vs naive approach

Assumption-Aware Cone Extraction

• Stops at assumption-constrained signals
• Dramatically reduces model size
• Enables verification of large designs (e.g., Ibex ~10K cells)

K-Induction

• Proves properties hold for all time
• Not limited to bounded depths
• Depth should match pipeline depth for best results

License

CC-BY-NC-SA-4.0 - Copyright 2025 Nathan Bleier (nbleier@umich.edu)

Free for non-commercial use. Contact for commercial licensing.

Related Projects

• PdatDsl - ISA subset specification DSL
• CoreSim - Generates VCDs and JSON files
• ScorrPdat - RTL synthesis and analysis tools