| *** tpb has joined #yosys | 00:00 | |
| *** lf has quit IRC | 00:35 | |
| *** lf_ has joined #yosys | 00:35 | |
| *** kristianpaul has quit IRC | 00:56 | |
| *** kristianpaul has joined #yosys | 00:57 | |
| *** cr1901_modern has quit IRC | 01:15 | |
| *** cr1901_modern has joined #yosys | 01:17 | |
| *** lf has joined #yosys | 02:07 | |
| *** lf_ has quit IRC | 02:08 | |
| *** Degi has quit IRC | 02:11 | |
| *** Degi has joined #yosys | 02:13 | |
| *** kristianpaul has quit IRC | 02:45 | |
| *** kristianpaul has joined #yosys | 02:45 | |
| *** az0re has quit IRC | 04:19 | |
| *** az0re has joined #yosys | 04:55 | |
| *** az0re has quit IRC | 04:55 | |
| *** az0re has joined #yosys | 05:45 | |
| *** emeb_mac has quit IRC | 06:52 | |
| *** citypw has joined #yosys | 06:56 | |
| *** Asu has joined #yosys | 07:30 | |
| *** indy has quit IRC | 08:31 | |
| *** indy has joined #yosys | 08:36 | |
| *** jakobwenzel has joined #yosys | 09:06 | |
| *** cr1901_modern has quit IRC | 09:11 | |
| *** miek has quit IRC | 09:16 | |
| *** jordigw has quit IRC | 09:16 | |
| *** miek has joined #yosys | 09:29 | |
| *** jordigw has joined #yosys | 09:31 | |
| *** citypw has quit IRC | 10:09 | |
| *** vidbina has joined #yosys | 10:31 | |
| *** cr1901_modern has joined #yosys | 10:32 | |
| *** jakobwenzel has quit IRC | 10:39 | |
| *** jakobwenzel has joined #yosys | 10:42 | |
| *** vidbina has quit IRC | 11:10 | |
| *** jakobwenzel has quit IRC | 11:28 | |
| *** vidbina has joined #yosys | 12:32 | |
| *** kristianpaul has quit IRC | 13:01 | |
| *** kristianpaul has joined #yosys | 13:07 | |
| *** jakobwenzel has joined #yosys | 13:52 | |
| *** citypw has joined #yosys | 14:17 | |
| *** citypw has joined #yosys | 14:18 | |
| *** emeb has joined #yosys | 15:32 | |
| *** jakobwenzel has joined #yosys | 15:55 | |
| *** jakobwenzel has quit IRC | 16:49 | |
| *** citypw has quit IRC | 16:52 | |
| *** jakobwenzel has joined #yosys | 16:57 | |
| *** ayazar1 has joined #yosys | 17:30 | |
| *** vidbina has quit IRC | 17:34 | |
| *** ayazar1 has quit IRC | 18:40 | |
| *** dys has quit IRC | 20:01 | |
| *** dys has joined #yosys | 20:02 | |
| *** N2TOH_ has joined #yosys | 20:05 | |
| *** N2TOH has quit IRC | 20:09 | |
| *** emeb_mac has joined #yosys | 20:39 | |
| *** kristianpaul has quit IRC | 20:49 | |
| *** kristianpaul has joined #yosys | 20:55 | |
| *** jakobwenzel has quit IRC | 21:12 | |
| *** sorear has quit IRC | 21:13 | |
| *** sorear has joined #yosys | 21:14 | |
| cr1901_modern | Before I spend hours reading the source: how is the implementation of the equiv_induct command different from running yosys-smtbmc in induction mode and delegating to an external SMT solver? | 21:53 |
|---|---|---|
| *** alexhw has quit IRC | 21:54 | |
| daveshah | My understanding is that it does some name based matching of registers to help the proof | 21:54 |
| cr1901_modern | yosys doesn't have a built in SMT solver (?) but it does have minisat; is equiv_induct using minisat to run the proof instead? | 21:55 |
| daveshah | Yes | 21:55 |
| daveshah | No SMT involved | 21:55 |
| mwk | equiv_induct does not do register matching; the wrapper equiv_opt pass does | 21:56 |
| mwk | equiv_induct requires you to already have preexisting $equiv cells | 21:56 |
| cr1901_modern | equiv_opt was the pass I was looking at, but I wanted to see how equiv_induct works first | 21:56 |
| cr1901_modern | Anyways, nothing wrong with using SAT of course, other than "I won't be able to follow how the pass works without SMT niceties" :P | 21:57 |
| daveshah | I think you could use something like equiv_miter with write_smt2 if you wanted | 21:59 |
| daveshah | But its not a route I've personally tried | 21:59 |
| cr1901_modern | hmmm | 22:02 |
| *** indy has quit IRC | 22:07 | |
| *** Asu has quit IRC | 22:17 | |
| *** indy has joined #yosys | 22:19 | |
| cr1901_modern | So, afaict "miter -equiv" annotates two modules with the same ports with XOR gates on the outputs, and equiv_miter does something analogous with existing $equiv cells in the design? | 22:38 |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!