<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: 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.
<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>
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>
(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"
<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
<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