ChanServ changed the topic of #yosys to: Yosys Open SYnthesis Suite: https://github.com/YosysHQ/yosys/ | Channel logs: https://libera.irclog.whitequark.org/yosys/
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
emeb has quit [Quit: Leaving.]
adjtm_ has joined #yosys
adjtm has quit [Read error: Connection reset by peer]
adjtm has joined #yosys
adjtm_ has quit [Ping timeout: 240 seconds]
nelgau_ has joined #yosys
nelgau has quit [Ping timeout: 250 seconds]
Klotz has quit [Quit: Klotz]
tlwoerner has quit [Quit: Leaving]
tlwoerner has joined #yosys
citypw has joined #yosys
cr1901_ has joined #yosys
cr1901 has quit [Ping timeout: 252 seconds]
cr1901_ is now known as cr1901
emeb_mac has quit [Quit: Leaving.]
X-Scale has quit [Ping timeout: 240 seconds]
X-Scale` has joined #yosys
X-Scale` is now known as X-Scale
kristianpaul has quit [Ping timeout: 252 seconds]
kristianpaul has joined #yosys
shorne has joined #yosys
<shorne> Well, hello, I have spent the last few weeks deep diving into formal verification with yosys. I am re-defining our formal verification properties in the OpenRISC mor1kx core around the Load/Store Unit including, rams, dcache, dmmu and now LSU.
<shorne> Someone said Test benches are for ensuring you system is valid for the TB provided inputs. Formal verification is for ensuring your system works for all valid inputs.
<shorne> I find this formal verification is no silver bullet, as defining the valid inputs is the tricky part.
<gatecat> Yeah, the particular danger is with `assume` statements which restrict the input/state space
<shorne> yea, or like for me now is I put some assume's to start simple
<shorne> i.e. assume (!dbus_err_i);
<shorne> then I just leave that there :)
<gatecat> Mm
Klotz has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
citypw has joined #yosys
emeb has joined #yosys
<cr1901> shorne: https://github.com/cr1901/yosys-experiments/tree/master/sat/dffhold It's not always possible to do k-induction either
citypw has quit [Ping timeout: 240 seconds]
emeb has quit [Quit: Leaving.]
emeb has joined #yosys
emeb has quit [Quit: Leaving.]
emeb has joined #yosys
<jix> adding simple-path constraints makes k-induction complete in theory (whether it's useful in practice, I don't know yet, also not sure if any of the sby engines/solvers support it)
adamse has left #yosys [#yosys]
<lkcl> shorne, the generally-accepted "word" on formal correctness proofs is that they're much more useful - to everyone including you - when several people implement the same design and use the same formal correctness proof
<lkcl> the logic behind that being that you can accidentally make assumptions about the assumes/asserts.
<lkcl> the other thing that is a royal pain in the ass: inputs (or even combinations of bits *in* inputs) that you don't use, didn't put in the assumes, and the formal correctness engines go
<lkcl> "oh yeah i found this permutation of input bits you never thought possible could ever be set and hadn't covered in any switch statements (etc) but *if* you ever set them the output is borked, there you go"
<lkcl> :)
<lkcl> this one drove 2 people absolutely nuts for several weeks when trying to do a formal correctness proof for the libre-soc Power ISA rotate module