clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
vonnieda has joined #yosys
gsi_ has joined #yosys
gsi__ has quit [Ping timeout: 258 seconds]
PyroPeter has quit [Ping timeout: 252 seconds]
PyroPeter has joined #yosys
citypw has joined #yosys
proteusguy has joined #yosys
rohitksingh_work has joined #yosys
emeb_mac has quit [Ping timeout: 252 seconds]
citypw has quit [Ping timeout: 258 seconds]
vid has joined #yosys
Jybz has joined #yosys
futarisIRCcloud has joined #yosys
fsasm has joined #yosys
jevinskie has joined #yosys
m4ssi has joined #yosys
jevinskie has quit [Ping timeout: 258 seconds]
Ultrasauce has quit [Quit: Ultrasauce]
Ultrasauce has joined #yosys
jevinskie has joined #yosys
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
<tnt> Ok, I think my proof is good now (it passes and actually proves stuff :p) https://pastebin.com/rLGqiTXL
<tpb> Title: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - Pastebin.com (at pastebin.com)
jevinskie has quit [Ping timeout: 255 seconds]
tlwoerner has quit [Quit: Leaving]
citypw has joined #yosys
tlwoerner has joined #yosys
maikmerten has joined #yosys
<maikmerten> is there special magic necessary to build nextpnr with the GUI on Ubuntu 19.04? cmake doesn't find Python, despite libboost-all-dev, python-dev and python3-dev being installed
<maikmerten> CMakeError.log doesn't contain any mentioning of python
<tnt> ZipCPU: arf ... cover(f_was_full && f_empty);
<tnt> ZipCPU: it's cheating ... its asserting reset to go back to empty :)
<maikmerten> I vaguely remember there being issues on Ubuntu 18.10, too, and doing a horrible symlink "fix", but don't remember where to look
<ZipCPU> tnt: Adjust the f_was_full flag so that it clears on reset
<tnt> ZipCPU: yeah, I figured, I just found it sneaky :)
<maikmerten> ZipCPU, btw, I think your intuition that my stability problems with some placer seeds may be caused by driving IO from normally/randomly placed registers might be correct. I could not reproduce my stability problems when using BRAM as system RAM, but ~13% of placer runs with RAM in external SRAM fail.
<ZipCPU> maikmerten: Knowing is half the battle, ;)
<maikmerten> (of course, there could be other external problems, but the reliable bitstreams are "reliable" in function and the failing bitstreams are "reliable" in failing)
<ZipCPU> It sounds, though, like you have an SRAM problem of which I/O drivers are one possibility
<ZipCPU> How are you currently handling the SRAM I/Os?
<ZipCPU> Inferred?
<maikmerten> aye. No constraints whatsoever.
<tnt> maikmerten: what frequency are you running that sram at ?
<maikmerten> 25.125 MHz
<ZipCPU> I think I may have added an extra clock period to my controller when I did SRAM. It got me away from the instability problems, but slowed down the SRAM interaction as well.
<maikmerten> I'm ambitiously driving things without waitstates
<ZipCPU> Have you tried directly instantiating the SB_IO elements?
<tnt> (and put registers in them ...)
<maikmerten> not yet
<ZipCPU> Got it
<ZipCPU> Feel free to keep us all posted here, I'd love to hear how it's going
<maikmerten> I'm currently not sure how I'd instantiate a SB_IO and specify "that register over there, that should really go over here"
<ZipCPU> No?
<ZipCPU> I can help with that if you need it
* ZipCPU looks up the manual describing SB_IO's
<maikmerten> thanks for your kind helpfulness :-)
<maikmerten> oh, I'm instantiating SB_IOs already
* ZipCPU hasn't helped ... yet ;)
<maikmerten> in the toplevel of my design to get reliable tristate working
<tnt> maikmerten: you need to (1) remove the register from the logic (i.e. it shouldn't be described in your verilog) and (2) set PIN_MODE appropriately.
<tpb> Title: spu32/top.v at master · maikmerten/spu32 · GitHub (at github.com)
<maikmerten> tnt, yeah, that's what I feared ;-)
<tnt> (i.e. you can't tell it to 'move' the register, you need to remove it ...)
<ZipCPU> Ok, the SB_IOs are described in the iCE40FamilyHandbook.pdf
<tnt> 110100 is what you want
<maikmerten> https://github.com/YosysHQ/nextpnr/blob/master/docs/constraints.md <-- I hoped that would give me insight on how to place some constraints for arbitrary bels
<tpb> Title: nextpnr/constraints.md at master · YosysHQ/nextpnr · GitHub (at github.com)
<tnt> (that registers the input path and the output data and output enable)
<maikmerten> like "sram_address[0] - place that in <wherever>"
<tnt> maikmerten: unless you manually instanciate the DFF you won't be able to put the constraint on the right object.
<maikmerten> the ECP5 example looks promising, but this is iCE40
<ZipCPU> maikmerten: Google the iCE40 family handbook, and page 152 or so describes the SB_IO primitives
<tpb> Title: ice40-playground/spi_fast_core.v at master · smunaut/ice40-playground · GitHub (at github.com)
<tnt> That's how I did it in my spi core to force placement of some of the cells without using the sb_io regs.
<maikmerten> ZipCPU, I got the handbook :-)
<maikmerten> tnt, thanks
<maikmerten> *starred*
<maikmerten> (btw, thanks for all the nice support I receive in this channel. I'm messing around with FPGAs in a somewhat unstructured way in my spare time and some questions certainly are very basic or contain clear oversights on my part. Thanks for being patient!)
<tnt> maikmerten: your sram controller is a bit weird ... I mean registering the wishbone output data on the negative edge ....
<ZipCPU> maikmerten: Can I quote you on that on twitter? ;)
<tnt> pretty sure all wishbone signals are supposed to be synced to the same edge.
<ZipCPU> tnt: Did you post the code in question?
<ZipCPU> ... or is it posted?
<tpb> Title: spu32/sram512kx8_wb8_vga.v at master · maikmerten/spu32 · GitHub (at github.com)
jevinskie has joined #yosys
* ZipCPU opens tnt's link
<ZipCPU> Yeah, WB is supposed to be single edge of a clock only
<ZipCPU> Good catch, tnt
<ZipCPU> The other issue is that ... I remember at one time nextpnr couldn't handle both edges of the clock. Not sure I've heard the end of that, whether it can now or not
<tnt> it can
<ZipCPU> So ... it can properly reason about the timing of both edges of the clock?
<tnt> arachne and icetime couln't. Well ... it couldn't do a proper timing analysis, the bitstream would be correct.
<tnt> nextpnr can analyze the half clock cycle just fine.
* ZipCPU downloads the code, adjusts the "input" declarations to be "input wire" declarations
<maikmerten> ZipCPU, if you like to ;-)
<maikmerten> yeah, nextpnr can properly reason posedege <-> negedge timing wise
jevinskie has quit [Ping timeout: 246 seconds]
<maikmerten> (the reason for sampling the sram data on the negedge is that I need the data to be available on the following posedge)
vonnieda has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzz…]
<maikmerten> and given how the Wishbone spec illustrates "FASM" memory interfacing, the bus device can change output data somewhere between positive clock edges
<maikmerten> (as long as the data is stable for read on the positive edge)
<maikmerten> (c.f. llustration 8-14: Simple 16 x 8-bit SLAVE memory of the WB b4 spec, page 111)
rohitksingh_work has quit [Read error: Connection reset by peer]
<maikmerten> so I figured that presenting new output data "somewhere" could just as well be "exactly in the middle between posedges, which happens to be negedge)
<ZipCPU> Usually, that only slows down your design
<maikmerten> it does :-)
<ZipCPU> How about I_data ... is that clock synchronous at all? (Probably not, right?)
<maikmerten> not exactly in that spot in that design though ;-)
<maikmerten> no, I_data happens to be valid after the SRAM access time
<maikmerten> (so asynchronous)
<maikmerten> so O_wb_data could just be wired to I_data (from SRAM)
<maikmerten> but I'm somewhat worried that I_data will become invalid when new requests arrive, which is why I stuff the data into registers
<maikmerten> (IIRC the SRAM I use guarantees stable output data for a minimum of 0ns after a new address is applied, which is... not much)
<maikmerten> so applying a new address and reading data on the same clock edge seems dangerous to me
* maikmerten looks into SRAM data sheet
<maikmerten> yeah, t_DH (data hold) is specced at "min 0"
<tnt> What's the sram model ?
<ZipCPU> maikmerten: So ... things look something like this? https://imgur.com/a/pAU6fko
<tpb> Title: Imgur: The magic of the Internet (at imgur.com)
<maikmerten> ZipCPU, that looks right
<maikmerten> tnt, as in "model number" (that'd be AS7C34096A) or as in "abstract operational concept"?
<tnt> yeah p/n
<maikmerten> ah, k
<tnt> which speed grade ?
<maikmerten> it's a standard 10ns 512Kx8 asynchronous RAM
<maikmerten> (well, whatever "standard" means. I've seen alternative parts with the same specs, pin layout and overall timing from other vendors, too)
vonnieda has joined #yosys
<maikmerten> okay, gotta fetch an appointment, cya later!
maikmerten has quit [Quit: gotta run]
vid has quit [Ping timeout: 268 seconds]
vid has joined #yosys
rohitksingh has joined #yosys
jakobwenzel has quit [Quit: jakobwenzel]
vonnieda has quit [Ping timeout: 258 seconds]
vonnieda has joined #yosys
emeb has joined #yosys
vid has quit [Ping timeout: 246 seconds]
maikmerten has joined #yosys
rohitksingh has quit [Ping timeout: 246 seconds]
rohitksingh has joined #yosys
Jybz has quit [Ping timeout: 252 seconds]
<tpb> Title: fwb_slave.v · GitHub (at gist.github.com)
<ZipCPU> That checks the WB interface. It's also what I used to generate the cover statement I sent earlier
<maikmerten> ZipCPU, wow, that's so cool!
<ZipCPU> To "prove" that the memory works, you'd need to assume an arbitrary address and initial value, and then prove that the value gets properly returned and changed as a result of your interacting with the core
<ZipCPU> Normally, I wouldn't need to use $global_clock since almost all of my designs are synchronous. Since you chose to use both edges of the clock, the proof really needs to be set up as an asynchronous proof -- which is what I did
<ZipCPU> You can read more about formally verifying memory things here if you are interested: http://zipcpu.com/zipcpu/2018/07/13/memories.html
<tpb> Title: Formally Verifying Memory and Cache Components (at zipcpu.com)
<maikmerten> the f_ prefix is for "formal"?
emeb_mac has joined #yosys
emeb_mac has quit [Client Quit]
Jybz has joined #yosys
<ZipCPU> Yes, though it is only a convention I use
m4ssi has quit [Remote host closed the connection]
<maikmerten> conventions are plenty fine ;-)
<maikmerten> okay, sby sure creates quite some output
<ZipCPU> It should create two directories
<ZipCPU> If any assertion fails, that will show up in the *_prf/engine_0/ directory
<ZipCPU> The example trace will show up in the *_cvr/engine_0/ directory
<maikmerten> yup, two directories there are
<ZipCPU> That's partly because this proof has two parts as I set it up: a prove (proves that the assertions will never be violated) and a second one for cover (finds one way to make the cover() statements true)
<maikmerten> so, just to be sure: that is good (assertions will never be violated) -> SBY 18:32:12 [sram512kx8_wb8_vga_prf] summary: successful proof by k-induction.
<maikmerten> and that is the cover: SBY 18:32:12 [sram512kx8_wb8_vga_cvr] summary: engine_0 (smtbmc) returned PASS
<maikmerten> that auto-generated testbench with the system stimulus is pretty neat
jevinskie has joined #yosys
<maikmerten> okay, tying O_wb_ack to zero nicely leads to a FAIL, so that's nice as well ;-)
<maikmerten> (I'm currently in a "new toys, new toys!" mode)
janrinze has quit [Ping timeout: 252 seconds]
<ZipCPU> ;)
<ZipCPU> The cover summary means it was able to make the cover() statements true
<ZipCPU> You should then be able to find one trace for every cover statement within your file. It may be that some cover() statements share the same trace though
<maikmerten> yup, I see one cover() statement and one trace
jevinskie has quit [Ping timeout: 245 seconds]
jevinskie has joined #yosys
rohitksingh has quit [Ping timeout: 258 seconds]
fsasm has quit [Ping timeout: 246 seconds]
jevinskie has quit [Ping timeout: 245 seconds]
gnufan_home has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 248 seconds]
rohitksingh has joined #yosys
dys has joined #yosys
rohitksingh has quit [Ping timeout: 258 seconds]
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 268 seconds]
rohitksingh has joined #yosys
proteusguy has quit [Ping timeout: 246 seconds]
<maikmerten> one example of a register being far away from the SB_IO driven by it: https://pasteboard.co/If9QJEz.png
<tpb> Title: Pasteboard - Uploaded Image (at pasteboard.co)
<tnt> image not found ?
<maikmerten> hmm, works for me
<maikmerten> I can imagine the timing gettin pretty skewed there, especially as other address lines have registers somewhat closer
rohitksingh has quit [Remote host closed the connection]
<tnt> heh, yeah.
<tnt> :)
maikmerten has quit [Remote host closed the connection]
<tnt> ZipCPU: is there no way to access registers from submodules during formal checks ?
<ZipCPU> Not in the open version
<tnt> I need to assert on the content of a ram ... but that ram is a submodule ...
<ZipCPU> The way around that is to create a port, used only in formal mode, to pass the information you need around
<tnt> iew
<ZipCPU> Yeah
<ZipCPU> I had the same problem within the ZipCPU: https://github.com/ZipCPU/zipcpu/blob/master/rtl/core/zipcpu.v
<tpb> Title: zipcpu/zipcpu.v at master · ZipCPU/zipcpu · GitHub (at github.com)
<tnt> oh well ... it was a fun experiment.
s_frit has joined #yosys
<ZipCPU> That happens to be one of the reasons why many of my designs are only one deep, such as the AXI crossbar I've been working on
<daveshah> There's probably a way to do it with clever use of the expose command in the Yosys script
<ZipCPU> daveshah: If the first was ew, that's gotta be a double eww!
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
dys has quit [Ping timeout: 252 seconds]
gnufan_home has quit [Quit: Leaving.]
vonnieda has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzz…]
Jybz has quit [Ping timeout: 255 seconds]
tpb has quit [Remote host closed the connection]
tpb has joined #yosys