nobodywasishere has quit [Read error: Connection reset by peer]
az0re has joined #yosys
proteusguy has quit [Ping timeout: 240 seconds]
proteusguy has joined #yosys
elGamal has quit [Max SendQ exceeded]
elGamal has joined #yosys
Asu has joined #yosys
_whitelogger has joined #yosys
X-Scale` has joined #yosys
X-Scale has quit [Ping timeout: 240 seconds]
X-Scale` is now known as X-Scale
elGamal has quit [Max SendQ exceeded]
elGamal has joined #yosys
jakobwenzel has joined #yosys
cr1901_modern has quit [Quit: Leaving.]
cr1901_modern has joined #yosys
cr1901_modern has quit [Quit: Leaving.]
cr1901_modern has joined #yosys
AdamHorden has quit [Ping timeout: 256 seconds]
X-Scale` has joined #yosys
AdamHorden has joined #yosys
X-Scale has quit [Ping timeout: 256 seconds]
X-Scale` is now known as X-Scale
gtw has quit [Ping timeout: 256 seconds]
AdamHorden has quit [Ping timeout: 264 seconds]
AdamHorden has joined #yosys
jakobwenzel has quit [Ping timeout: 240 seconds]
jakobwenzel has joined #yosys
<thardin>
does sign extension happen when extracting bits from a signed wire into another signed wire?
emeb has joined #yosys
<thardin>
nm, I'll use an arithmetic shift instead
cr1901_modern has quit [Quit: Leaving.]
cr1901_modern has joined #yosys
LJ_cache has joined #yosys
<DaKnig>
thardin: in what lang?
cr1901_modern has quit [Quit: Leaving.]
cr1901_modern has joined #yosys
<thardin>
verilog
citypw has quit [Ping timeout: 240 seconds]
<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?
<Lofty>
z0ttel: depends on which equivalence checking method you're using, but yes
<Lofty>
equiv_induct has a different definition of "equivalent" than sat or equiv_simple, AIUI
<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.
<az0re>
Should be the same, then
<z0ttel>
okay, cool, thx :)
<Lofty>
z0ttel: sure equiv_induct is useful for combinatorial circuits; it's *way* faster
<z0ttel>
equiv_induct can't prove the base case, circuit inherently diverges!
<Lofty>
That's...generally an indication these are *not* equivalent
<z0ttel>
Mh, can I make yosys show me a counterexample?
<Lofty>
Uh, the `sat` command will do that, at least
<Lofty>
I don't think equiv_induct has enough information for that
<Lofty>
But `miter` followed by `sat -prove-asserts` would give a counterexample, I think.
<DaKnig>
would it try to minimize the example?
<az0re>
Err hang on a second. How is it possible for the same combinational circuit to fail equiv_induct but pass equiv_struct?
<az0re>
My mental model must be wrong
<z0ttel>
miter -equiv gold gate miter; hierarchy -top miter; flatten; sat -prove-asserts <- that gives me a "proof finished, no models found" QED.
<z0ttel>
az0re: it did report some failing equivalences on internal wires after equiv_struct...
<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.
<z0ttel>
Also, I'm using debian stable with default packaged yosys, so it may just be an ancient version doing ancient things.
cr1901_modern has quit [Ping timeout: 264 seconds]
<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?