| *** tpb <[email protected]> has joined #yosys | 00:00 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has quit IRC (Remote host closed the connection) | 00:19 | |
| *** danderson <danderson!~dave@tailscale/danderson> has joined #yosys | 02:04 | |
| *** ats <ats!~ats@2001:8b0:83b:b53f::a> has quit IRC (Ping timeout: 248 seconds) | 02:17 | |
| *** ats <[email protected]> has joined #yosys | 02:18 | |
| *** kraiskil <[email protected]> has quit IRC (Ping timeout: 244 seconds) | 06:15 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has joined #yosys | 06:50 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has quit IRC (Remote host closed the connection) | 07:06 | |
| *** mbgreyhat <[email protected]> has joined #yosys | 07:16 | |
| *** anticw <[email protected]> has quit IRC (Ping timeout: 252 seconds) | 07:57 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has quit IRC (Read error: Connection reset by peer) | 08:02 | |
| *** kristianpaul <kristianpaul!~paul@user/kristianpaul> has joined #yosys | 08:03 | |
| *** anticw <[email protected]> has joined #yosys | 10:03 | |
| *** mbgreyhat <[email protected]> has quit IRC (Remote host closed the connection) | 10:43 | |
| *** Adrien[m] <Adrien[m]!adrienpbma@2a01:4f8:c012:5b7:0:1:0:7e> has quit IRC (Quit: Idle timeout reached: 172800s) | 14:57 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has joined #yosys | 17:27 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has quit IRC (Client Quit) | 17:27 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has joined #yosys | 17:30 | |
| mkudinov | Hi guys. I started learning formal verification and I have a question about sby. | 17:36 |
|---|---|---|
| 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... | 17:36 |
| mkudinov | Thanks for any help! | 17:36 |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has quit IRC (Quit: Client closed) | 17:37 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has joined #yosys | 17:37 | |
| 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 | 17:40 |
| 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 | 17:41 |
| jix | an induction counterexample doesn't have to start in reset, but can start in any state that satisfies the assumptions and assertions | 17:42 |
| 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 | 17:43 |
| 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? | 17:43 |
| jix | yeah, you can use the engine "abc pdr" for that | 17:45 |
| 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 | 17:45 |
| jix | yeah that's required for induction | 17:45 |
| mkudinov | Alright, thanks for the help! | 17:45 |
| 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 | 17:46 |
| 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 | 17:47 |
| jix | but for that it essentially slides the induction part across the state, so it can't be fixed to start in reset | 17:47 |
| mkudinov | Hmmm, interesting! So this is why I got pass for basecase, but fail for induction. | 17:53 |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has quit IRC (Ping timeout: 240 seconds) | 18:22 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has joined #yosys | 18:40 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has quit IRC (Remote host closed the connection) | 18:43 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has joined #yosys | 19:41 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has quit IRC (Quit: Client closed) | 20:10 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has joined #yosys | 20:11 | |
| *** mkudinov <mkudinov!~mkudinov@2a02:2168:a06:5758::1> has quit IRC (Quit: Client closed) | 20:26 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has joined #yosys | 20:44 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has quit IRC (Remote host closed the connection) | 20:47 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has joined #yosys | 20:49 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has quit IRC (Remote host closed the connection) | 21:00 | |
| *** nonchip <[email protected]> has quit IRC (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) | 22:07 | |
| *** nonchip <[email protected]> has joined #yosys | 22:07 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has joined #yosys | 22:54 | |
| *** hwpplayer1 <hwpplayer1!~user@user/hwpplayer1> has quit IRC (Remote host closed the connection) | 22:56 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!