Open Source Formal Verification in VHDL
summary
GHDL now synthesizes VHDL into Yosys via a GHDL→Yosys plugin and supports PSL in VHDL‑2008 so SymbiYosys can run SMT solvers on designs. A hand‑built bit‑serial CPU ALU is synthesized (targeted to 74 chips, currently running on an FPGA) and formally verified; verification finds an off‑by‑one carry bug when opcode changes just before reset. Fixes: make carry combinatorial or require opcode stable before reset. Docker images provided.
AI-written summary · about
chapters (5)
related talks
21mOpen Source Digital Design Tooling Updates
30mMicrowatt and GHDL - An Open Hardware CPU written in VHDL...
23mUnlocking Open Source RISC-V SoC Verification
30mOSVVM: Methodology, Library, and Models
18mGiving Students A Byte of Open-Source: Advancing Hardware Education
07mFPGA and open hardware
26mLessons learned while formally verifying the ZipCPU
18mOpen source chip design: for fun and for profit