@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 …
-
I just call it with "sby -f stack.sby". The funny thing is that it did work before, and that it does read the file. For example, if I make a mistake, it will point it out. That's why I deliberately put assert(0) in there among other false assertions.
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 … - 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.