<promach_>
finnb : use your own local installed iverilog
<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 warnings
<promach_>
ZipCPU: is it true that yosys-smtbmc does not support reg [A-1:0][B-1:0][C-1:0] array; ?
<ZipCPU>
yosys gives you the error, or yosys-smtbmc?
<promach_>
ZipCPU: sby
<ZipCPU>
Sigh. That doesn't answer the question. To my knowledge, yosys itself doesn't support multi-dimensional arrays
<promach_>
ZipCPU: ok, so I cannot do formal verification of this code using sby ?
<ZipCPU>
I'm not even sure the SMT format supports multidimensional memories
<ZipCPU>
Perhaps this isn't a memory?
<promach_>
huh ? it is still a 3d array, whether it is memory or not
<promach_>
ZipCPU: I thought the only difference noticeable by the tool is either the array is packed or unpacked
promach_ has quit [Quit: WeeChat 2.3]
emeb_mac has joined #yosys
emeb has quit [Quit: Leaving.]
X-Scale` has joined #yosys
X-Scale has quit [Ping timeout: 240 seconds]
X-Scale` is now known as X-Scale
gsi_ has joined #yosys
gsi__ has quit [Ping timeout: 245 seconds]
xdeller_ has quit [Read error: Connection reset by peer]
xdeller_ has joined #yosys
proteusguy has joined #yosys
leviathanch has joined #yosys
jevinskie has joined #yosys
rohitksingh_work has joined #yosys
pie__ has joined #yosys
pie___ has quit [Ping timeout: 245 seconds]
dys has quit [Ping timeout: 240 seconds]
emeb_mac has quit [Ping timeout: 245 seconds]
dys has joined #yosys
rohitksingh_work has quit [Read error: Connection reset by peer]
rohitksingh_work has joined #yosys
dys has quit [Ping timeout: 244 seconds]
m4ssi has joined #yosys
X-Scale` has joined #yosys
X-Scale has quit [Ping timeout: 246 seconds]
X-Scale` is now known as X-Scale
leviathanch has quit [Remote host closed the connection]
rohitksingh_work has quit [Read error: Connection reset by peer]
rohitksingh has joined #yosys
rohitksingh has quit [Read error: Connection reset by peer]
rohitksingh has joined #yosys
<somlo>
daveshah: 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 up
<daveshah>
I found the problem with the UART. It was actually the PLL's feedback config being wrong, throwing the freq off
<somlo>
so we'd have to add some sort of buffering to get all the uart output queued up properly
<sxpert>
funny how that looks strangely similar to what is described in the saturn CPU docs ;)
<somlo>
daveshah: 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 :) )
<daveshah>
I ended up using Diamond
<somlo>
oh, fair enough :)
rohitksingh has quit [Ping timeout: 246 seconds]
<somlo>
daveshah: what does uart_dbg do on the versa5g?
<daveshah>
That connects to pin 4 on X3 (EXPCON1), so I could look at the UART with a logic analyser
<somlo>
semi-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 :)
rohitksingh has joined #yosys
<somlo>
daveshah: oh, I see you added a 2000 delay in putchar, that's probably what avoids dealing with the "wait" signal :)
<daveshah>
The 9600 was a test in case the baud rate accuracy of 115200 at 10MHz was too poor
<daveshah>
115200 should be fine now too
<MoeIcenowy>
oops
<MoeIcenowy>
hyperram seems to be bga
AlexDaniel has joined #yosys
<daveshah>
MoeIcenowy: yeah, if you don't want BGA then QSPI PSRAM is the best bet
rohitksingh has quit [Ping timeout: 245 seconds]
finnb has joined #yosys
<finnb>
Any idea what this yosys error message means?
<tpb>
Title: "Found error in internal cell" when comparing signed against negated square root · Issue #807 · YosysHQ/yosys · GitHub (at github.com)
<finnb>
Thanks :)
<finnb>
so it wasn't just me then
<cr1901_modern>
Excellent daveshah :) https://github.com/YosysHQ/nextpnr/pull/228 Unfortunately I kinda forgot why I wanted this in the first place (it's been a busy month) :P
<tpb>
Title: ecp5: Embed baseconfigs in nextpnr by daveshah1 · Pull Request #228 · YosysHQ/nextpnr · GitHub (at github.com)
m4ssi has quit [Remote host closed the connection]
jevinskie has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
finnb has quit [Remote host closed the connection]
rohitksingh has joined #yosys
m4ssi has joined #yosys
m4ssi has quit [Client Quit]
rohitksingh has quit [Ping timeout: 250 seconds]
m4ssi has joined #yosys
m4ssi has quit [Remote host closed the connection]
<somlo>
daveshah: after getting derailed several times by unrelated dayjob stuff, I finally managed to test the rocket-chip blinky bitstream, and (spoiler alert) -- it works! :)
<somlo>
amazing 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!!!
<daveshah>
Awesome
<daveshah>
Thanks for your work getting this running too!
<somlo>
next on the agenda is for me to take nextpnr PR#219 for a spin, and report back some additional before/after run time datapoints
dys has joined #yosys
<sxpert>
I have 2 20 bits reg, how can I do an unsigned >= ?
mjoldfield has quit []
<ZipCPU>
sxpert: The same way as always?
<ZipCPU>
I must be missing something
<sxpert>
nah, I was ;-)
<sxpert>
the thing ended up being replaced with a bunch of assign and wires
<sxpert>
and substractions, grabbing the carry
<ZipCPU>
Cool! You are on your way
* ZipCPU
is writing a blog article about how fast a CPU can toggle a GPIO pin
<ZipCPU>
Are you working off your own bus standard, or one of the ones I'm less familiar with?
<sxpert>
ZipCPU: I'm replicating an HP48, so I'm replicating the bus it uses internally
<ZipCPU>
You know what I'm going to recommend, right? ;)
<sxpert>
nope
<ZipCPU>
I'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)
<ZipCPU>
It's an easy/cheap bang for your buck, and one of the easiest and most useful bits of formal to do
<sxpert>
oh, I rewrote the thing from scratch over the evening last night
<ZipCPU>
Add in the formal properties .... you'll go faster
<sxpert>
and separated bus and decoder as much as possible
<sxpert>
it was going faster at last compile, 120Mhz or so
<ZipCPU>
Which chip? iCE40?
<sxpert>
ESP5
<ZipCPU>
Nice
<ZipCPU>
Have you ever tried the formal tools?
<sxpert>
nope
<ZipCPU>
Your missing a real treat
<sxpert>
hah
<ZipCPU>
If you save them for later, though, you'll be missing out on their biggest utility
<ZipCPU>
Some 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 design
<sxpert>
my formal method is paper & pen
<sxpert>
and lots of scribbling
<ZipCPU>
Mine used to be a test bench wrapper and simulation. Then I tried formal, and realized how many bugs I'd been missing.
<ZipCPU>
After 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.
<sxpert>
well the bus interaction is entirely inside the fpga, between modules
<sxpert>
not with outside things for now
<ZipCPU>
Well, both
<ZipCPU>
The 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 happened
<ZipCPU>
Getting unstuck from there can take a lot of work. Formal can keep that from happening in the first place