Case studies

Short, concrete case studies that show what I built, how I approached it, and what evidence exists.

Floating-point formal verification

Case study (formal verification) A scalable floating-point verification workflow using RTL-to-RTL model checking against a golden reference, structured into staged helper assertions to make proofs converge. Focus: proof structure · helper lemmas · counterexample-guided refinement Domains: floating-point · arithmetic · correctness-critical blocks Stack: SystemVerilog · SVA · formal tooling · Python automation Problem Floating-point units are correctness-critical and difficult to cover comprehensively with simulation alone. Formal proofs often fail without a disciplined decomposition strategy. ...

RISC-V “Kreacher”

Case study (RTL + integration) A collaborative RISC-V processor integrated into a SoC environment, with contributions focused on datapath correctness and clean integration interfaces. Scope: datapath modules · integration boundaries · correctness discipline Stack: SystemVerilog · RTL integration workflow Note: code is not public (team project) Problem SoC integration requires stable interfaces, disciplined block boundaries, and correctness-first implementation to avoid late-stage integration regressions. Approach Implemented datapath modules including ALU and decoder Focused on functional accuracy and clean integration Kept interfaces predictable for SoC-level bring-up Evidence Work product exists as team integration deliverables (code not public). I can share details that are safe to discuss. ...

SaxoFlow

Case study (open-source tooling) SaxoFlow is an evidence-first design + verification workflow that combines open-source EDA tools with GenAI-assisted generation and iteration loops—built to make learning and prototyping faster and more systematic. Focus: verification workflow automation + reproducibility Stack: Python · SystemVerilog · SVA · open-source EDA ecosystem Artifacts: CLI flows · agent-assisted generation · logs/evidence trail Problem Digital design and verification iteration is slowed down by environment setup, tool fragmentation, and repeated manual loops (install → run → debug → re-run). ...