Integrated toolchain for RISC-V processor design, verification, and optimization using DSL-based instruction constraints.
This repository integrates three components of the PDAT (Processor Design and Test) ecosystem:
- PdatDsl - Domain-Specific Language for specifying RISC-V ISA subsets
- ScorrPdat - RTL synthesis optimization and formal equivalence checking
- CoreSim - Constrained-random simulation framework with VCD-based analysis
Together, these tools enable:
- Specification of processor ISA constraints
- Automated synthesis optimization
- Simulation-based signal correspondence analysis
- Formal verification of RTL designs
- Python 3.7+
- Git with submodule support
- VCS (Synopsys) - Required for simulation
- Synlig - SystemVerilog frontend for Yosys
- ABC - Sequential logic optimization tool
- Yosys - Open-source synthesis framework
- Z3 - SMT solver (for advanced verification)
- SKY130 PDK - For gate-level synthesis
If you haven't already cloned with submodules:
git clone --recursive <repository-url> PdatScorrWrapper
cd PdatScorrWrapperIf you already cloned, initialize the submodules:
git submodule update --init --recursiveThis will initialize:
PdatDsl/- DSL parser and code generationScorrPdat/- RTL synthesis and optimizationCoreSim/- Simulation framework with Ibex core
cd PdatDsl
pip install -e .
cd ..This installs the pdat-dsl command-line tool for parsing DSL files and generating SystemVerilog constraints.
Verify installation:
pdat-dsl versioncd ScorrPdat
pip install -r requirements.txt
cd ..This installs Python dependencies for synthesis scripts and RTL analysis tools.
cd CoreSim
git submodule update --init --recursive
cd ..This initializes the Ibex core and other processor submodules required for simulation.
Note: VCS must be installed and available in your PATH for simulation.
# 1. Create or use an existing DSL specification
cd PdatDsl
cat examples/example_16reg.dsl
# 2. Run synthesis optimization with constraints
cd ../ScorrPdat
./synth_ibex_with_constraints.sh ../PdatDsl/examples/example_16reg.dsl
# 3. Run simulation (requires VCS)
cd ../CoreSim
./run_ibex_random.sh testbenches/ibex/dsls/example_16reg.dslScorrPdat provides batch processing for multiple DSL files:
cd ScorrPdat
./batch_synth.sh [options]This will process multiple DSL specifications and generate optimized RTL for each.
Create a DSL file specifying your processor's instruction constraints:
# example_spec.dsl
require RV32I
require RV32M
require_registers x0-x15
# Outlaw specific instructions
instruction DIV
instruction REMValidate the specification:
cd PdatDsl
pdat-dsl parse examples/example_spec.dslGenerate optimized RTL with instruction constraints applied:
cd ScorrPdat
./synth_ibex_with_constraints.sh ../PdatDsl/examples/example_spec.dsl --gatesOptions:
--gates- Generate gate-level netlist--3stage- Enable 3-stage pipeline mode--abc-depth N- Set k-induction depth for ABC
Output: Optimized RTLIL and optionally gate-level Verilog in output/
Generate VCD traces for signal correspondence analysis:
cd CoreSim
./run_ibex_random.sh testbenches/ibex/dsls/example_spec.dsl --constants-onlyOptions:
--flush-cycles N- NOP cycles for pipeline flush (default: 100)--random-cycles N- Random instruction cycles (default: 1000)--3stage- Enable 3-stage pipeline--constants-only- Filter to constant signals only
Output: VCD files and JSON files in output/:
ibex_reset_state.vcd- Initial stateibex_random_sim.vcd- Full traceinitial_state.json- Initial flip-flop valuessignal_correspondences.json- Equivalence classes
Use the RTL-scorr Yosys plugin (separate repository) with generated JSONs:
# Example using rtl_scorr plugin
yosys -m rtl_scorr.so -p "
read_verilog ibex_core.v
rtl_scorr output/signal_correspondences.json \
output/initial_state.json \
-apply-opt -k 2
"PdatScorrWrapper/
├── .gitmodules # Submodule configuration
├── README.md # This file
├── PdatDsl/ # DSL parser and code generation
│ ├── pdat_dsl/ # Python package
│ ├── examples/ # Example DSL files
│ └── README.md
├── ScorrPdat/ # RTL synthesis and optimization
│ ├── scripts/ # Analysis tools
│ ├── rtl_scorr/ # SMT-based verification
│ ├── synth_ibex_with_constraints.sh
│ ├── batch_synth.sh
│ └── README.md
└── CoreSim/ # Simulation framework
├── cores/ # Processor submodules (Ibex, etc.)
├── testbenches/ # VCS testbenches
├── scripts/ # Compilation and utilities
├── run_ibex_random.sh
└── README.md
- Edit DSL - Modify ISA constraints in
PdatDsl/examples/ - Synthesize - Run
./batch_synth.shin ScorrPdat - Simulate - Run
./run_ibex_random.shin CoreSim - Analyze - Inspect generated JSONs and reports
- Iterate - Refine constraints and repeat
# Create new DSL file
cd PdatDsl/examples
cat > my_custom_spec.dsl << 'EOF'
require RV32I
require_registers x0-x7
instruction MUL
instruction DIV
EOF
# Validate
pdat-dsl parse my_custom_spec.dsl
# Synthesize
cd ../../ScorrPdat
./synth_ibex_with_constraints.sh ../PdatDsl/examples/my_custom_spec.dslOverride the default Ibex core location:
export IBEX_ROOT=/path/to/custom/ibexDefault search order:
$IBEX_ROOT(if set)../PdatCoreSim/cores/ibex../CoreSim/cores/ibex
git submodule update --init --recursivecd PdatDsl
pip install -e .Ensure VCS is installed and in your PATH:
which vcsInstall Synlig and ABC according to their respective documentation.
This project is licensed under the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License (CC BY-NC-SA 4.0).
- Non-commercial use: Free to use, modify, and share under the ShareAlike terms
- Commercial use: Contact Nathan Bleier (nbleier@umich.edu) for commercial licensing options
See individual submodule LICENSE files for details.
- RtlScorr - Yosys plugin for formal signal correspondence verification
- Ibex Core - lowRISC's 2-stage/3-stage RV32IMC processor
Contributions are welcome! Please see individual submodule repositories for contribution guidelines.
For questions or commercial licensing:
- Nathan Bleier - nbleier@umich.edu