Friday, 2019-05-17

*** tpb has joined #yosys00:00
*** vonnieda has joined #yosys02:09
*** gsi_ has joined #yosys02:11
*** gsi__ has quit IRC02:14
*** PyroPeter has quit IRC02:52
*** PyroPeter has joined #yosys03:05
*** citypw has joined #yosys03:46
*** proteusguy has joined #yosys04:18
*** rohitksingh_work has joined #yosys04:49
*** emeb_mac has quit IRC07:14
*** citypw has quit IRC07:41
*** vid has joined #yosys08:02
*** Jybz has joined #yosys08:32
*** futarisIRCcloud has joined #yosys08:42
*** fsasm has joined #yosys08:48
*** jevinskie has joined #yosys09:17
*** m4ssi has joined #yosys09:40
*** jevinskie has quit IRC09:49
*** Ultrasauce has quit IRC10:31
*** Ultrasauce has joined #yosys10:32
*** jevinskie has joined #yosys10:39
*** futarisIRCcloud has quit IRC11:01
tntOk, I think my proof is good now (it passes and actually proves stuff :p)
tpbTitle: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - (at
*** jevinskie has quit IRC11:12
*** tlwoerner has quit IRC12:20
*** citypw has joined #yosys12:22
*** tlwoerner has joined #yosys12:35
*** maikmerten has joined #yosys12:35
maikmertenis 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 installed12:37
maikmertenCMakeError.log doesn't contain any mentioning of python12:38
tntZipCPU: arf ... cover(f_was_full && f_empty);12:39
tntZipCPU: it's cheating ... its asserting reset to go back to empty :)12:39
maikmertenI vaguely remember there being issues on Ubuntu 18.10, too, and doing a horrible symlink "fix", but don't remember where to look12:39
ZipCPUtnt: Adjust the f_was_full flag so that it clears on reset12:39
tntZipCPU: yeah, I figured, I just found it sneaky :)12:41
maikmertenZipCPU, 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.12:46
ZipCPUmaikmerten: Knowing is half the battle, ;)12:46
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)12:47
ZipCPUIt sounds, though, like you have an SRAM problem of which I/O drivers are one possibility12:47
ZipCPUHow are you currently handling the SRAM I/Os?12:47
maikmertenaye. No constraints whatsoever.12:48
tntmaikmerten: what frequency are you running that sram at ?12:48
maikmerten25.125 MHz12:48
ZipCPUI 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.12:48
maikmertenI'm ambitiously driving things without waitstates12:49
ZipCPUHave you tried directly instantiating the SB_IO elements?12:49
tnt(and put registers in them ...)12:50
maikmertennot yet12:51
ZipCPUGot it12:51
ZipCPUFeel free to keep us all posted here, I'd love to hear how it's going12:52
maikmertenI'm currently not sure how I'd instantiate a SB_IO and specify "that register over there, that should really go over here"12:52
ZipCPUI can help with that if you need it12:52
* ZipCPU looks up the manual describing SB_IO's12:52
maikmertenthanks for your kind helpfulness :-)12:52
maikmertenoh, I'm instantiating SB_IOs already12:52
* ZipCPU hasn't helped ... yet ;)12:53
maikmertenin the toplevel of my design to get reliable tristate working12:53
maikmerten <-- ca. lines 29012:53
tntmaikmerten: 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.12:53
tpbTitle: spu32/top.v at master · maikmerten/spu32 · GitHub (at
maikmertentnt, yeah, that's what I feared ;-)12:54
tnt(i.e. you can't tell it to 'move' the register, you need to remove it ...)12:54
ZipCPUOk, the SB_IOs are described in the iCE40FamilyHandbook.pdf12:54
tnt110100 is what you want12:55
maikmerten <-- I hoped that would give me insight on how to place some constraints for arbitrary bels12:55
tpbTitle: nextpnr/ at master · YosysHQ/nextpnr · GitHub (at
tnt(that registers the input path and the output data and output enable)12:55
maikmertenlike "sram_address[0] - place that in <wherever>"12:55
tntmaikmerten: unless you manually instanciate the DFF you won't be able to put the constraint on the right object.12:56
maikmertenthe ECP5 example looks promising, but this is iCE4012:56
ZipCPUmaikmerten: Google the iCE40 family handbook, and page 152 or so describes the SB_IO primitives12:57
tpbTitle: ice40-playground/spi_fast_core.v at master · smunaut/ice40-playground · GitHub (at
tntThat's how I did it in my spi core to force placement of some of the cells without using the sb_io regs.12:57
maikmertenZipCPU, I got the handbook :-)12:57
maikmertentnt, thanks12:58
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!)13:05
tntmaikmerten: your sram controller is a bit weird ... I mean registering the wishbone output data on the negative edge ....13:10
ZipCPUmaikmerten: Can I quote you on that on twitter?  ;)13:11
tntpretty sure all wishbone signals are supposed to be synced to the same edge.13:11
ZipCPUtnt: Did you post the code in question?13:11
ZipCPU... or is it posted?13:12
tpbTitle: spu32/sram512kx8_wb8_vga.v at master · maikmerten/spu32 · GitHub (at
*** jevinskie has joined #yosys13:13
* ZipCPU opens tnt's link13:26
ZipCPUYeah, WB is supposed to be single edge of a clock only13:26
ZipCPUGood catch, tnt13:27
ZipCPUThe 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 not13:27
tntit can13:28
ZipCPUSo ... it can properly reason about the timing of both edges of the clock?13:29
tntarachne and icetime couln't.  Well ... it couldn't do a proper timing analysis, the bitstream would be correct.13:29
tntnextpnr can analyze the half clock cycle just fine.13:29
* ZipCPU downloads the code, adjusts the "input" declarations to be "input wire" declarations13:32
maikmertenZipCPU, if you like to ;-)13:33
maikmertenyeah, nextpnr can properly reason posedege <-> negedge timing wise13:34
*** jevinskie has quit IRC13:40
maikmerten(the reason for sampling the sram data on the negedge is that I need the data to be available on the following posedge)13:45
*** vonnieda has quit IRC13:46
maikmertenand given how the Wishbone spec illustrates "FASM" memory interfacing, the bus device can change output data somewhere between positive clock edges13:46
maikmerten(as long as the data is stable for read on the positive edge)13:47
maikmerten(c.f. llustration 8-14: Simple 16 x 8-bit SLAVE memory of the WB b4 spec, page 111)13:47
*** rohitksingh_work has quit IRC13:48
maikmertenso I figured that presenting new output data "somewhere" could just as well be "exactly in the middle between posedges, which happens to be negedge)13:48
ZipCPUUsually, that only slows down your design13:49
maikmertenit does :-)13:49
ZipCPUHow about I_data ... is that clock synchronous at all?  (Probably not, right?)13:49
maikmertennot exactly in that spot in that design though ;-)13:49
maikmertenno, I_data happens to be valid after the SRAM access time13:51
maikmerten(so asynchronous)13:51
maikmertenso O_wb_data could just be wired to I_data (from SRAM)13:53
maikmertenbut I'm somewhat worried that I_data will become invalid when new requests arrive, which is why I stuff the data into registers13:54
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)13:55
maikmertenso applying a new address and reading data on the same clock edge seems dangerous to me13:56
* maikmerten looks into SRAM data sheet13:56
maikmertenyeah, t_DH (data hold) is specced at "min 0"13:57
tntWhat's the sram model ?13:58
ZipCPUmaikmerten: So ... things look something like this?
tpbTitle: Imgur: The magic of the Internet (at
maikmertenZipCPU, that looks right14:01
maikmertentnt, as in "model number" (that'd be AS7C34096A) or as in "abstract operational concept"?14:02
tntyeah p/n14:02
maikmertenah, k14:02
tntwhich speed grade ?14:02
maikmertenit's a standard 10ns 512Kx8 asynchronous RAM14:02
maikmerten(well, whatever "standard" means. I've seen alternative parts with the same specs, pin layout and overall timing from other vendors, too)14:03
*** vonnieda has joined #yosys14:04
maikmertenokay, gotta fetch an appointment, cya later!14:12
*** maikmerten has quit IRC14:12
*** vid has quit IRC14:23
*** vid has joined #yosys14:25
*** rohitksingh has joined #yosys14:31
*** jakobwenzel has quit IRC14:53
*** vonnieda has quit IRC14:53
*** vonnieda has joined #yosys15:05
*** emeb has joined #yosys15:30
*** vid has quit IRC15:32
*** maikmerten has joined #yosys15:39
*** rohitksingh has quit IRC15:39
*** rohitksingh has joined #yosys15:43
*** Jybz has quit IRC15:51
tpbTitle: fwb_slave.v · GitHub (at
ZipCPUThat checks the WB interface.  It's also what I used to generate the cover statement I sent earlier16:01
maikmertenZipCPU, wow, that's so cool!16:01
ZipCPUTo "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 core16:02
ZipCPUNormally, 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 did16:04
ZipCPUYou can read more about formally verifying memory things here if you are interested:
tpbTitle: Formally Verifying Memory and Cache Components (at
maikmertenthe f_ prefix is for "formal"?16:10
*** emeb_mac has joined #yosys16:13
*** Jybz has joined #yosys16:17
ZipCPUYes, though it is only a convention I use16:22
*** m4ssi has quit IRC16:26
maikmertenconventions are plenty fine ;-)16:30
maikmertenokay, sby sure creates quite some output16:33
ZipCPUIt should create two directories16:35
ZipCPUIf any assertion fails, that will show up in the *_prf/engine_0/ directory16:35
ZipCPUThe example trace will show up in the *_cvr/engine_0/ directory16:36
maikmertenyup, two directories there are16:36
ZipCPUThat'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)16:37
maikmertenso,  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.16:42
maikmertenand that is the cover: SBY 18:32:12 [sram512kx8_wb8_vga_cvr] summary: engine_0 (smtbmc) returned PASS16:43
maikmertenthat auto-generated testbench with the system stimulus is pretty neat16:47
*** jevinskie has joined #yosys16:47
maikmertenokay, tying O_wb_ack to zero nicely leads to a FAIL, so that's nice as well ;-)16:49
maikmerten(I'm currently in a "new toys, new toys!" mode)16:50
*** janrinze has quit IRC16:56
ZipCPUThe cover summary means it was able to make the cover() statements true16:58
ZipCPUYou 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 though16:58
maikmertenyup, I see one cover() statement and one trace17:01
*** jevinskie has quit IRC17:17
*** jevinskie has joined #yosys17:23
*** rohitksingh has quit IRC17:30
*** fsasm has quit IRC17:30
*** jevinskie has quit IRC17:32
*** gnufan_home has joined #yosys17:40
*** rohitksingh has joined #yosys17:46
*** rohitksingh has quit IRC17:59
*** rohitksingh has joined #yosys18:02
*** dys has joined #yosys18:18
*** rohitksingh has quit IRC18:22
*** rohitksingh has joined #yosys18:24
*** rohitksingh has quit IRC18:42
*** rohitksingh has joined #yosys18:56
*** proteusguy has quit IRC19:23
maikmertenone example of a register being far away from the SB_IO driven by it:
tpbTitle: Pasteboard - Uploaded Image (at
tntimage not found ?19:27
maikmertenhmm, works for me19:28
maikmertensame picture, different hoster:
maikmertenI can imagine the timing gettin pretty skewed there, especially as other address lines have registers somewhat closer19:30
*** rohitksingh has quit IRC19:31
tntheh, yeah.19:33
*** maikmerten has quit IRC20:00
tntZipCPU: is there no way to access registers from submodules during formal checks ?20:08
ZipCPUNot in the open version20:08
tntI need to assert on the content of a ram ... but that ram is a submodule ...20:08
ZipCPUThe way around that is to create a port, used only in formal mode, to pass the information you need around20:09
ZipCPUI had the same problem within the ZipCPU:
tpbTitle: zipcpu/zipcpu.v at master · ZipCPU/zipcpu · GitHub (at
tntoh well ... it was a fun experiment.20:11
*** s_frit has joined #yosys20:13
ZipCPUThat 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 on20:13
daveshahThere's probably a way to do it with clever use of the expose command in the Yosys script20:13
ZipCPUdaveshah: If the first was ew, that's gotta be a double eww!20:16
*** s_frit has quit IRC21:26
*** s_frit has joined #yosys21:26
*** dys has quit IRC21:59
*** gnufan_home has quit IRC22:27
*** vonnieda has quit IRC23:00
*** Jybz has quit IRC23:12

Generated by 2.13.1 by Marius Gedminas - find it at!