| *** tpb has joined #yosys | 00:00 | |
| *** citypw has joined #yosys | 01:30 | |
| *** SpaceCoaster has joined #yosys | 01:44 | |
| *** Degi has quit IRC | 03:30 | |
| *** Degi has joined #yosys | 03:30 | |
| *** LJ_cache has joined #yosys | 03:59 | |
| *** az0re has quit IRC | 04:07 | |
| *** LJ_cache has quit IRC | 05:06 | |
| *** nobodywasishere has quit IRC | 05:11 | |
| *** az0re has joined #yosys | 05:49 | |
| *** proteusguy has quit IRC | 05:54 | |
| *** proteusguy has joined #yosys | 06:07 | |
| *** elGamal has quit IRC | 06:20 | |
| *** elGamal has joined #yosys | 06:22 | |
| *** Asu has joined #yosys | 06:22 | |
| *** _whitelogger has quit IRC | 08:09 | |
| *** _whitelogger has joined #yosys | 08:11 | |
| *** X-Scale` has joined #yosys | 08:58 | |
| *** X-Scale has quit IRC | 08:59 | |
| *** X-Scale` is now known as X-Scale | 08:59 | |
| *** elGamal has quit IRC | 09:56 | |
| *** elGamal has joined #yosys | 09:57 | |
| *** jakobwenzel has joined #yosys | 10:57 | |
| *** cr1901_modern has quit IRC | 13:06 | |
| *** cr1901_modern has joined #yosys | 13:07 | |
| *** cr1901_modern has quit IRC | 13:12 | |
| *** cr1901_modern has joined #yosys | 13:13 | |
| *** AdamHorden has quit IRC | 13:15 | |
| *** X-Scale` has joined #yosys | 13:19 | |
| *** AdamHorden has joined #yosys | 13:20 | |
| *** X-Scale has quit IRC | 13:21 | |
| *** X-Scale` is now known as X-Scale | 13:21 | |
| *** gtw has quit IRC | 13:34 | |
| *** AdamHorden has quit IRC | 13:38 | |
| *** AdamHorden has joined #yosys | 13:52 | |
| *** jakobwenzel has quit IRC | 13:56 | |
| *** jakobwenzel has joined #yosys | 13:56 | |
| thardin | does sign extension happen when extracting bits from a signed wire into another signed wire? | 14:43 |
|---|---|---|
| *** emeb has joined #yosys | 14:44 | |
| thardin | nm, I'll use an arithmetic shift instead | 14:46 |
| *** cr1901_modern has quit IRC | 15:15 | |
| *** cr1901_modern has joined #yosys | 15:16 | |
| *** LJ_cache has joined #yosys | 16:20 | |
| DaKnig | thardin: in what lang? | 16:23 |
| *** cr1901_modern has quit IRC | 16:27 | |
| *** cr1901_modern has joined #yosys | 16:27 | |
| thardin | verilog | 16:35 |
| *** citypw has quit IRC | 16:45 | |
| z0ttel | If an equivalence check passes for the outputs, but fails for some intermediate wires, can I assume that the (entirely combinatorial) modules implement the same functions? | 17:01 |
| Lofty | z0ttel: depends on which equivalence checking method you're using, but yes | 17:06 |
| Lofty | equiv_induct has a different definition of "equivalent" than sat or equiv_simple, AIUI | 17:06 |
| z0ttel | equiv_simple and equiv_struct yield the same result. Is equiv_induct any use for combinatorial circuits? Shouldn't have any temporally relevant behaviour. | 17:08 |
| az0re | Should be the same, then | 17:08 |
| z0ttel | okay, cool, thx :) | 17:09 |
| Lofty | z0ttel: sure equiv_induct is useful for combinatorial circuits; it's *way* faster | 17:13 |
| z0ttel | equiv_induct can't prove the base case, circuit inherently diverges! | 17:19 |
| Lofty | That's...generally an indication these are *not* equivalent | 17:20 |
| z0ttel | Mh, can I make yosys show me a counterexample? | 17:34 |
| Lofty | Uh, the `sat` command will do that, at least | 17:35 |
| Lofty | I don't think equiv_induct has enough information for that | 17:35 |
| Lofty | But `miter` followed by `sat -prove-asserts` would give a counterexample, I think. | 17:36 |
| DaKnig | would it try to minimize the example? | 17:40 |
| az0re | Err hang on a second. How is it possible for the same combinational circuit to fail equiv_induct but pass equiv_struct? | 17:43 |
| az0re | My mental model must be wrong | 17:43 |
| z0ttel | miter -equiv gold gate miter; hierarchy -top miter; flatten; sat -prove-asserts <- that gives me a "proof finished, no models found" QED. | 17:48 |
| z0ttel | az0re: it did report some failing equivalences on internal wires after equiv_struct... | 17:58 |
| z0ttel | The backend I get internal wiring from enumerates wires differently for the two structures I compare, so it makes sense for some of the wires to be shuffled between the two. | 18:00 |
| z0ttel | Also, I'm using debian stable with default packaged yosys, so it may just be an ancient version doing ancient things. | 18:00 |
| *** cr1901_modern has quit IRC | 18:29 | |
| az0re | Yes, sure I understand they are structurally different. But as that command shows, they are functionally equivalent at the PIs/POs. I guess my question is better stated: How can it be that these two combinational circuits are equivalent yet `equiv_induct` fails? | 18:44 |
| *** oldtopman has quit IRC | 19:40 | |
| *** oldtopman has joined #yosys | 19:40 | |
| *** Asu has quit IRC | 22:03 | |
| *** strobokopp has joined #yosys | 22:48 | |
| *** az0re has quit IRC | 22:59 | |
| *** cr1901_modern has joined #yosys | 23:05 | |
| *** lf has quit IRC | 23:39 | |
| *** emeb has quit IRC | 23:39 | |
| *** lf has joined #yosys | 23:40 | |
Generated by irclog2html.py 2.17.2 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!