Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

@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?

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

(general-purpose registers, code and data are all in the same BRAM, and PC/flags are observable via instructions, so that should be sufficient)

If wish my clients were this prompt and direct Do you have the ISA formalised, if so, what formalism?

I don't! I've never worked with formal verification of gateware before (ok, I ran a few trivial tests with yosys-smtbmc, but that's it) and I want to learn it. The ISA is really straightforward (https://github.com/whitequark/Glasgow/blob/master/software/glasgow/arch/boneless/__init__.py#L131-L257 …) so I imagine formalizing it can't be *that* hard