I managed to get Yosys formal verification working with Clash circuits! behold, verification of a counter :) https://gist.github.com/thoughtpolice/f339e8aa55dbf2dd4f2ba63fa517410f#file-counter-hs …
Show this thread
-
(note that this previously wasn't possible, due to the fact Clash didn't support synchronous resets before recently)
Show this thread
Yosys can be used to verify asynchronous resets and multiple clock domains as well JFYI. :)
-
-
not surprising I'd mess it up :) -- last time I tried it I believe I got myself stuck since it didn't know what to do with an
$adff cell -
been meaning to test out the multiple clock domain stuff too but I'm slowly working through the Symbiyosys docs/your slides, essentially :P
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.