Found some other big bugs, for example the divide instruction wasn't waiting for the multiply instruction to complete before issue. (Why would any one follow a multiply immediately with a divide?--wasn't in my test bench) I added these to the list in http://zipcpu.com/blog/2018/04/02/formal-cpu-bugs.html …
-
This Tweet is unavailable.
-
I’m impressed at what you’ve done with formal verification. But don’t you quickly run into combinational explosion? eg. RISCV32IM is ~40 instructions. With sequence of 8 you have around 6.5 trillion permutations without considering pipeline or reg. Or is seq of 8 more than req?
That's why you use SAT and SMT solvers instead of iterating over all possibilities https://en.wikipedia.org/wiki/Boolean_satisfiability_problem ….
-
-
Thanks. I’m clearly going to have to get my head around this properly and try it myself. Is http://www.clifford.at/papers/2017/smtbmc-sby/slides.pdf … a good place to start?
-
I like to think so. It has some nice examples that should help get you started.
- 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.