Formal Verification and Optimization of a Ring-Oscillator Design for a RISC-V Microcontroller
Course: ECE 584 - Fall 2026 (UIUC)
Author: Dev Patel
Links: GitHub Repository
This project involved the design, optimization, and formal verification of an Adaptive Clock Generator (ACG) for W.H.I.P.P.E.T., a low-power RISC-V processor using Dynamic Voltage and Frequency Scaling (DVFS).
The Challenge
Traditional analog design relying on manual SPICE simulations fail to guarantee area optimality and cannot exhaustively verify asynchronous timing hazards like "runt pulses" in clock generators.
Technical Methodology
- SMT Optimization: Utilized Z3 (Python) to formulate a Satisfiability Modulo Theories problem, finding the provably optimal inverter-chain configuration for three distinct DVFS modes.
- Formal Model Checking: Employed NuXMV to exhaustively verify the RTL selection logic across ∼1017 states, proving the absence of glitches during clock switching.
- Mixed-Signal Validation: Bridged the analog-digital gap by validating final configurations in Cadence Virtuoso ADE to ensure real-world viability.
Formal Specifications
To ensure robustness, the design was verified against critical CTL (Computation Tree Logic) properties.
AG (req -> AF ack)
SPEC AG ! (glitch_detected)
Using NuXMV, we verified the RTL selection logic against 12 critical properties related to liveness, safety, and glitch-freedom, ensuring that clock switching does not introduce metastable states or runt pulses.
Key Results
Achieved target frequencies (4MHz, 1MHz, 0.25MHz) with high accuracy after accounting for silicon parasitics.