Friday, 2019-02-08

*** tpb has joined #yosys00:00
promach_finnb : use your own local installed iverilog01:06
promach_finnb: if I use reg [(NUM_OF_INTERMEDIATE_LAYERS-1):0] middle_layers [0:(SMALLER_WIDTH-1)] [(A_WIDTH+B_WIDTH-1):0]; , yosys-smtbmc gives me out-of-bound array access warnings01:08
promach_ZipCPU: is it true that yosys-smtbmc does not support  reg [A-1:0][B-1:0][C-1:0] array;   ?01:25
ZipCPUyosys gives you the error, or yosys-smtbmc?01:27
promach_ZipCPU: sby01:28
ZipCPUSigh.  That doesn't answer the question.  To my knowledge, yosys itself doesn't support multi-dimensional arrays01:28
promach_ZipCPU: ok, so I cannot do formal verification of this code using sby ?01:29
ZipCPUI'm not even sure the SMT format supports multidimensional memories01:29
ZipCPUPerhaps this isn't a memory?01:30
promach_huh ? it is still a 3d array, whether it is memory or not01:32
promach_ZipCPU: I thought the only difference noticeable by the tool is either the array is packed or unpacked01:33
*** promach_ has quit IRC01:36
*** emeb_mac has joined #yosys01:42
*** emeb has quit IRC01:49
*** X-Scale` has joined #yosys02:00
*** X-Scale has quit IRC02:01
*** X-Scale` is now known as X-Scale02:01
*** gsi_ has joined #yosys02:26
*** gsi__ has quit IRC02:29
*** xdeller_ has quit IRC03:04
*** xdeller_ has joined #yosys03:05
*** proteusguy has joined #yosys03:37
*** leviathanch has joined #yosys03:49
*** jevinskie has joined #yosys04:08
*** rohitksingh_work has joined #yosys04:30
*** pie__ has joined #yosys04:37
*** pie___ has quit IRC04:41
*** dys has quit IRC06:44
*** emeb_mac has quit IRC06:57
*** dys has joined #yosys08:07
*** rohitksingh_work has quit IRC08:08
*** rohitksingh_work has joined #yosys08:09
*** dys has quit IRC08:22
*** m4ssi has joined #yosys08:57
*** X-Scale` has joined #yosys09:07
*** X-Scale has quit IRC09:09
*** X-Scale` is now known as X-Scale09:09
*** leviathanch has quit IRC09:21
*** rohitksingh_work has quit IRC11:21
*** rohitksingh has joined #yosys12:13
*** rohitksingh has quit IRC12:58
*** rohitksingh has joined #yosys14:26
somlodaveshah: I haven't taken care of the uart's "back-pressure" wait signal -- in the attosoc setup it effectively stalls the mmio write, but with the rocket, through the layers of AXI interfaces, there's no simple way to do that from where I hooked it up14:32
daveshahI found the problem with the UART. It was actually the PLL's feedback config being wrong, throwing the freq off14:33
somloso we'd have to add some sort of buffering to get all the uart output queued up properly14:33
tpbTitle: GitHub - daveshah1/yoloRISC: porting lowRISC to yosys/nextpnr/trellis on the Lattice ECP5 fpga (at
somloah, I redid the pll and started the compilation last night, then went home -- so I just got back and was going to try it out :)14:33
daveshahCompile time should be down to 15 minutes synth and PnR with that analytic placer PR14:34
somloand yeah, tweet away if you think it's worth it :)14:34
somlowas going to try that today too14:34
somloall we need now is a DRAM controller and we can have a self-hosting Linux computer that can fully recompile its own "hardware"14:35
* sxpert wonders why we keep using Dram on those fpga boards, when srams are so cheap14:41
daveshahsxpert: SRAM is much more expensive for a given capacity14:41
sxpertI see14:41
sxpertand dram is a PITA to work with14:42
daveshahSDRAM is fine14:42
daveshahit's the more modern DRAMs that are a pain (but the fancier modern SRAMs are not super easy either)14:42
daveshahBut largest available SRAM (288Mbit) is ~$300, whereas 1Gbit of DDR3 is ~$3 (single quantity pricing)14:44
daveshahso you can see why DRAM becomes preferable14:44
sxpertah, I see indeed14:45
sxpertI understand that SRAM is much lower power14:46
sxpertso that may be preferable for a portable app14:46
daveshahIn practice large SRAMs are performance optimised and pretty power hungry14:47
daveshahsmartphones manage fine with low power DRAM14:47
sxpertmy app would need about 1MB of ram14:47
daveshahThat is definitely SRAM territory14:48
daveshahor perhaps HyperRAM, which is DRAM with a simpler and lower pin count interface14:48
sxpertfound some at digikey that would fit with 60mA consumption or so, for 5€14:49
daveshahThat seems like a lot of current for SRAM14:50
sxpertor maybe I didn't read that properly ;)14:51
*** Cerpin has joined #yosys14:51
sxpertwas looking at this one
sxpertor that one, don't remember
sxpertdaveshah: anyhow, getting ahead of myself... last night I heeded your advice and rewrote most of the code I had15:07
*** FL4SHK has quit IRC15:15
MoeIcenowydaveshah: does HyperRAM have self-refresh?15:17
daveshahYes, it does15:17
sxpertnot much choice there though15:19
sxpertfunny how that looks strangely similar to what is described in the saturn CPU docs ;)15:21
somlodaveshah: how did you come up with the pll parameters? I just ran ecppll from the command line and got something different (which btw, doesn't work :) )15:24
daveshahI ended up using Diamond15:24
somlooh, fair enough :)15:24
*** rohitksingh has quit IRC15:35
somlodaveshah: what does uart_dbg do on the versa5g?15:47
daveshahThat connects to pin 4 on X3 (EXPCON1), so I could look at the UART with a logic analyser15:47
somlosemi-related: dropping down to 9600 baud helps avoid overwhelming the UART, or was that accomplished just by fixing the pll? (I *still* haven't recompiled it, just studying your changes :)15:51
*** rohitksingh has joined #yosys15:53
somlodaveshah: oh, I see you added a 2000 delay in putchar, that's probably what avoids dealing with the "wait" signal :)15:55
daveshahThe 9600 was a test in case the baud rate accuracy of 115200 at 10MHz was too poor15:57
daveshah115200 should be fine now too15:57
MoeIcenowyhyperram seems to be bga15:58
*** AlexDaniel has joined #yosys15:59
daveshahMoeIcenowy: yeah, if you don't want BGA then QSPI PSRAM is the best bet16:00
*** rohitksingh has quit IRC16:17
*** finnb has joined #yosys16:26
finnbAny idea what this yosys error message means?16:27
tpbTitle: ERROR: Found error in internal cell \mandelbrot.$lt$projects/mandelbrot/hdl/mand - (at
daveshahfinnb: Seems to be signedness related16:29
tpbTitle: yosys/ at master · YosysHQ/yosys · GitHub (at
daveshahquite possibly an internal bug in the frontend or optimisation16:30
finnbI basically have a value which is "if foo > -BAR" where localparam BAR = $sqrt(BAZ)16:36
finnbwhere foo is a signed register16:36
finnbI can solve it if I calculate manually what BAR is16:36
finnbi.e BAR = 6416:37
ddrownwhat about -1*BAR16:42
finnbOnly seems a problem when using $sqrt16:49
daveshahLet me have a look16:49
daveshahSeems like a Yosys bug16:49
tpbTitle: escaped_i[0] <= ((im + im_c_pipe[WIDTH + 1]) > MAX_SQUARE) - (at
finnbthat's the actual part which fails16:56
finnbwhere MAX_SQUARE is -BAR in my example16:57
daveshahfinnb: I've created
tpbTitle: "Found error in internal cell" when comparing signed against negated square root · Issue #807 · YosysHQ/yosys · GitHub (at
finnbThanks :)17:01
finnbso it wasn't just me then17:01
cr1901_modernExcellent daveshah :) Unfortunately I kinda forgot why I wanted this in the first place (it's been a busy month) :P17:13
tpbTitle: ecp5: Embed baseconfigs in nextpnr by daveshah1 · Pull Request #228 · YosysHQ/nextpnr · GitHub (at
*** m4ssi has quit IRC17:14
*** jevinskie has quit IRC17:29
*** finnb has quit IRC17:34
*** rohitksingh has joined #yosys18:45
*** m4ssi has joined #yosys18:55
*** m4ssi has quit IRC18:56
*** rohitksingh has quit IRC19:00
*** m4ssi has joined #yosys19:03
*** m4ssi has quit IRC20:09
somlodaveshah: after getting derailed several times by unrelated dayjob stuff, I finally managed to test the rocket-chip blinky bitstream, and (spoiler alert) -- it works! :)21:29
somloamazing how I could just throw rocket at yosys/trellis/nextpnr and it "Just Worked", practically out of the box -- awesome toolchain, many thanks for your hard work on it!!!21:30
daveshahThanks for your work getting this running too!21:31
somlonext on the agenda is for me to take nextpnr PR#219 for a spin, and report back some additional before/after run time datapoints21:33
*** dys has joined #yosys21:43
sxpertI have 2 20 bits reg, how can I do an unsigned >= ?22:05
*** mjoldfield has quit IRC22:19
ZipCPUsxpert: The same way as always?23:12
ZipCPUI must be missing something23:12
sxpertnah, I was ;-)23:15
sxpertthe thing ended up being replaced with a bunch of assign and wires23:15
sxpertand substractions, grabbing the carry23:17
ZipCPUCool!  You are on your way23:17
* ZipCPU is writing a blog article about how fast a CPU can toggle a GPIO pin23:17
tpbTitle: hp-saturn/hp48_02_sys_ram.v at master · sxpert/hp-saturn · GitHub (at
sxpertsee here ;-)23:18
ZipCPUAre you working off your own bus standard, or one of the ones I'm less familiar with?23:18
sxpertZipCPU: I'm replicating an HP48, so I'm replicating the bus it uses internally23:19
ZipCPUYou know what I'm going to recommend, right?  ;)23:20
ZipCPUI'm going to recommend you build a file containing formal properties associated with any bus interaction.  You can then include that file in any design that interacts with the bus and verify that the bus acts "appropriately" (whatever that means)23:20
ZipCPUIt's an easy/cheap bang for your buck, and one of the easiest and most useful bits of formal to do23:21
sxpertoh, I rewrote the thing from scratch over the evening last night23:21
ZipCPUAdd in the formal properties .... you'll go faster23:22
sxpertand separated bus and decoder as much as possible23:22
sxpertit was going faster at last compile, 120Mhz or so23:22
ZipCPUWhich chip?  iCE40?23:22
ZipCPUHave you ever tried the formal tools?23:23
ZipCPUYour missing a real treat23:23
ZipCPUIf you save them for later, though, you'll be missing out on their biggest utility23:24
ZipCPUSome folks like the idea of building a design, then verifying it.  On the other hand, if you use formal while building your design, it gets a whole lot easier to design23:24
sxpertmy formal method is paper & pen23:24
sxpertand lots of scribbling23:24
ZipCPUMine used to be a test bench wrapper and simulation.  Then I tried formal, and realized how many bugs I'd been missing.23:25
ZipCPUAfter getting *REALLY* burned by some ugly bugs that were painful to find in hardware, I've been starting with formal.  *Especially* for any sort of bus interaction.23:25
sxpertwell the bus interaction is entirely inside the fpga, between modules23:26
sxpertnot with outside things for now23:26
ZipCPUWell, both23:26
ZipCPUThe problem with a bus bug is that it tends to cause the design to freeze and lock up hard, leaving you with no idea what just happened23:26
ZipCPUGetting unstuck from there can take a lot of work.  Formal can keep that from happening in the first place23:27
sxpertI did the classic 4 phase clocking here23:27
ZipCPUHere, try this bug story out for size:
tpbTitle: Mystery post: The ugliest bug I've ever encountered (at
ZipCPUSee if you can guess where the bug was (it's revealed at the end)23:28
sxpertI see23:43
ZipCPUSince writing that, I discovered formal.  Finding and fixing that bug was quite painful.  I prefer avoiding such pain, if at all possible.  ;)23:44
sxpertwell, nextpnr complains about there beeing combinatorial loops...23:44
sxpertlast time around it was using 600 slices, it uses 43000 now, wtf ?23:47
ZipCPUWhat uses 43k?  Your design?23:47
ZipCPUCheck your multiplies23:47
sxpertno multiplies23:48
ZipCPUThat and any block RAM23:48
sxpertthat may be the issue23:48
sxpertI have reg     [3:0]sys_ram [0:SYS_RAM_LEN - 1];23:48
ZipCPUHow big is SYS_RAM_LEN/23:48
sxpertnormally should be 256k 4 bit values23:49
sxpertI limited to 64k at this time23:49
ZipCPUOh, and why only 4-bits wide?  Some block RAM's (iCE40) have a minimum width of 16 bits or so23:49
sxpertoh !23:49
daveshahECP5 BRAM are fine at 4 bits23:50
daveshahI'm pretty sure iCE40 are too23:50
daveshahIt's bitstream configurable23:50
sxpertguess it didn't generate blockrams for that23:50
ZipCPUdaveshah: Do you remember what some of the block RAM synthesis problems are that someone might find with an ECP5?23:51
sxpertis there a magic incantation ?23:51
daveshahThe most common problem would be more than one write port23:51
daveshahOr possibly excessively complex read/write enable logic23:51
ZipCPUDo the write and read ports need to share a common address?23:51
daveshahNot in the modes that Yosys supports23:52
sxpertdaveshah: all writes are in the same always ()23:52
sxpertat only one location even23:52
daveshahIn that case it's probably
tpbTitle: Yosys fails to infer BRAM with complex enable logic · Issue #710 · YosysHQ/yosys · GitHub (at
daveshahLooking at your code the BRAM access is deep inside a state machine23:53
ZipCPUOk, that's the problem23:53
daveshahYosys can struggle with that sometimes23:53
ZipCPUYou can't place multiple block RAM reads from the same block RAM into an always block23:53
sxpertI see23:54
* sxpert refactors23:54
* sxpert adds more enable wires23:56
ZipCPUsxpert: Check out the basic block RAM rules in this tutorial file:
tpbTitle: Mystery post: The ugliest bug I've ever encountered (at
ZipCPUSorry, wrong link23:58
ZipCPURule #3: Don't put a RAM in a cascaded if (or case statement for that matter)23:59
ZipCPURule #5: Don't put a RAM in a block with other things--not all synthesizers can handle it23:59

Generated by 2.13.1 by Marius Gedminas - find it at!