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 …
-
for example. You could do all sorts of things with a C model that is optimized for model checking.
maybe you already have formal models of your CPU in Verilog and C. With this you could check them for equivalence.
-
-
Interesting. Maybe you could also run a "trace" of some compiled c-code on the cpu model and check that directly against the source
-
I looked into cprover for hardcaml BMC with LTL/CTL props. It seemed the property compilation might be the harder problem.
- Show replies
New conversation -
-
-
I know a guy at Intel who wrote a C model of a large Verilog project by hand. Took him quite some time.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.