kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
cr1901_modern has quit [Ping timeout: 260 seconds]
cr1901_modern has joined #yosys
lf has joined #yosys
lf_ has quit [Ping timeout: 260 seconds]
Degi has quit [Ping timeout: 256 seconds]
Degi has joined #yosys
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
az0re has quit [Remote host closed the connection]
az0re has joined #yosys
az0re has quit [Remote host closed the connection]
az0re has joined #yosys
emeb_mac has quit [Quit: Leaving.]
citypw has joined #yosys
Asu has joined #yosys
indy has quit [Ping timeout: 246 seconds]
indy has joined #yosys
jakobwenzel has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
miek has quit [Ping timeout: 246 seconds]
jordigw has quit [Ping timeout: 246 seconds]
miek has joined #yosys
jordigw has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
vidbina has joined #yosys
cr1901_modern has joined #yosys
jakobwenzel has quit [Ping timeout: 260 seconds]
jakobwenzel has joined #yosys
vidbina has quit [Ping timeout: 264 seconds]
jakobwenzel has quit [Quit: jakobwenzel]
vidbina has joined #yosys
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
jakobwenzel has joined #yosys
jakobwenzel has quit [Client Quit]
citypw has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
emeb has joined #yosys
jakobwenzel has joined #yosys
jakobwenzel has quit [Quit: jakobwenzel]
citypw has quit [Ping timeout: 240 seconds]
jakobwenzel has joined #yosys
ayazar1 has joined #yosys
vidbina has quit [Ping timeout: 260 seconds]
ayazar1 has quit [Quit: ayazar1]
dys has quit [Ping timeout: 240 seconds]
dys has joined #yosys
N2TOH_ has joined #yosys
N2TOH has quit [Ping timeout: 260 seconds]
emeb_mac has joined #yosys
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
jakobwenzel has quit [Ping timeout: 260 seconds]
sorear has quit [Read error: Connection reset by peer]
sorear has joined #yosys
<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?
alexhw has quit [Ping timeout: 256 seconds]
<daveshah>
My understanding is that it does some name based matching of registers to help the proof
<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?
<daveshah>
Yes
<daveshah>
No SMT involved
<mwk>
equiv_induct does not do register matching; the wrapper equiv_opt pass does
<mwk>
equiv_induct requires you to already have preexisting $equiv cells
<cr1901_modern>
equiv_opt was the pass I was looking at, but I wanted to see how equiv_induct works first
<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
<daveshah>
I think you could use something like equiv_miter with write_smt2 if you wanted
<daveshah>
But its not a route I've personally tried
<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?