| *** tpb has joined #yosys | 00:00 | |
| *** vonnieda has joined #yosys | 02:09 | |
| *** gsi_ has joined #yosys | 02:11 | |
| *** gsi__ has quit IRC | 02:14 | |
| *** PyroPeter has quit IRC | 02:52 | |
| *** PyroPeter has joined #yosys | 03:05 | |
| *** citypw has joined #yosys | 03:46 | |
| *** proteusguy has joined #yosys | 04:18 | |
| *** rohitksingh_work has joined #yosys | 04:49 | |
| *** emeb_mac has quit IRC | 07:14 | |
| *** citypw has quit IRC | 07:41 | |
| *** vid has joined #yosys | 08:02 | |
| *** Jybz has joined #yosys | 08:32 | |
| *** futarisIRCcloud has joined #yosys | 08:42 | |
| *** fsasm has joined #yosys | 08:48 | |
| *** jevinskie has joined #yosys | 09:17 | |
| *** m4ssi has joined #yosys | 09:40 | |
| *** jevinskie has quit IRC | 09:49 | |
| *** Ultrasauce has quit IRC | 10:31 | |
| *** Ultrasauce has joined #yosys | 10:32 | |
| *** jevinskie has joined #yosys | 10:39 | |
| *** futarisIRCcloud has quit IRC | 11:01 | |
| tnt | Ok, I think my proof is good now (it passes and actually proves stuff :p) https://pastebin.com/rLGqiTXL | 11:11 |
|---|---|---|
| tpb | Title: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - Pastebin.com (at pastebin.com) | 11:11 |
| *** jevinskie has quit IRC | 11:12 | |
| *** tlwoerner has quit IRC | 12:20 | |
| *** citypw has joined #yosys | 12:22 | |
| *** tlwoerner has joined #yosys | 12:35 | |
| *** maikmerten has joined #yosys | 12:35 | |
| 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 | 12:37 |
| maikmerten | CMakeError.log doesn't contain any mentioning of python | 12:38 |
| tnt | ZipCPU: arf ... cover(f_was_full && f_empty); | 12:39 |
| tnt | ZipCPU: it's cheating ... its asserting reset to go back to empty :) | 12:39 |
| 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 | 12:39 |
| ZipCPU | tnt: Adjust the f_was_full flag so that it clears on reset | 12:39 |
| tnt | ZipCPU: yeah, I figured, I just found it sneaky :) | 12:41 |
| 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. | 12:46 |
| ZipCPU | maikmerten: 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 |
| ZipCPU | It sounds, though, like you have an SRAM problem of which I/O drivers are one possibility | 12:47 |
| ZipCPU | How are you currently handling the SRAM I/Os? | 12:47 |
| ZipCPU | Inferred? | 12:47 |
| maikmerten | aye. No constraints whatsoever. | 12:48 |
| tnt | maikmerten: what frequency are you running that sram at ? | 12:48 |
| maikmerten | 25.125 MHz | 12:48 |
| 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. | 12:48 |
| maikmerten | I'm ambitiously driving things without waitstates | 12:49 |
| ZipCPU | Have you tried directly instantiating the SB_IO elements? | 12:49 |
| tnt | (and put registers in them ...) | 12:50 |
| maikmerten | not yet | 12:51 |
| ZipCPU | Got it | 12:51 |
| ZipCPU | Feel free to keep us all posted here, I'd love to hear how it's going | 12:52 |
| 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" | 12:52 |
| ZipCPU | No? | 12:52 |
| ZipCPU | I can help with that if you need it | 12:52 |
| * ZipCPU looks up the manual describing SB_IO's | 12:52 | |
| maikmerten | thanks for your kind helpfulness :-) | 12:52 |
| maikmerten | oh, I'm instantiating SB_IOs already | 12:52 |
| * ZipCPU hasn't helped ... yet ;) | 12:53 | |
| maikmerten | in the toplevel of my design to get reliable tristate working | 12:53 |
| maikmerten | https://github.com/maikmerten/spu32/blob/master/boards/hx8k-breakout/top.v <-- ca. lines 290 | 12:53 |
| 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. | 12:53 |
| tpb | Title: spu32/top.v at master · maikmerten/spu32 · GitHub (at github.com) | 12:53 |
| maikmerten | tnt, 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 |
| ZipCPU | Ok, the SB_IOs are described in the iCE40FamilyHandbook.pdf | 12:54 |
| tnt | 110100 is what you want | 12:55 |
| 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 | 12:55 |
| tpb | Title: nextpnr/constraints.md at master · YosysHQ/nextpnr · GitHub (at github.com) | 12:55 |
| tnt | (that registers the input path and the output data and output enable) | 12:55 |
| maikmerten | like "sram_address[0] - place that in <wherever>" | 12:55 |
| tnt | maikmerten: unless you manually instanciate the DFF you won't be able to put the constraint on the right object. | 12:56 |
| maikmerten | the ECP5 example looks promising, but this is iCE40 | 12:56 |
| ZipCPU | maikmerten: Google the iCE40 family handbook, and page 152 or so describes the SB_IO primitives | 12:57 |
| tnt | https://github.com/smunaut/ice40-playground/blob/master/cores/spi_slave/rtl/spi_fast_core.v#L274 | 12:57 |
| tpb | Title: ice40-playground/spi_fast_core.v at master · smunaut/ice40-playground · GitHub (at github.com) | 12:57 |
| 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. | 12:57 |
| maikmerten | ZipCPU, I got the handbook :-) | 12:57 |
| maikmerten | tnt, thanks | 12:58 |
| maikmerten | *starred* | 12: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 |
| tnt | maikmerten: your sram controller is a bit weird ... I mean registering the wishbone output data on the negative edge .... | 13:10 |
| ZipCPU | maikmerten: Can I quote you on that on twitter? ;) | 13:11 |
| tnt | pretty sure all wishbone signals are supposed to be synced to the same edge. | 13:11 |
| ZipCPU | tnt: Did you post the code in question? | 13:11 |
| ZipCPU | ... or is it posted? | 13:12 |
| tnt | https://github.com/maikmerten/spu32/blob/master/ram/sram512kx8_wb8_vga.v | 13:13 |
| tpb | Title: spu32/sram512kx8_wb8_vga.v at master · maikmerten/spu32 · GitHub (at github.com) | 13:13 |
| *** jevinskie has joined #yosys | 13:13 | |
| * ZipCPU opens tnt's link | 13:26 | |
| ZipCPU | Yeah, WB is supposed to be single edge of a clock only | 13:26 |
| ZipCPU | Good catch, tnt | 13:27 |
| 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 | 13:27 |
| tnt | it can | 13:28 |
| ZipCPU | So ... it can properly reason about the timing of both edges of the clock? | 13:29 |
| tnt | arachne and icetime couln't. Well ... it couldn't do a proper timing analysis, the bitstream would be correct. | 13:29 |
| tnt | nextpnr can analyze the half clock cycle just fine. | 13:29 |
| * ZipCPU downloads the code, adjusts the "input" declarations to be "input wire" declarations | 13:32 | |
| maikmerten | ZipCPU, if you like to ;-) | 13:33 |
| maikmerten | yeah, nextpnr can properly reason posedege <-> negedge timing wise | 13:34 |
| *** jevinskie has quit IRC | 13: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 IRC | 13:46 | |
| maikmerten | and given how the Wishbone spec illustrates "FASM" memory interfacing, the bus device can change output data somewhere between positive clock edges | 13: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 IRC | 13:48 | |
| 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) | 13:48 |
| ZipCPU | Usually, that only slows down your design | 13:49 |
| maikmerten | it does :-) | 13:49 |
| ZipCPU | How about I_data ... is that clock synchronous at all? (Probably not, right?) | 13:49 |
| maikmerten | not exactly in that spot in that design though ;-) | 13:49 |
| maikmerten | no, I_data happens to be valid after the SRAM access time | 13:51 |
| maikmerten | (so asynchronous) | 13:51 |
| maikmerten | so O_wb_data could just be wired to I_data (from SRAM) | 13:53 |
| 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 | 13: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 |
| maikmerten | so applying a new address and reading data on the same clock edge seems dangerous to me | 13:56 |
| * maikmerten looks into SRAM data sheet | 13:56 | |
| maikmerten | yeah, t_DH (data hold) is specced at "min 0" | 13:57 |
| tnt | What's the sram model ? | 13:58 |
| ZipCPU | maikmerten: So ... things look something like this? https://imgur.com/a/pAU6fko | 13:58 |
| tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 13:58 |
| maikmerten | ZipCPU, that looks right | 14:01 |
| maikmerten | tnt, as in "model number" (that'd be AS7C34096A) or as in "abstract operational concept"? | 14:02 |
| tnt | yeah p/n | 14:02 |
| maikmerten | ah, k | 14:02 |
| tnt | which speed grade ? | 14:02 |
| maikmerten | it's a standard 10ns 512Kx8 asynchronous RAM | 14: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 #yosys | 14:04 | |
| maikmerten | okay, gotta fetch an appointment, cya later! | 14:12 |
| *** maikmerten has quit IRC | 14:12 | |
| *** vid has quit IRC | 14:23 | |
| *** vid has joined #yosys | 14:25 | |
| *** rohitksingh has joined #yosys | 14:31 | |
| *** jakobwenzel has quit IRC | 14:53 | |
| *** vonnieda has quit IRC | 14:53 | |
| *** vonnieda has joined #yosys | 15:05 | |
| *** emeb has joined #yosys | 15:30 | |
| *** vid has quit IRC | 15:32 | |
| *** maikmerten has joined #yosys | 15:39 | |
| *** rohitksingh has quit IRC | 15:39 | |
| *** rohitksingh has joined #yosys | 15:43 | |
| *** Jybz has quit IRC | 15:51 | |
| ZipCPU | maikmerten: https://gist.github.com/ZipCPU/6f026f6925314f3f5462b80ada013ee5 | 16:00 |
| tpb | Title: fwb_slave.v · GitHub (at gist.github.com) | 16:00 |
| ZipCPU | That checks the WB interface. It's also what I used to generate the cover statement I sent earlier | 16:01 |
| maikmerten | ZipCPU, wow, that's so cool! | 16:01 |
| 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 | 16:02 |
| 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 | 16:04 |
| ZipCPU | You can read more about formally verifying memory things here if you are interested: http://zipcpu.com/zipcpu/2018/07/13/memories.html | 16:05 |
| tpb | Title: Formally Verifying Memory and Cache Components (at zipcpu.com) | 16:05 |
| maikmerten | the f_ prefix is for "formal"? | 16:10 |
| *** emeb_mac has joined #yosys | 16:13 | |
| *** Jybz has joined #yosys | 16:17 | |
| ZipCPU | Yes, though it is only a convention I use | 16:22 |
| *** m4ssi has quit IRC | 16:26 | |
| maikmerten | conventions are plenty fine ;-) | 16:30 |
| maikmerten | okay, sby sure creates quite some output | 16:33 |
| ZipCPU | It should create two directories | 16:35 |
| ZipCPU | If any assertion fails, that will show up in the *_prf/engine_0/ directory | 16:35 |
| ZipCPU | The example trace will show up in the *_cvr/engine_0/ directory | 16:36 |
| maikmerten | yup, two directories there are | 16:36 |
| 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) | 16:37 |
| 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. | 16:42 |
| maikmerten | and that is the cover: SBY 18:32:12 [sram512kx8_wb8_vga_cvr] summary: engine_0 (smtbmc) returned PASS | 16:43 |
| maikmerten | that auto-generated testbench with the system stimulus is pretty neat | 16:47 |
| *** jevinskie has joined #yosys | 16:47 | |
| maikmerten | okay, 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 IRC | 16:56 | |
| ZipCPU | ;) | 16:57 |
| ZipCPU | The cover summary means it was able to make the cover() statements true | 16:58 |
| 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 | 16:58 |
| maikmerten | yup, I see one cover() statement and one trace | 17:01 |
| *** jevinskie has quit IRC | 17:17 | |
| *** jevinskie has joined #yosys | 17:23 | |
| *** rohitksingh has quit IRC | 17:30 | |
| *** fsasm has quit IRC | 17:30 | |
| *** jevinskie has quit IRC | 17:32 | |
| *** gnufan_home has joined #yosys | 17:40 | |
| *** rohitksingh has joined #yosys | 17:46 | |
| *** rohitksingh has quit IRC | 17:59 | |
| *** rohitksingh has joined #yosys | 18:02 | |
| *** dys has joined #yosys | 18:18 | |
| *** rohitksingh has quit IRC | 18:22 | |
| *** rohitksingh has joined #yosys | 18:24 | |
| *** rohitksingh has quit IRC | 18:42 | |
| *** rohitksingh has joined #yosys | 18:56 | |
| *** proteusguy has quit IRC | 19:23 | |
| maikmerten | one example of a register being far away from the SB_IO driven by it: https://pasteboard.co/If9QJEz.png | 19:27 |
| tpb | Title: Pasteboard - Uploaded Image (at pasteboard.co) | 19:27 |
| tnt | image not found ? | 19:27 |
| maikmerten | hmm, works for me | 19:28 |
| maikmerten | same picture, different hoster: http://pasteall.org/pic/show.php?id=b232b0317c40f9a25a5ce0e17ad9cb6d | 19:29 |
| maikmerten | I can imagine the timing gettin pretty skewed there, especially as other address lines have registers somewhat closer | 19:30 |
| *** rohitksingh has quit IRC | 19:31 | |
| tnt | heh, yeah. | 19:33 |
| maikmerten | http://pasteall.org/pic/show.php?id=b2661bd7070ec7715e931fd3bdb81189 | 19:44 |
| tnt | :) | 19:51 |
| *** maikmerten has quit IRC | 20:00 | |
| tnt | ZipCPU: is there no way to access registers from submodules during formal checks ? | 20:08 |
| ZipCPU | Not in the open version | 20:08 |
| tnt | I need to assert on the content of a ram ... but that ram is a submodule ... | 20:08 |
| ZipCPU | The way around that is to create a port, used only in formal mode, to pass the information you need around | 20:09 |
| tnt | iew | 20:09 |
| ZipCPU | Yeah | 20:09 |
| ZipCPU | I had the same problem within the ZipCPU: https://github.com/ZipCPU/zipcpu/blob/master/rtl/core/zipcpu.v | 20:09 |
| tpb | Title: zipcpu/zipcpu.v at master · ZipCPU/zipcpu · GitHub (at github.com) | 20:09 |
| tnt | oh well ... it was a fun experiment. | 20:11 |
| *** s_frit has joined #yosys | 20:13 | |
| 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 | 20:13 |
| daveshah | There's probably a way to do it with clever use of the expose command in the Yosys script | 20:13 |
| ZipCPU | daveshah: If the first was ew, that's gotta be a double eww! | 20:16 |
| *** s_frit has quit IRC | 21:26 | |
| *** s_frit has joined #yosys | 21:26 | |
| *** dys has quit IRC | 21:59 | |
| *** gnufan_home has quit IRC | 22:27 | |
| *** vonnieda has quit IRC | 23:00 | |
| *** Jybz has quit IRC | 23:12 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!
