Introduction to Formal Verification with Symbiotic EDA Open Source Tools
summary
Overview of using Symbiotic EDA open source flow with SymbiYosys (sby), PySMT and SMT/SAT solvers (yices default, Z3, Boolector) to write asserts/assumes and get concrete counterexamples and covers. Demonstrations include a 3-stage pipeline on a single-ported memory (real design has 10 stages, 40 instructions), a bus/peripheral check that finds an uninitialized counter bug, a wolf‑goat‑cabbage cover found in 8 steps, and proofs requiring k‑induction with default depth 20.
AI-written summary · about
chapters (10)
- 0:00Intro
- 1:40What is Formal Verification
- 5:33Formal Verification with solvers
- 7:50Cover
- 11:44Bounded Model Check
- 15:29Busy Counter
- 20:19Double Shift Register
- 22:09Induction Step
- 25:14Induction Exercise
- 40:51Induction Workflow
related talks
21mCombined Dynamic and Formal Verification Approach to Processor Verification
25mFormally Verifying AXI Interfaces
18mSMT2Test: From SMT Formulas to Effective Test Cases
21mValidating SMT Solvers for Correctness and Performance via Grammar-based Enumeration
18mMore than the Core Verifying RISC V SoCs
18mPreview: Verification (Correctness)
17mDesign for Hardware Memory Model Verification
25mRISC-V System-level Certification from Verification Foundations