C_Elegans-work has quit [Ping timeout: 258 seconds]
rohitksingh has joined ##openfpga
ayjay_t has quit [Read error: Connection reset by peer]
ayjay_t has joined ##openfpga
Miyu has joined ##openfpga
emeb has joined ##openfpga
dj_pi has joined ##openfpga
m4ssi has quit [Quit: Leaving]
genii has joined ##openfpga
whitequark has quit [Quit: Reconnecting]
whitequark has joined ##openfpga
_whitelogger has joined ##openfpga
ayjay_t has quit [Read error: Connection reset by peer]
ayjay_t has joined ##openfpga
powerbit has quit [Ping timeout: 272 seconds]
rohitksingh has quit [Ping timeout: 250 seconds]
<whitequark>
ZipCPU: do you have any advice for formal verification of FIFOs?
<ZipCPU>
Yes
<whitequark>
nMigen has a fairly large selection; FWFT, non-FWFT, FWFT with sync backing memory, async, async buffered...
<whitequark>
and it has had very heinous bugs in FIFOs before
<whitequark>
(though those would I think be only caught by verifying post-synthesis netlist from Vivado, but that can be done)
<ZipCPU>
The contract for a FIFO is: if you write two successive values in, you should be able to read those same two values out, in order, some time later
<whitequark>
ooh
<ZipCPU>
I've written two articles on synchronous FIFOs, but the asynchronous article actually has the two write test within it
<whitequark>
how do I write an assertion for that?
<ZipCPU>
It's a state machine:
<ZipCPU>
State 1: First item has been written
<ZipCPU>
State 2: First and second items have been written
<ZipCPU>
cr1901_modern: That's part of it ... that just recognizes being in the various states
<whitequark>
hmmm, this seems really complicated, somehow
<whitequark>
i feel like it ought to be simpler
<whitequark>
nMigen should definitely offer first-class multi-clock-domain formal support
<ZipCPU>
I have another example which looks a bit simpler using concurrent assertions
<whitequark>
none of this manual messing with $global_clock and $stable
<whitequark>
all of that should be automatically inferred from your design
<ZipCPU>
You don't need $global_clock or $stable with synchronous designs
<whitequark>
I know
<whitequark>
what I'm saying is that verifying single-domain designs in nMigen should be as close to verifying multi-domain designs as possible
<cr1901_modern>
Then just always run the clk2fflogic pass
<ZipCPU>
No, don't!
<whitequark>
that would not have the same semantics.
<ZipCPU>
SymbiYosys has an "multiclock on" option that replaces clk2fflogic
<whitequark>
I mean close in terms of developer effort
<whitequark>
oh?
<cr1901_modern>
I don't use symbiyosys
<cr1901_modern>
or rather, haven't used it
<whitequark>
how do you use multiclock?
<ZipCPU>
SymbiYosys is easier to work with than yosys-smtbmc
<cr1901_modern>
manually specifying to yosys to run clk2fflogic pass
* ZipCPU
steps away, will come back later
<whitequark>
ZipCPU: I think I figured out what I don't like about your approach
<whitequark>
specifically wrt FIFO contract
<whitequark>
it treats the FIFO as white-box, and I want to treat it as black-box
<whitequark>
perhaps a black-box with embedded asserts/assumes for induction support, but the overall harness would still do black-box testing
<whitequark>
that's not to say it's wrong; I only dislike it
<cr1901_modern>
dunno if that's always possible or even desirab- oh, you mentioned "embedded asserts/assumes for induction support"
<davidc__>
hey, does any one know if clifford is on IRC?
<daveshah>
not regularly
<davidc__>
Ok. Nothing pressing; I just kicked his vloghammer Xilinx bugs to someone that I know in Xilinx FAE, so I was gonna make the introduction if it was useful.
<ZipCPU>
davidc__: If you are chatting with a Xilinx FAE, did you see the AXI-lite bug I blogged about recently?
<ZipCPU>
whitequark: Formal Verification is fundamentally a white box testing method. While you can create "black box" "contracts" describing how a module should perform, the properties necessary to prove that the contract can be met tend to be quite intrusive
<whitequark>
ZipCPU: essentially I think I want a *methodology*, which splits a formal specification into a black box contract and a set of white box properties
emeb has quit [Quit: Leaving.]
<ZipCPU>
I've done FIFO's several times on the blog. Once without formal, once asynchronously, and once describing my first experience with formal methods. While the latter has a bit of a proof, it's not a complete one
<ZipCPU>
I only know of the one way to get to the complete proof, and that's the two writes followed by two reads test
<pie___>
is that really sufficient? its not like you have induction
<whitequark>
ZipCPU: yeah, the basis of my black box contract is the two writes plus two reads test.
<whitequark>
but I am concerned about complexity, and intertwinedness with the innards of the FIFO, of the rest of the specification
<ZipCPU>
Sure
<whitequark>
I am going to follow the approach I think is better when verifying nMigen's FIFOs
<whitequark>
let's see whether that works
<ZipCPU>
Here's the difficult part: you want to be able to restart that proof in the middle, so every step of the proof has to fully define the part it is on
<ZipCPU>
Or, at least passing induction will require it ...
<whitequark>
I understand that
<ZipCPU>
If you find a better/simpler way, then I'm all ears. I'd love to hear it.
<pie___>
<smalltext>use a functional language, make things correct by construction? :P</smalltext>
<whitequark>
I think I see one. but let's see first if I can actually finish a proof.
<ZipCPU>
pie__: Thank you for the suggestion. I've heard that suggestion before, but ... don't understand it. I might need to spend a day or two with someone to really appreciate your suggestion. (Thanks for making it tho)
<pie___>
ZipCPU, im somewhat joking but only because im not particularly familiar with the method myself (yet?)
<pie___>
ZipCPU, i recommend you look into the curry-howard isomorphism, and CLaSH (clash-lang.org), but i am unsure if and how applicable the concepts are to clash
<pie___>
they are probably applicable at least to the extent they are applicable to haskell
<pie___>
there is also an irc channel
<ZipCPU>
Shhh!!! Don't mention Haskell! shapr will try to teach it to me! :D :D :D
<pie___>
<3 ;3
<pie___>
i need to learn agda :V
<shapr>
NO
<shapr>
oh wait
<shapr>
yes
<shapr>
whitequark: your twitter is great fun to read
<shapr>
rqou: whatever happened with the russian display boards? did you build a better driver board?
<shapr>
ZipCPU: I think Haskell would blow your mind, and then you'd be like "wait, this is like proving things in verilog" and then you'd get a job at a big financial company doing HFT on FPGA
<pie___>
do HFT for a year, get rich, retire, write us moar tutorials :V
<davidc__>
ZipCPU / azonenberg lets see if these first ones get results before I chuck a dump-truck of bugs at him; this is a social connection, not a contractual one :P
m_w has joined ##openfpga
<azonenberg>
lol
<azonenberg>
ok
<azonenberg>
davidc__: the one i was thinking of i have to check in 2018.3 still
<azonenberg>
but it was incorrect synthesis of verilog strings containing \0 characters
<azonenberg>
there's another one that is causing some concatenated strings to be truncated that i havent repro'd in a minimal case yet
<azonenberg>
but VCS synthesizes it right and vivado truncates the first char of some substrings
<m_w>
azonenberg, you ever figure out the issue with your gigabit phy?
<Finde>
azonenberg: have you looked at VCS vs modelsim by any chance? I saw drastically different string handling with modelsim I think it was (could've been incisive)
<azonenberg>
Finde: no i have not, i dont have access to modelsim
<azonenberg>
isim, xsim, and vcs
<Finde>
fair
<azonenberg>
m_w: i have not
<azonenberg>
i tried a ton of things
<Finde>
being in an academic setting I get to hit my head against each of the simulators to find which hurts least ;)
<azonenberg>
i am now making an eval board with probe points and jumpers up the wazoo to reconfigure things
<azonenberg>
and twice as many decoupling caps as usual
<azonenberg>
that can take both the 9021 and 9031
<azonenberg>
in hopes it will shed some light on my problem
<azonenberg>
but i'm literally shooting in the dark here
<azonenberg>
i have zero idea what could be causing it
<_whitenotifier-c>
[Glasgow] rohitk-singh commented on pull request #95: arch.xilinx: add empty __init__ file to please setuptools - https://git.io/fhCNc
<azonenberg>
So lots of room to tweak
ayjay_t has quit [Read error: Connection reset by peer]
<m_w>
cool
ayjay_t has joined ##openfpga
<azonenberg>
m_w: then avddh and dvddh are adjustable across the full range
<shapr>
m_w: you know how I pushed for a beaglewire discussion forum? I now think I was wrong and it was a waste of your time, sorry. on the other hand, I am still enjoying the BeagleWire!