@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?
Is it using your own ISA? Do you want to fully verify the CPU against an ISA spec or just some "sanity check" safety properties such as correct handling of pipeline hazards?
-
-
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/ ….
End of conversation
New conversation -
-
-
Forgive me if I am butting in or being patronising but +1 what they ^^^ said : what do you want to verify about it? Verification needs a system and a specification.
-
I want to verify that for any valid sequence of instructions, the observable behavior of CPU (i.e. internal memory writes, and external bus reads/writes) matches what is required by the ISA
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.