hwpplayer1 has quit [Remote host closed the connection]
danderson has joined #yosys
ats has quit [Ping timeout: 248 seconds]
ats has joined #yosys
kraiskil has quit [Ping timeout: 244 seconds]
hwpplayer1 has joined #yosys
hwpplayer1 has quit [Remote host closed the connection]
mbgreyhat has joined #yosys
anticw has quit [Ping timeout: 252 seconds]
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
anticw has joined #yosys
mbgreyhat has quit [Remote host closed the connection]
Adrien[m] has quit [Quit: Idle timeout reached: 172800s]
mkudinov has joined #yosys
mkudinov has quit [Client Quit]
mkudinov has joined #yosys
<mkudinov>
Hi guys. I started learning formal verification and I have a question about sby.
<mkudinov>
What's the difference between bmc and prove modes? It say in the docs that the first is bounded model check, while the other is unbounded, but I'm still clueless what it's supposed to mean. In bmc my asserts are passing, but in prove I get a fail for induction. In counterexample wave it seems like my `assume`s were ignored...
<mkudinov>
Thanks for any help!
mkudinov has quit [Quit: Client closed]
mkudinov has joined #yosys
<jix>
mkudinov: BMC checks that the properties hold for a certain number of steps after reset (the depth option in SBY) and prove tries to check that the properties will hold forever
<jix>
for an engine that uses k-induction in prove mode, like smtbmc, induction can fail even if the property does hold, the overall result will then be UNKNOWN
<jix>
an induction counterexample doesn't have to start in reset, but can start in any state that satisfies the assumptions and assertions
<jix>
if induction fails but the property is true, the coutnerexample trace must start in a state that's actually unreachable, and the way to make it pass induction is to add an assertion that holds and excludes that initial state
<mkudinov>
jix Thanks! Now everything's clear. The failure was indeed with smtbmc. What engine can I use to check that it was false negative? Abc would do?
<jix>
yeah, you can use the engine "abc pdr" for that
<mkudinov>
All my counterexamples should start with reset, because I have `initial assume(rst)`, though prove counterexample started without reset with random values in registers
<jix>
yeah that's required for induction
<mkudinov>
Alright, thanks for the help!
<jix>
k-induction works this way: you check that the properties hold in the first k steps after reset, and you check separately that if the propeties hold for k steps in a row they must also hold for one additional step
<jix>
and the second part, the induction step, allows you to extend the base case, the first k steps indefinitely, i.e. it shows that the properties hold forever
<jix>
but for that it essentially slides the induction part across the state, so it can't be fixed to start in reset
<mkudinov>
Hmmm, interesting! So this is why I got pass for basecase, but fail for induction.
mkudinov has quit [Ping timeout: 240 seconds]
hwpplayer1 has joined #yosys
hwpplayer1 has quit [Remote host closed the connection]
mkudinov has joined #yosys
mkudinov has quit [Quit: Client closed]
mkudinov has joined #yosys
mkudinov has quit [Quit: Client closed]
hwpplayer1 has joined #yosys
hwpplayer1 has quit [Remote host closed the connection]
hwpplayer1 has joined #yosys
hwpplayer1 has quit [Remote host closed the connection]