kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
Degi has quit [Ping timeout: 240 seconds]
Degi has joined #yosys
N2TOH has joined #yosys
citypw has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
emeb_mac has quit [Quit: Leaving.]
jakobwenzel has joined #yosys
<z0ttel>
Does symbiyosys "prove basecase" differ from bmc and can I give it a separate depth than the induction?
<daveshah>
It doesn't differ afaik, but there is no way of giving it a different depth
<daveshah>
I'm not sure why you'd want a different depth though. Lower would render the proof unsound, higher would be superfluous
<z0ttel>
oh, okay I realize my error now, induction depends on $depth steps too... okay, thx
<z0ttel>
But, an optimisation would then be to check induction results after each basecase step and terminate with PASS when induction was successful with less steps than basecase has so far?
<daveshah>
No, because induction differs between the first N-1 steps and the final N step
chipb has quit [Quit: chipb]
chipb has joined #yosys
<z0ttel>
So the command line output counting down induction steps isn't SymbiYosys trying to solve the full induction with less than $depth?
vidbina has joined #yosys
Asu has joined #yosys
<daveshah>
No, the way the induction part works is N-1 cycles assuming that assertions are true then checking assertions on the final cycle
peeps[zen] has joined #yosys
peepsalot has quit [Ping timeout: 240 seconds]
<z0ttel>
I mean, I now realise that a k-induction proof essentially proves: (assertions hold for k-1 steps) -> (assertions holds in step k) with a base case of step 0 to k-1
<z0ttel>
But Symbiyosys counts down the induction steps starting at k and, depending on what I'm trying to prove, stops the induction step at different steps with a PASS result.
strobokopp has joined #yosys
show1 has quit [Quit: WeeChat 2.7]
show has joined #yosys
jakobwenzel1 has joined #yosys
kristianpaul has quit [Read error: Connection reset by peer]
kristianpaul has joined #yosys
emeb has joined #yosys
jakobwenzel1 has quit [Quit: jakobwenzel1]
citypw has quit [Ping timeout: 240 seconds]
az0re has quit [Remote host closed the connection]
az0re has joined #yosys
<ZipCPU>
z0ttel: I've asked for this optimization for some time. If induction can prove PASS in 5 steps, the basecase should be ended after 5 steps.
<ZipCPU>
There's another optimization you can do as well, but I don't know that the tool could do it, so sometimes you can end your proof early: If induction finishes in 10 steps, and the basecase is stuck on step 3--but yet you know your design can enter into an idle state on step 2, then you can know that your design will pass
kraiskil has joined #yosys
<thardin>
damn the ecp5's are nice. it's looking like finding ADCs to feed them that don't cost an arm and a leg is trickier
<tnt>
for some of them a single kidney is enough.
emeb_mac has joined #yosys
_whitelogger has joined #yosys
thardin has quit [Ping timeout: 256 seconds]
Asu has quit [Ping timeout: 256 seconds]
<cr1901_modern>
I don't remember why the k-induction counts down, but it confuses me too (since if you look at the SMT files generated, k-induction will _add_ more states as the k-induction counter counts down)
kristianpaul has quit [Read error: Connection reset by peer]