Also: v2c uses a non-open source Verilog front-end. Yosys C back-end is back on the todo list..https://twitter.com/oe1cxw/status/768433225387634688 …
-
I looked into cprover for hardcaml BMC with LTL/CTL props. It seemed the property compilation might be the harder problem.
time will show how useful a C back-end really is for larger designs. But it certainly would be a nice addition to the toolbox.
-
-
Indeed. Interesting performance claims for SW verifiers and much research going on.
-
Applicability to HW? Dunno - the models I generate are basically levelized simulations with 1 big combinatorial update function.
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.