Memory controller formal verification
Formal Verification Manager
FVM is a unified CLI tool for formal verification of memory controller designs. Pre-built SVA libraries for DDR4, DDR5, and CXL-MEM 3.0 with support for Jasper, Questa, and VC Formal.
What It Does
Complete formal verification workflow
Memory controller designs are complex and hard to verify. FVM solves this with pre-built SVA libraries, a unified multi-tool interface, deterministic code generation, and JEDEC timing integration.
- Pre-built SVA libraries — 6 for DDR4, 9 for DDR5, ready to integrate
- Unified multi-tool interface — One CLI for Jasper, Questa, and VC Formal
- Deterministic code generation — Byte-identical output verified by CI
- JEDEC integration — Timing from specs, overridable per-project
- Exhaustive verification — Pure formal checking, no simulation
Traditional approach: Manual assertions + tool-specific interfaces → slow, error-prone
FVM approach: Pre-built libraries + unified interface + code generation → fast, reliable, repeatable
Core Features
Built for precision and scale
📚 SVA Libraries
Complete, pre-written assertions for DDR4 timing, protocol, power, init, and training. DDR5 extends with ECC and dual-channel support.
🔧 Multi-Tool Support
Abstracts Cadence Jasper, Siemens Questa, and Synopsys VC Formal through a single unified CLI interface.
⚙️ Code Generation
Jinja2-templated assertion generation with deterministic, idempotent output verified by 48 CI drift tests.
⏱️ JEDEC Integration
Timing parameters sourced from JEDEC specs with per-project overrides. Invariant checking at generation time.
✓ CXL-MEM 3.0
Derives DDR5 timing database with CXL link-latency offsets and enforces fixed CXL structure constraints.
🐍 Python-First
Rich CLI built with Click, pydantic config models, easy integration into design automation pipelines.
SVA Libraries
What they verify
DDR4 (6 Libraries)
| Library | Verifies |
|---|---|
ddr4_timing.sv |
tRCD, tRAS, tRP, tRC timing constraints |
ddr4_protocol.sv |
Bank state machine, command validity |
ddr4_cmd_sequence.sv |
State transitions, MR programming order |
ddr4_power.sv |
Power state management |
ddr4_init.sv |
Initialization sequence correctness |
ddr4_training.sv |
Training phase constraints |
DDR5 Extensions (9 Total)
DDR5 adds 3 new libraries:
| New Library | Purpose |
|---|---|
ddr5_cmd_sequence_assumptions.sv |
Constrain DUT to valid DDR5 command sequences |
ddr5_ecc.sv |
On-die ECC: tECC latency, scrub protocol |
ddr5_dual_channel.sv |
2×32-bit independent channels per DIMM |
Plus DDR5-specific enhancements: same-bank refresh (REFsb), separate read/write CCD, read-to-write turnaround (tRTW), Multi-Purpose Command (MPC), and MRS programming order.
Architecture
Three-layer design
Layer 1: C++17 Core
SVA Parser — Parse and validate SystemVerilog assertions
Bind Generator — Create bind statements to attach assertions to RTL
Timing Model — JEDEC timing parameter validation
Layer 2: Python Orchestration
CLI (Click) — User-facing commands and interface
Tool Adapters — Subprocess interface to formal engines
DDR Knowledge Base — JEDEC specs and per-project overrides
Layer 3: SVA Libraries
Pre-built assertions for DDR4, DDR5, CXL-MEM, plus common building blocks (handshake, FIFO)
Testing
Comprehensive test coverage
Test Breakdown
- 538+ pytest functions total
- 109 SVA structural tests
- 48 generator drift tests (byte-identical output verification)
- C++ test suite for core functionality
CI Pipeline
| Job | Purpose | Timeout |
|---|---|---|
| Lint | Code quality checks | 5 min |
| Python Tests | Python 3.11 & 3.12 | 12 min each |
| SVA Tests | SVA library structural validation | 8 min |
| Gen Drift | Generator consistency | 5 min |
| C++ Tests | Core functionality | 10 min |
| Full Suite | All tests combined | 20 min |
Key Invariant: fvm gen-lib output is
byte-identical across runs. Generator drift tests fail if generated
files diverge from committed libraries.
Project Status
Complete and production-ready
✅ Complete
- DDR4 SVA libraries (6) — hand-tested
- DDR5 SVA libraries (9) — 517 tests
- Multi-tool support (Jasper, Questa, VC Formal)
- Python CLI orchestration
- C++ parser and bind generator
🚧 In Progress
- CXL-MEM 3.0 demo and integration
📋 Planned
- CXL-IO 3.0 (TLP transaction layer)
- Web dashboard UI
- Extended tool support