<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.
<ZipCPU|Laptop> Hmm ... let's consider: (write_first) ##1 (write_idle) [0:$] ##1 (write_second) |=> (first_item_in_fifo) [0:*] ##1 (read_first) ##1 (read_is_idle) [0:$] ##1 (read_second);
<ZipCPU|Laptop> Can this be divorced from the DUT to make a specification only assertion?
<ZipCPU|Laptop> I'm not sure it can be
<ZipCPU|Laptop> Certainly if you did, you'd lose the cabaility of proving this via induction
<whitequark> nMigen does not have an equivalent of SVA (nor can Yosys do the above), so I have something similar with if-else constructs: https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py#L153-L175
<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"
<_whitenotifier-c> [Glasgow] Success. The Travis CI build passed - https://travis-ci.org/whitequark/Glasgow/builds/481697323?utm_source=github_status&utm_medium=notification
<whitequark> ZipCPU|lapt0p: here is what I ended up with: https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py#L36-L187
rohitksingh has joined ##openfpga
greg__ has joined ##openfpga
Asu has joined ##openfpga
<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 ;-)]
Miyu has joined ##openfpga
greg__ has quit [Ping timeout: 250 seconds]
kbob has joined ##openfpga
kbob is now known as Guest59032
_whitelogger has joined ##openfpga
Stary has quit [Quit: ZNC - http://znc.in]
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.
<adamgreig> makes sense
greg__ has joined ##openfpga
X-Scale` has joined ##openfpga
X-Scale has quit [Ping timeout: 244 seconds]
X-Scale` is now known as X-Scale
Asu has quit [Quit: Konversation terminated!]