@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?
-
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
Do you have the ISA formalised, if so, what formalism?That looks pretty doable. You probably want to use symbiyosys (sby) instead of calling yosys-smtbmc directly. It's a bit more "black boxy" but it really simplifies trying different solvers. (The performance difference can be huge so it definitely pays to try different things.)
-
-
so, my main question is: where do I start? do I open https://symbiyosys.readthedocs.io/en/latest/ and read through it? are there better introductory texts?
-
Just bits and pieces as of now unfortunately. Readthedocs is one bit. There are also some tutorials on https://zipcpu.com and my latest slides are at http://www.clifford.at/papers/2018/sby-formal/ …. Feedback on what kind of materials would be good for getting people started would be appreciated.
End of conversation
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.