<whitequark>
ZipCPU: ok, I think I finally formulated what I want to get wrt FV of a FIFO.
<whitequark>
it is a mode that is a hybrid of BMC and k-induction, of sorts.
<whitequark>
the idea is that it works like BMC (and indeed, can use sby's `mode bmc`), with two important exceptions:
<whitequark>
1. the initial state of all FFs is undetermined.
<whitequark>
2. all assertions of the model are turned into assumptions, so that the initial state is constrained to something sensible
<whitequark>
ok, sorry, I'm not being very clear. let me try again.
<whitequark>
you have a model. the model consists of DUT (that has logic, FFs, etc) and specification (that has logic, FF, etc).
<whitequark>
in normal BMC, all of these FFs start out at their init values. in k-induction, all of these FFs start out at arbitrary values, and are constrained by assertions.
<whitequark>
what I want is a more finely grained approach. in it, DUT FFs would start at arbitrary values, but constrained by assertions on the DUT internal state (i.e. white-box assertions)
<whitequark>
however, specification FFs would start out at their initial state.
<whitequark>
this lets me combine white-box and black-box methods. specifically, as I implemented it for the FIFO, the DUT contains some assertions, which are inherent to that DUT implementation
<whitequark>
and then the FIFO contract specification contains some assertions, which exclusively check the DUT external interface.
<whitequark>
this has the following result. at the beginning, the DUT materializes in an arbitrary valid state. the specification materializes in its initial state.
<whitequark>
this lets me write normal sequential logic in the specification that *still* applies to *every* valid starting DUT state, thus exploring a much larger state space than normal BMC.
<whitequark>
but at the same time, this lets me write my specification in a completely black box fashion, which makes it vastly simpler and easier to write.
<whitequark>
have my cake and eat it too, of sorts. thoughts?
<whitequark>
cc sorear
<whitequark>
I did some initial experimentation with this method and the results are promising, but of course I may be missing something very important.
Stary has joined ##openfpga
m_w has joined ##openfpga
paul_99 has joined ##openfpga
unixb0y has quit [Ping timeout: 240 seconds]
unixb0y has joined ##openfpga
emeb has quit [Quit: Leaving.]
Zorix has quit [Remote host closed the connection]
Zorix has joined ##openfpga
Miyu has quit [Ping timeout: 250 seconds]
Zorix has quit [Quit: Leaving]
Zorix has joined ##openfpga
pie__ has quit [Read error: Connection reset by peer]
pie_ has joined ##openfpga
pie__ has joined ##openfpga
pie_ has quit [Ping timeout: 245 seconds]
_whitelogger has joined ##openfpga
_whitelogger has joined ##openfpga
rohitksingh has joined ##openfpga
* ZipCPU|Laptop
is thinking about whitequark's idea
<whitequark>
fwiw I discussed it with Clifford and the plumbing for it can be easily made using an additional chformal mode, which I will probably ad.
<whitequark>
*add.
<ZipCPU|Laptop>
I'm not sure I follow the idea well enough yet. So, why would you not use induction as is for this check?
<ZipCPU|Laptop>
Where the specification can also start in an arbitrary state constrained only by assertions?
<ZipCPU|Laptop>
A simple example comes to mind of why you might wish to use induction with specification and DUT properties: a serial port
<whitequark>
ZipCPU: the reason I do not want to use induction is that the specification FSM and the DUT may easily end in inconsistent state
<ZipCPU|Laptop>
As part of my tutorial, I recently posted a serial port receiver implementation. As initially configured, this receiver requires 868 clocks per baud, or 8680 clocks per byte (8N1)
<whitequark>
e.g. specification FSM may think that it already wrote an entry into FIFO but it's not there.
<whitequark>
this *can* be constrained with appropriate assumes, which get very unwieldy very quickly.
<ZipCPU|Laptop>
There would be no possibility of verifying something in a much longer fashion, such as the 8680 clocks of the serial port, without using induction in both
<ZipCPU|Laptop>
So, your reason for not wanting to use induction is to be able to keep the specification proof unaware of the internals of the DUT?
<whitequark>
indeed.
<ZipCPU|Laptop>
This wouldn't work with some designs certainly
<ZipCPU|Laptop>
(The serial port would be a notable design where this would be a useless approach)
<whitequark>
that is true. it requires that the design would already carry assertions about its internal state, for one. so it is not entirely black box.
<ZipCPU|Laptop>
It might work with a lot of transaction based approaches ... but it would make the proof length longer than it has to be at the same time
<whitequark>
that is definitely true.
<ZipCPU|Laptop>
I'm thinking of SPI flash as another example
<whitequark>
I would gladly exchange time spent writing specification (and moreso, specification complexity) for proof length.
<whitequark>
mostly because decoupling specification from DUT allows me greater ease in changing either
<ZipCPU|Laptop>
Why does your specification need to be that complex though? You could write your specification in this simple fashion if you wanted as is
<whitequark>
how would this work with induction then?
<ZipCPU|Laptop>
:/
<whitequark>
I don't understand, sorry.
* ZipCPU|Laptop
isn't sure how well he understands his own idea
<ZipCPU|Laptop>
Here's my thought: You can write your white-box specification normally
<ZipCPU|Laptop>
But then tie it to the rest of the design for induction
<ZipCPU|Laptop>
The specification is as simple as you want, but the logic within it needs to be constrained to the DUTs internals
<whitequark>
let me demonstrate with an example
<ZipCPU|Laptop>
Ok
<whitequark>
I have SyncFIFO and SyncFIFOBuffered. SyncFIFOBuffered uses a non-FWFT FIFO (to allow for use of block RAM) and it effectively uses the output register of the internal non-FWFT FIFO to simulate an FWFT FIFO with latency 1 and one level deeper.
<ZipCPU|Laptop>
Go on
<whitequark>
writing out the condition for "FIFO has these two entries consecutively, somewhere inside" in this context becomes more complicated. I *can* write it, but I want to avoid doing such things, because I aim for a very short and clear specification, writing it in such a way as to minimize the amount of specification bugs.
<whitequark>
in my experience, formal methods find bugs I would not otherwise discover, but at the same time, I end up with more bugs in my specification than in my DUT
<whitequark>
this motivates me to seek ways of simplifying specification, and given *how* much more bugs I have in specification than in DUT, I aim for something radical.
<whitequark>
e.g. when I wrote the first specification for my CPU, it found one fairly obscure bug. But not before I fixed about a dozen specification bugs. Maybe more.
<whitequark>
I am not happy about that code, or its SVA equivalent.
<ZipCPU|Laptop>
Exactly ... this is just easier to express in the window here
<whitequark>
what I want is... in English, I would express this as. "this FIFO matches the ideal FIFO model, with latency bounded by 1."
<whitequark>
(and for non-buffered version, "with latency bounded by 0.")
<ZipCPU|Laptop>
I'm not sure the latency is really a part of the specification, rather the implementation only
<whitequark>
in case of nMigen's FIFO, it is a part of the contract, and it is documented.
<whitequark>
of course, another FIFO might be different.
<ZipCPU|Laptop>
Curious: Why are you testing in your specification that after the first read there's only one item in the FIFO?
<whitequark>
can you point me to the line?
* ZipCPU|Laptop
just found the "else" ... I was looking at line 160
<ZipCPU|Laptop>
I'm not sure what to say on the idea. I'll need to spend some more time thinking about it
<whitequark>
I am actually rewriting this right now in terms of proving model equivalence, because even this black-box specification seems too verbose and error-prone to me.
<whitequark>
indeed I have spent rather a lot of time fiddling with conditions and asserts until I got them just right, and the comments reflect that.
<whitequark>
I think all of that time has been wasted (other than as a learning opportunity) and a better method is necessary.
<ZipCPU|Laptop>
... so the first proof would be BMC on the Spec + DUT
<ZipCPU|Laptop>
The second proof would then be this modified (Induction on DUT) (BMC on spec)
<ZipCPU|Laptop>
However, you'd still need the full N steps, else the induction on DUT would fail
<whitequark>
that sounds right to me.
rohitksingh has quit [Ping timeout: 246 seconds]
pie___ has joined ##openfpga
pie__ has quit [Ping timeout: 246 seconds]
rohitksingh has joined ##openfpga
ZipCPU|Laptop has quit [Ping timeout: 240 seconds]
rohitksingh has quit [Ping timeout: 245 seconds]
ZipCPU|Laptop has joined ##openfpga
ZipCPU|lapt0p has joined ##openfpga
ZipCPU|Laptop has quit [Ping timeout: 268 seconds]
lutsabound has joined ##openfpga
<ZipCPU|lapt0p>
whitequark: I can think of several examples where your idea would not work. Two worth discussing include a very large FIFO, and a serial port
<whitequark>
I acknowledge that; but I think to an extent this highlights weaknesses elsewhere
<whitequark>
specifically, for e.g. a FIFO, we are currently limited to verifying one instantiation at a time.
<ZipCPU|lapt0p>
elsewhere?
<whitequark>
in nMigen I only verify specific widths and depths of a FIFO. I have to select the depths in such a way that different instantiations get selected, e.g. power-of-2 and NPOT depths.
<ZipCPU|lapt0p>
Not quite my question. Consider, for example, a FIFO where you start nearly full. You write two values to the FIFO and (perhaps) it is then full. You'll never get to empty within a reasonable number of cycles
<whitequark>
right, I understood that
<ZipCPU|lapt0p>
Likewise, one of the FIFO's I worked with had a bug where any write request (in spite of full flag) would always get written to the FIFO. Were the FIFO full, that would overwrite the last element
<whitequark>
so, I can see two reasons for trying to verify a very deep FIFO.
<ZipCPU|lapt0p>
Without at least one clock per FIFO element, you'd never find the bug
<whitequark>
reason 1: you are verifying the exact instantiations of components of your design.
<whitequark>
reason 2: your language leaves you uncertain whether you hit an edge case as you make parameters larger, e.g. perhaps going over 32 bits somewhere will produce a change in behavior.
<ZipCPU|lapt0p>
I was considering reason 1
<whitequark>
indeed. this is a valid reason and it is something my approach could not handle.
<whitequark>
it therefore represents a tradeoff: a much simpler model that requires having faith that the properties proven for small instantiations hold for all instantiations.
<whitequark>
I am okay with this tradeoff in many cases, but it is also valid to not be fine with it.
<whitequark>
this also applies to your serial port example, fwiw, except "small" would now be "high baud rate"
<ZipCPU|lapt0p>
Asu: See the title line if you are interested in any past conversations
<ZipCPU|lapt0p>
The topic is somewhat recurring: Induction is hard and requires white box properties. How can I restore a simplicity of black box testing?
<Asu>
i'm still a newb in hw design and haven't looked into formal verification yet
<Asu>
but when i get back to it i'm definitively going to learn formal verification :P
<ZipCPU|lapt0p>
Asu: I'm hoping the tutorial (that's nearly written) will provide a nice entry level introduction for those who've never used formal before
<ZipCPU|lapt0p>
The tutorial, though, starts all the way back at "This is a register"--so it's very much designed for total beginners
<Asu>
cool
<ZipCPU|lapt0p>
I personally don't see Formal Verification as an "advanced" topic that should be learned after RTL, but rather a companion topic that should be learned with RTL
<Asu>
the most complex thing i've come up so far in hw design is a simple BF CPU
<ZipCPU|lapt0p>
That's complex enough to want formal methods
<Asu>
i suppose what formal can bring to the table is figuring out bugs before i even have to put a program in and debug it if it goes wrong?
<ZipCPU|lapt0p>
yes!
<ZipCPU|lapt0p>
That's only one part
<ZipCPU|lapt0p>
Another part would be to verify that the CPU's bus'es follow the rules of the road
<Asu>
... because debugging by looking out signals in a waveform viewer wasn't nice :P
<ZipCPU|lapt0p>
Especially not for a CPU!
lutsabound has quit [Quit: Connection closed for inactivity]
ayjay_t has quit [Read error: Connection reset by peer]
ayjay_t has joined ##openfpga
Flea86 has quit [Quit: Goodbye and thanks for all the dirty sand ;-)]
ayjay_t has quit [Read error: Connection reset by peer]
ayjay_t has joined ##openfpga
emeb has joined ##openfpga
Stary has joined ##openfpga
ZipCPU|lapt0p has quit [Remote host closed the connection]
ayjay_t has quit [Read error: Connection reset by peer]
ayjay_t has joined ##openfpga
ZipCPU|Laptop has joined ##openfpga
rohitksingh has quit [Ping timeout: 250 seconds]
noobineer has joined ##openfpga
noobineer has quit [Ping timeout: 246 seconds]
noobineer has joined ##openfpga
GenTooMan has joined ##openfpga
<mithro>
If anyone is at Linux.conf.au 2019 I have FPGA Tomu boards and other give aways for people!
* tnt
really wants to check out Australia soon ... Linux.conf.au would be a good excuse.
<tnt>
mithro: what "other" btw ? :p
CoffeeFlux has left ##openfpga [##openfpga]
<mithro>
tnt: Mostly Artix 7 stuff to encourage SymbiFlow contribution
emeb has quit [Quit: Leaving.]
Richard_Simmons has quit [Remote host closed the connection]
zem has quit [Ping timeout: 250 seconds]
zem has joined ##openfpga
<adamgreig>
if most states in my state machine need to do something like 'wait five cycles', am i better off having five states that each advance to the next, or one state and a separate counter register that gets incremented/decremented, or what's the tradeoff?
rrika has joined ##openfpga
<adamgreig>
i get that more states means bigger state decoding logic and perhaps at some point you swap from one-hot being good to binary encoding being good, but presumably a separate counter adds a bunch more logic to each state too
<tnt>
I usually go for a separate counter.
<tnt>
counters are small, and you can write it as a decrement and trigger on the overflow so you really have a register output driving the next_state logic which is nice.