@oe1cxw so, I made a nice and simple CPU today, now I want to formally verify it.
is there some introductory material for SymbiYosys that explains how to verify nontrivial designs?
-
my own ISA, and fully verify. it is not pipelined right now, purely FSM-driven--I want more assurance than a few unit tests before migrating to a more complex design (if ever).
You could go the riscv-formal route and create a verification trace port. See for example this slides: http://www.clifford.at/papers/2018/riscv-formal/ ….
