<cr1901_modern>
One dummy design I wanted to formally verify is an SPI core... the only invariant I can think of proving is "connect it to a dummy 32-bit SPI slave and assert that the SPI's core data at cycle 0 == the SPI slave's data at cycle 33.
<cr1901_modern>
Thus I have proven that the SPI core at least sends data correctly
<cr1901_modern>
First off, is that a good invariant to prove? Second, can it feasibly be proven using yosys?
<rqou>
that sounds reasonable
<rqou>
i believe it should be possible to prove, but i'm not sure
<rqou>
azonenberg?
<cr1901_modern>
rqou: This additionally leads to my second confusion about yosys' SMT capabilities >>
<cr1901_modern>
AFAIK, SMT is "SAT with some restrictions lifted."
<awygle>
i eventually bought a book about this stuff but i haven't had time to read it
<cr1901_modern>
There is a very good tutorial for SAT solvers written in Python if you do a cursory Google search! :)
<cr1901_modern>
However, this tutorial claims that SAT is only applicable to "combinational logic equations"; yosys is capable of proving statements that span multiple clocks
<awygle>
cr1901_modern: sounds great but i wouldn't know what to do with it :) i think you and i have the same problem getting our teeth into the subject
<rqou>
yosys somehow tracks the state evolution
<cr1901_modern>
I'm not sure how to make the leap from combinational to sequential
<rqou>
i don't know/remember how that part works exactly
scrts has quit [Ping timeout: 240 seconds]
<rqou>
another thing that isn't super intuitive is the induction that yosys performs
<cr1901_modern>
And I'm not even sure how a SAT solver could model a latch/instantaneous transition like that (combinational loop without illegal state?)
<rqou>
so for a FF you very clearly have a "before state" that combines with some input to lead to an "after state"
<rqou>
you could do that with combinatorial loops too as long as they don't oscillate
<cr1901_modern>
"another thing that isn't super intuitive is the induction that yosys performs" What does induction mean in this context?
<rqou>
iirc back in 2016 if you had an oscillating combinatorial loop the yosys prover would return incorrect answers
<rqou>
part of bounded model checking involves assuming you start at some symbolic state (rather than a concrete state) and then trying to prove the state evolution off of that
<rqou>
if you can do that and combine it with a proof that does start at some concrete state, you can combine these using induction to prove that a property always holds
<cr1901_modern>
symbolic state (I must've forgotten about this stuff :/)?
<cr1901_modern>
ahhh
<rqou>
basically "for any initial state"
<rqou>
rather than "for this initial state"
<cr1901_modern>
well if you proved for "any initial state" why do you need a concrete state?
<rqou>
er, read the slide deck :P
<cr1901_modern>
Oh whoops
<cr1901_modern>
I think I'll do that and also re watch the Dec 2016 presentation again.
<cr1901_modern>
I remember one of clifford's examples bothering me
<cr1901_modern>
rqou: Mind helping me when I get to that point in that presentation (possibly)?
<rqou>
yeah, the reason i say read the slides is because i don't quite remember either
<rqou>
:P :P
<cr1901_modern>
This also only works w/ finite state right? I mean, in practice, everything is an FSM, but I can imagine an assertion not being violated with say, a smaller memory store, but when you swap to a bigger memory store your assertion breaks >>
<cr1901_modern>
That means you have to in theory test infinite possible configurations of memory and up to an "infinite state machine"
<rqou>
er, memory is also finite
<rqou>
(in reality at least)
<cr1901_modern>
Hence "in practice, everything is an FSM"
<cr1901_modern>
Point blank, having an arbitrary memory store seems like it could really throw a wrench into proving a design correct to due state space explosion
<qu1j0t3>
cr1901_modern: i looked pretty hard at the python SAT tutorial.. it led me to knuth
<qu1j0t3>
who wrote a dozen of them in his nutty C
<cr1901_modern>
Hmm... did he also deal w/ state transitions?
scrts has joined ##openfpga
<qu1j0t3>
all his solvers just deal with single static sets of equations
<qu1j0t3>
i realised that some of the stuff i wanted to do may not map well to SAT systems
<cr1901_modern>
Well I just minddumped all my issues I've had w/ learning formal verification in one place, that's good at least
<awygle>
be sure to dump the solutions if you come across them, too :P
<cr1901_modern>
Idk if japaric/pftbest said anything to you but I have recently been playing w/ msp430 rust
<cr1901_modern>
so was wondering why I don't see you in #rust-embedded
<awygle>
cr1901_modern: because... that would make too much sense?
<cr1901_modern>
Good a reason as any...
<awygle>
na i only just upgraded to a real IRC client, so before i was dipping in and out of there in Mibbit, and since i've been kind of distracted from that work recently i forgot to join.
<awygle>
thanks for the reminder, it has now been rectified
<qu1j0t3>
things are converging to a happy status
<cr1901_modern>
Well, it's a small world... so I would hope there's some happiness to conserve
<rqou>
wait, there's a #rust-embedded?
<rqou>
on mozilla or freenode?
<cr1901_modern>
mozilla
<rqou>
hmm i should lurk on it
<rqou>
oh btw i got yelled at a while back for squatting too many crates :P
<rqou>
wait that's a ridiculously short user list
<rqou>
nobody uses embedded rust?
<cr1901_modern>
It's not an advertised channel that much I don't think
<cr1901_modern>
I don't remember how I learned about it
<awygle>
it's kind of japaric's thing? not sure if it's listed on the Big List O' Rust IRC Channels
<whitequark>
rqou: wait what? squatting?
<rqou>
i registered some crates for lulz because i was honestly surprised i could register them
<rqou>
if anybody actually wants one of the squatted crate names, i'll give it to them
<awygle>
i'm probably late on this but anybody have a perspective on this chiplicity thing?