Bike has joined ##openfpga
hackkitten has quit [Ping timeout: 246 seconds]
hackkitten has joined ##openfpga
Flea86 has joined ##openfpga
keesj has quit [Ping timeout: 272 seconds]
keesj has joined ##openfpga
keesj has quit [Ping timeout: 258 seconds]
keesj has joined ##openfpga
emeb has left ##openfpga [##openfpga]
Flea86 has quit [Quit: Goodbye and thanks for all the dirty sand ;-)]
dj_pi has joined ##openfpga
dj_pi has quit [Ping timeout: 268 seconds]
unixb0y has quit [Ping timeout: 258 seconds]
unixb0y has joined ##openfpga
rohitksingh_work has joined ##openfpga
soylentyellow__ has joined ##openfpga
soylentyellow__ has quit [Client Quit]
soylentyellow_ has quit [Ping timeout: 240 seconds]
Bike has quit [Quit: Lost terminal]
Miyu has quit [Ping timeout: 240 seconds]
pie___ has joined ##openfpga
pie__ has quit [Ping timeout: 268 seconds]
rohitksingh_work has quit [Ping timeout: 245 seconds]
rohitksingh_work has joined ##openfpga
m_w has joined ##openfpga
azonenberg_work has quit [Ping timeout: 250 seconds]
azonenberg_work has joined ##openfpga
Bob_Dole has quit [Ping timeout: 260 seconds]
Bob_Dole has joined ##openfpga
Flea86 has joined ##openfpga
m4ssi has joined ##openfpga
m_w has quit [Ping timeout: 268 seconds]
bibor has quit [Quit: WeeChat 1.6]
soylentyellow has joined ##openfpga
bibor has joined ##openfpga
bibor has quit [Client Quit]
bibor has joined ##openfpga
Flea86 has quit [Quit: Goodbye and thanks for all the dirty sand ;-)]
m_w has joined ##openfpga
m_w has quit [Ping timeout: 268 seconds]
rohitksingh_work has quit [Read error: Connection reset by peer]
<_whitenotifier-e> [whitequark/Glasgow] whitequark pushed 1 commit to nmigen [+0/-0/±39] https://git.io/fhCcn
<_whitenotifier-e> [whitequark/Glasgow] whitequark 1d8e1d0 - Bulk port of all gateware to nMigen compatibility layer.
<_whitenotifier-e> [Glasgow] Failure. The Travis CI build failed - https://travis-ci.org/whitequark/Glasgow/builds/479871492?utm_source=github_status&utm_medium=notification
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> State 3: First item has been read
rohitksingh has joined ##openfpga
<ZipCPU> State 4: Second item has been read
<ZipCPU> The state machine is shown at the end
<ZipCPU> It will be simpler in a synchronous environment than an asynchronous environment
<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.
edmund has quit [Quit: Ex-Chat]
X-Scale has quit [Ping timeout: 244 seconds]
mumptai has joined ##openfpga
ZipCPU has quit [Quit: ZNC 1.6.4 - http://znc.in]
ZipCPU has joined ##openfpga
<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
<ZipCPU> davidc__: Here's the documentation of the broken AXI-lite implementation: http://zipcpu.com/formal/2018/12/28/axilite.html
<azonenberg> davidc__: if you're sending bugs to a fae i might have a few too
<Finde> this has probably already been passed around but thought I'd share: https://github.com/PrincetonUniversity/prga
<Finde> it's on the program for OSDA https://osda.gitlab.io/
<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> Here's the first experience link: https://zipcpu.com/blog/2017/10/19/formal-intro.html
<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
<Finde> dunno if it's useful for any of you, but LeWiz made their two ethernet macs open under LGPL recently: https://github.com/lewiz-support?tab=repositories
<m_w> azonenberg, I was hoping the oscillator thing was the magic bullet
_whitenotifier-c has joined ##openfpga
<_whitenotifier-c> [Glasgow] whitequark closed pull request #95: arch.xilinx: add empty __init__ file to please setuptools - https://git.io/fhCNq
<_whitenotifier-c> [whitequark/Glasgow] whitequark pushed 1 commit to master [+1/-0/±0] https://git.io/fhCN3
<_whitenotifier-c> [whitequark/Glasgow] rohitk-singh 9f98773 - arch.xilinx: add empty __init__ file to please setuptools
<azonenberg> m_w: new board has a crystal instead of mems
<azonenberg> 1.8 to 3.3 vdd adjustable
<_whitenotifier-c> [Glasgow] Error. The Travis CI build could not complete due to an error - https://travis-ci.org/whitequark/Glasgow/builds/480046137?utm_source=github_status&utm_medium=notification
<azonenberg> ac or dc coupling
<_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!
<_whitenotifier-c> [Glasgow] Success. The Travis CI build passed - https://travis-ci.org/whitequark/Glasgow/builds/480046263?utm_source=github_status&utm_medium=notification
<azonenberg> also the 1.2, 1.8, 2.5, and 3.3v rails are jumperable to come from either a LTC3374 like on starshipraider, or an LDO
<azonenberg> i'm trying to simultaneously reproduce my existing setup and allow tweak room to fix the issue
Bob_Dole has quit [Ping timeout: 268 seconds]
<m_w> shapr, hey great to hear
<m_w> the forum is not wasting too much of my time
<m_w> you figure out the memory mapped interface?
<m_w> I really wish I have more time to work on the beaglewire
<m_w> it is all sunken cost so my motivation is pretty low
<shapr> m_w: still haven't figured out the memory mapped interface
<shapr> would very much like to :-)
<m_w> shapr, it is not that bad once you figure it out
<shapr> but so far I've been doing verilog on the ice40 that only talks to pmods
<m_w> I think patryk's examples need some work
<shapr> memory mapped anything is a big jump from building webapp services, but I like the variety
<shapr> I do wish for more examples, but the best way is for me to write some
<sorear> Does anyone know anything about the "internal priority changes" in https://lists.llvm.org/pipermail/llvm-dev/2019-January/129121.html ?
<m_w> shapr, well it is pretty straightforward but I think patryk's userspace mmap example is the wrong way to do it in most cases
<shapr> m_w: though I would happily bribe someone to write the memory mapped C code that matches that verilog demo
<sorear> ( Intel has decided to stop maintaining the nios2 compiler backend )
<m_w> shapr, I typically promote the use of kernel modules/driver for accessing memory mapped IO
<azonenberg> sorear: nios is dying? intel/altera is going full arm now?
<sorear> azonenberg: how much other supporting evidence do we have for that?
<shapr> I've never written a kernel module.
<whitequark> m_w: that doesn't sound right.
<whitequark> why is userspace not suitable for MMIO?
<whitequark> if you have an uncacheable mapping then it should be equivalent
<m_w> depend on the use case
<m_w> *depends
<m_w> if you have a standard peripheral, use the kernel subsystems
<shapr> so beaglebone capes drivers make more sense as a kernel module?
<sorear> what if: semantically-pcie beaglebone capes, vfio
<m_w> shapr, because it is mapped to an FPGA to depends on the loaded bitstream
<shapr> m_w: I think I'm missing some context
<shapr> or maybe a preposition
<shapr> The mmap address is mapped to an FPGA, and ... what? depends on the loaded bitstream?
<whitequark> m_w: I'd say this is backwards--if you want a peripheral exposed via standard kernel APIs, use the kernel subsystems
<whitequark> it's perfectly valid and reasonable to drive an Ethernet card via userspace MMIO, for example
ayjay_t has quit [Read error: Connection reset by peer]
ayjay_t has joined ##openfpga
<m_w> I suppose
<shapr> I'd happily bribe someone to write some code that lets me shift bits from the BeagleBone to the ice40, acceptance criteria would be "deliver C code that makes the arm_blink_leds work": https://github.com/pmezydlo/BeagleWire/blob/master/examples/arm_blink_leds/top.v
<m_w> shapr, the bridgelib should let you do that
* shapr looks
<shapr> I'll try it
<m_w> the pointer is mmap'd to the IO space
<m_w> it is 16 bit word aligned
<m_w> this does that magic to setup the pointer
<m_w> then just access the IO space like it is a regular pointer
<m_w> looks like the arm led example maps to the first address in the map lower 4 bits
<m_w> so change the following two lines to write the patterns:
<shapr> if I get it working, where do I send your bribe? :-)
<shapr> buy another beaglewire?
<m_w> I get no money for the current sales
<shapr> that makes me sad
<m_w> until they run out
<m_w> I made about 500USD on the project, if you don't count my time
<shapr> that's not much money
<shapr> was exactly the board I wanted though
<shapr> where I could install+run all the tools on the board with the fpga
<m_w> it can run self contained but it is a bit slow compiling bitstreams
<shapr> maybe one day I'll know enough to have an opinion on mmio in userspace vs kernel module
<m_w> anyone here adept at making text fixtures?
<shapr> what's that?
<m_w> hardware for testing hardware
<shapr> oh *test* fixtures
<m_w> oops
<shapr> I get new vocabulary here all the time, so I just ask
<m_w> I was so low on funds from the campaign that I had to test the first batch of beaglewire by hand
<shapr> yow
<m_w> yeah it was a monster of a chore on 200 boards
<m_w> crowdsupply wants me to quote creation of a test fixture but I don't typically make them
<m_w> most companies charge a lot for them, more than can be justified for the volume of sales
<davidc__> m_w: bunnie recently wrote a good blog on it
<shapr> bunnie is my hero
<davidc__> m_w: sparkfun has also done some articles (their PCB-based pogo pin fixtures are useful and low cost)
<m_w> I did make a simple pogo pin fixture for lofive but this would would be a bit more complex
<m_w> davidc__, I have seen the sparkfun ones, quite nice
<davidc__> eh, past that my knowledge drops off rapidly.
<m_w> I just don't know what to quote for the creation of said fixture
Bob_Dole has joined ##openfpga
X-Scale has joined ##openfpga
xdeller has joined ##openfpga
tmeissner has joined ##openfpga
dj_pi has quit [Ping timeout: 245 seconds]
Maya-sama has joined ##openfpga
Miyu has quit [Read error: Connection reset by peer]
Maya-sama is now known as Miyu
tmeissner has quit [Quit: Textual IRC Client: www.textualapp.com]
mumptai has quit [Quit: Verlassend]
zng has quit [Ping timeout: 246 seconds]
rohitksingh has quit [Ping timeout: 268 seconds]
Flea86 has joined ##openfpga
Bike has joined ##openfpga