@oe1cxw I'm trying to use smtbmc and I've deliberately created false asserts, but the model checker still passes 
Am I doing something very stupid?
https://gist.github.com/GuzTech/9c162d1a01ef5f5344f966ed7ed6d9da …
-
Your initial assignment for ptr_m is conflicting with it's continuous assignment. Remove the initial assignment for ptr_m. (You should use "smtbmc --presat" to check if your (explicit and implicit) assumptions are contradicting. I might make this the default.)
Also: When you want to model clocks explicitly then you'll need to run "clk2fflogic" after prep. Otherwise all flops will automatically be driven by "$global_clock", not the event in the always clause.
-
-
Thank you! Yes, that initial assignment to ptr_m was an accident. After removing it, it immediately failed on me so that's good. I'm trying to follow along with the blog post of
@zipcpu but of course I didn't check his Makefile
http://zipcpu.com/blog/2017/10/19/formal-intro.html … -
He also has clk2fflogic and the --presat option. I guess I'm trying to do too much at once, so let me check simple things first, and then add the clock assumptions and assertions. I've got a lot to learn
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.