<ZipCPU>
You said you verified the timing results with icetime, right?
<cr1901_modern>
yes, both icetime and nextpnr claim to pass
<ZipCPU>
Can you tell what part of the design is failing?
<cr1901_modern>
Either the CPU is not executing insns at all, or it's never reaching the part where it emits chars to the UART
<ZipCPU>
Can you run it in a simulation?
<ZipCPU>
With the same hardware configuration?
<cr1901_modern>
Someone (not me) did yesterday and says it works
<cr1901_modern>
i.e. gets to the UART
<cr1901_modern>
But of course I'm gonna try as well
<cr1901_modern>
Just... juggling 5 different PRs related to this project right now :)
<ZipCPU>
Which UART? USB or external?
<cr1901_modern>
external
<ZipCPU>
Whew, okay.
<sorear>
are you running an exact verilog design / including all toplevel stuff, build scripts, etc / that someone else claims to have working on tinyfpga B2?
<ZipCPU>
Not sure how I'd debug the USB UART.
<cr1901_modern>
sorear: No. I haven't even seen said person's Verilog code. That's why I'm gonna try as well.
<cr1901_modern>
sorear: BUT in the past, I have done such a thing w/ a different softcore, and got a simulation/synthesis mismatch
<cr1901_modern>
even post-synth simulation claimed the design should work
<ZipCPU>
You aren't struggling with the SB_IO bug I tweeted about earlier, now, are you?
<awygle>
ZipCPU: i don't really understand that tweet. it seems to say "don't create a clock in fabric"?
kc5tja has joined #yosys
<kc5tja>
ZipCPU: Greetings!
<sorear>
ohai
<kc5tja>
Hello! Long time no chat.
<ZipCPU>
kc5tja: Long time, no chat!
<awygle>
ohai-yo
<ZipCPU>
kc5tja: My time is yours, now that we figured out the bug ... what's on your agenda?
<kc5tja>
I just got back from the gym, so still stuffing my face with replenishing drink and food. Once that's done, I'm going to add the SB_IO per your recommendation.
<kc5tja>
After *that*, assuming that works as expected, I would like to look into how to add the first steps for FV to the design.
<ZipCPU>
Wonderful!
<kc5tja>
As you indicate, there is an impossible condition detailed in the overall design; we can start with that.
<ZipCPU>
OK, fair enough.
<kc5tja>
Eventually, I'd like to get to a point where I start writing unit tests to cover the "happy paths" (and, thus, providing examples of how to properly use a core as a kind of executable documentation), while using FV to cover the edge-cases that I wouldn't think about myself. If that makes sense. I'm of the opinion that TDD + FV = best coverage possible.
<ZipCPU>
Sure!
<cr1901_modern>
ZipCPU: I don't understand your tweet either
<ZipCPU>
You can use the formal "cover()" statement to get some happy paths as well.
<ZipCPU>
Heheh ... kc5tja, care to explain to cr1901_modern what we hypothesized today?
<ZipCPU>
Here's the problem, cr1901_modern--it's centered around an SPI serial port.
<kc5tja>
Is cr1901_modern aware of my problem?
<ZipCPU>
No. You are welcome to share if you would like.
<cr1901_modern>
If you send a clock out of a port derived from the system clock, it already has to go through an SB_IO?
<sorear>
are you talking about the SB_IO tweet?
<cr1901_modern>
yes
<ZipCPU>
Yes.
<ZipCPU>
To run the serial port, you need to output CS_n, SCK, and MOSI, and then bring MISO back in.
<kc5tja>
Expect typos; the Cherry switches on my Das Keyboard seems to be failing due to lack of use. Possibly oxidation. But, that's not my immediate issue.
<ZipCPU>
If you want to run at full speed, the SCK needs some "special" help getting up to the same speed as the system clock.
<ZipCPU>
You could assign to SCK, as in: SCK = sys_clk & enable.
<sorear>
what happens if you try to run a clock signal out of an ordinary IO?
<ZipCPU>
The problem is, you have no guarantee of where nextpnr will place that data.
<ZipCPU>
That's what I'm describing.
<ZipCPU>
Because you have no control of placement, the delay between the logic within the chip and the external clock is ... uncontrolled.
<sorear>
"sys_clk & enable" sounds like a recipe for glitches to me, since enable is most likely going to change immediately *after* a clk edge when the registers it depends on update
<ZipCPU>
sorear: I've been staring at glitchless traces too long to imagine such bugs ;)
<kc5tja>
Problem I'm having right now: If I synthesize my flash ROM adapter core (ROMA == ROM Adapter) as it's presently written, it works fine -- I can send it READ commands, and it retrieves data back from the flash and deserializes it and puts it on the TileLink bus. My DMA core takes the low 8-bits of each 32-bit word fetched and forwards it to diagnostic LEDs on the icoBoard Gamma (via PMOD1 port), so I can
<kc5tja>
literally see what the flash contents are and compare them against a dump generated via "xxd -g4 -e project.bin".
<ZipCPU>
The subtle bug kc5tja is dealing with is that minor changes in his code take the design from working to non working.
<kc5tja>
HOWEVER, if I alter my code to select any other selection of bits (even if it's just one bit off, say bits 8..1 instead of 7..0), the logic is *just* *different* *enough* that Arachne PNR lays the circuit out differently, which produces different timing relationships.
<cr1901_modern>
Not sure how Xilinx and friends handle this tbh. I know the SPI flash clock pin isn't even accessible from series7
<cr1901_modern>
But sounds like a common problem
<kc5tja>
I expose my SPI clock directly out an I/O pin without any buffering or such, because that's how I've always done it on the Xilinx parts, and it's always "just worked."
<ZipCPU>
Xilinx recommends that if you output a clock, you should do so with their ODDR primitive.
<ZipCPU>
Ever since I upped the speed of my SPI implementations to full speed, I've been using the vendor DDR primitives.
<kc5tja>
Apparently, that's not guaranteed to be the case on Lattice parts. The going hypothesis (which I'll be testing shortly) is that the new route and placement for the clock logic is just different enough that the flash ROM is not synchronized with the *data* coming out of ICE_MOSI pin, leading the flash to receive command byte 01H instead of 03H (the latter of which is READ command).
<ZipCPU>
I think the former is a write enable command ... I looked it up earlier today, just not sure.
<cr1901_modern>
Maybe nextpnr needs a "hey, this clock is derived from another clock, so don't route it all over the place" mode :P
<kc5tja>
So, the work-around appears to be to use SB_IO primitives to either re-synchronize the clock signal that I'm generating, or to cause arachne-pnr to place logic with the constraint that it be proximal to the output pin, thus guaranteeing a more precise timing relationship.
<kc5tja>
ZipCPU: Is that a good summary?
<ZipCPU>
cr1901_modern: Maybe. I've thought about adding such.
<ZipCPU>
Yeah, that's about right. There's also the positive edge vs negative edge issue that's different between our implementations.
<ZipCPU>
I'm not quite certain what to make of that.
<cr1901_modern>
Is there a "deterministic mode" for nextpnr?
<sorear>
what frequency are you running at?
<cr1901_modern>
i.e. If I have two extremely similar designs, route them as close as possible to each other in placement
<ZipCPU>
cr1901_modern: Not currently. It's something I'm working on.
<ZipCPU>
kc5tja: You were running at ... was it 20MHz?
<kc5tja>
50MHz
<ZipCPU>
Must've been someone else at 20MHz. My own design is 50MHz, so that's common again between us.
<sorear>
the clock woes make a lot more sense if you only have 10ns between edges to start with
<ZipCPU>
sorear: I'm wondering about the positive vs negative edge issue. I ran my SPI flash giving it an SCK that was 180 out of phase with my sys clock.
<sorear>
i guess if you're registering MOSI close to the port, even a small delay on the clock would cause setup time violations
<ZipCPU>
I'm not sure if I want to recommend that or correct it.
<ZipCPU>
Ok, just hooked a serial port up to my TinyFPGA ... let's see if I can do anything with it.
<cr1901_modern>
I'd load up my repo but at present it depends on local changes I have to litex
<kc5tja>
If there are, configure isn't complaining about them.
<ZipCPU>
What shell are you using?
<ZipCPU>
bash or compatible?
<cr1901_modern>
Sorry to interject: So I accidentally forgot to disable the final power-down command for the SPI flash on this current test. I noticed something interesting when viewing LA traces. >>
<ZipCPU>
Yes?
<cr1901_modern>
lm32 synthesized with nextpnr. If SPI flash is in power down, all bits returned are 0xFFFFFFFF, right?
<ZipCPU>
Go on
<cr1901_modern>
Idk what that translates into in lm32 (I'll look it up in a second) but I don't think it's a jump.
<cr1901_modern>
So addresses should sequentially be placed onto the bus in order right?
<kc5tja>
Bash. But I'm using not-Debian-based Linux distro. I'm checking prerequisities still.
<cr1901_modern>
There was a weird jump to somewhere completely out of the address space a few cache lines in
<ZipCPU>
Thanks, kc5tja. cr1901_modern: Go on
<cr1901_modern>
Before going back to reading cache lines in sequential order
<cr1901_modern>
And then Pulseview crashed b/c it's a POS and I didn't get to take a pic
<ZipCPU>
Could that have been a data read?
<cr1901_modern>
Possible, but seems unlikely? In any case, I'll fire pulseview back up in a sec and then manually decode the opcode
<kc5tja>
It's rather disturbing just how many warnings are literally flying by my screen when compiling graphviz.
<kc5tja>
Like, seriously, this package must be a porting nightmare.
<ZipCPU>
:D
<ZipCPU>
I've tried to avoid graphviz in the past, and only regretted it later.
<qu1j0t3>
kc5tja: yeah :<
<kc5tja>
More people needs to invest in -Wall -Werror
<qu1j0t3>
yess
<ZipCPU>
Heheh ... Reminds me of my recent Verilator tweet. If someone hands me a file, my first two tests will be to look for default_nettype none, and then to see if it passes Verilator -Wall.
<kc5tja>
Negative. Even after making sure all deps are installed, yices2 still cannot complate configuration.
<ZipCPU>
Sigh.
<ZipCPU>
Ok, let's look at the config.log file, and see if we can figure out what's struggling.
<kc5tja>
Is there a specific git hash you have on your end? Maybe I can check out the same hash and try again.
<ZipCPU>
Sure, let me check
<ZipCPU>
I'm using this one: f8df407611366e17ab80e61ace83225fee1f25c2
<ZipCPU>
Wow ... it's a bit out of date too.
<kc5tja>
hmm, that didn't make a difference. OK, hang on and let me post config.log
<awygle>
ah, I see what you meant about the SPI clk now
<awygle>
I might have tried the SB_IO_GB or whatever it's called
<ZipCPU>
SB_IO
<ZipCPU>
SB_GB is a global buffer.
<awygle>
No, there are two. I'm referring to the other one
<kc5tja>
OK, I have boolector installed. I hope. GCC complained of a possible buffer overrun in an sprintf() function, so hopefully things will still work.
<awygle>
There's a combined SB_IO and SB_GB cell, which is in the same tile as, but drives a different net from, the pure SB_GB
<awygle>
Oh I owe somebody adding the other LM package, I should do that...
<ZipCPU>
There's an SB_GB_IO, if that's what you are referencing.
<awygle>
Yes! That.
<kc5tja>
ZipCPU: OK, what should I do next? I've completed boolector installation.
<ZipCPU>
Ready to try it all out?
<ZipCPU>
There's a BMC example on the SymbiYosys install web site.
<ZipCPU>
That'll require you to create your first .sby file, and just run SymbiYosys.
<kc5tja>
OK, checking.
<ZipCPU>
When we get to your code, the difference will be the properties we put into your code, and the name of the file in the script. (We'll probably drop the depth too --- 100 can be a challenge.)
<tinyfpga>
zipcpu: if you’re using the B2 then you need tinyfpgab
<ZipCPU>
I'm using the pre-production BX you sent me.
<tinyfpga>
Ohhh
<tinyfpga>
Hold on then
<ZipCPU>
Yes, it has taken me a *LONG* time to get this far. ;)
<ZipCPU>
Ahh ... okay, thank you. I was .. confused. :D
<kc5tja>
Le sigh.
<kc5tja>
"read" command unsupported.
<sorear>
last I heard, LP+HX+UP worked and awygle was working on LM but without success
<ZipCPU>
kc5tja: Not a problem!
<awygle>
sorear: i added support for the CM49 but my test board failed due to PCB reasons
<sorear>
and we have no takers for Ultra or UltraLite
<awygle>
someone on twitter is using the SWG25 or whatever
<ZipCPU>
That was a recent upgrade in yosys. You can use: "read_verilog -formal filename.v" instead
<ZipCPU>
That was the older interface.
<awygle>
so i promised to add support for that package so they could try it out
<kc5tja>
Trying
<awygle>
daveshah: do i only need to add the pins in icebox.py for new lm4k packages? or is there more to it?
<kc5tja>
SBY 19:30:06 [demo] base: ERROR: No such command: async2sync (type 'help' for a command overview)
<ZipCPU>
awygle: I'd be surprised if he's awake.
<sorear>
kc5tja: incidentally…you've probably already seen nextpnr/prjtrellis?
<awygle>
ZipCPU: i know :) he'll see it eventually, presumably.
<ZipCPU>
kc5tja: Ok, let's go update and rebuild yosys then.
<kc5tja>
sorear: No. I'm sticking with arachne-pnr until next-pnr is ready for production use.
<ZipCPU>
kc5tja: You use asynchronous resets in your design?
<kc5tja>
No.
<ZipCPU>
Ok, SymbiYosys is just being cautious then.
<kc5tja>
All my resets are in always @posedge() begin if (i_reset) ... end end blocks.
<ZipCPU>
So, the [script] section is a yosys script. It's not the entire yosys script. SymbiYosys tends to add some commands to it. In this case, it converts asynchronous resets to synchronous ones for the proof.
<ZipCPU>
It's a performance optimization, and can make the proof go faster, instead of having one that requires the multiclock option turned on.
<ZipCPU>
Technically, to do your roma.v file, I needed to turn multiclock on--because you did something _unusual_ with the clock.
<awygle>
ah, that *must * be all that's needed as packages are mentioned nowhere else
<ZipCPU>
So, yosys initially supported read_verilog as the command to parse Verilog code. Then the Verific parser was integrated, and yosys supported a "verific" command. The two were incompatible.
<ZipCPU>
To deal with that, a third command, "read" was created that would automatically select between whichever parser was installed.
<ZipCPU>
It would use the Verific parser if it was available, otherwise it would fall back to the traditional Yosys parser.
<kc5tja>
This step always takes a while... (still recompiling Yosys)
<ZipCPU>
And to think I had such wonderful dreams of teaching you the entire basics of FV before falling asleep.
<kc5tja>
OK, upgrading yosys and restoring the command to 'read' did the trick.
<ZipCPU>
Yes, cool!
<kc5tja>
Simplifying the installation process would go a long, long, long way towards improving adoption, I think.
* ZipCPU
sighs, lets out a long breath, then nods.
<kc5tja>
When considering developer experience, laziness is a selling point. ;)
<ZipCPU>
However ... I haven't had any of the problems you've just cited. Those were a surprise for me.
<kc5tja>
You're also using Debian, IIRC, yes?
<ZipCPU>
Ubuntu
<kc5tja>
I'm not -- I'm using Void Linux.
<awygle>
(see earlier rant about multiple nextpnr binaries)
<ZipCPU>
I've installed on both Ubuntu 16.04 and 18(something)
<ZipCPU>
kc5tja: That's probably part of the problem.
<ZipCPU>
Sounds like we are up and running, no?
<ZipCPU>
You did the demo?
<kc5tja>
Yes, it passed (finally)
<ZipCPU>
Wonderful! Let's take a look at your dmac.v core
<ZipCPU>
So, let's create a file called dmac.sby. For now, put it in the same directory as dmac.v
<sorear>
(void) ooh nice
<ZipCPU>
Copy this file from the .sby file in the example you just ran, but we'll need to make a change or two.
<ZipCPU>
First, let's remove the "depth 100" line. That'll set the depth back to the default: 20 timesteps
<ZipCPU>
Second, the script will need an: read -incdir ../../../../../include/verilog in order to get access to your tilelink.vh file.
<ZipCPU>
Then the "read" command shoudl read: "read -formal -sv dmac.v"
<ZipCPU>
The prep command: "prep -top dmac"
<ZipCPU>
The files section: dmac.v
<ZipCPU>
You should be able to run that, it should run quickly and do nothing.
<ZipCPU>
(To run it, type sby -f dmac.sby, once you have dmac.sby ready)
<ZipCPU>
Be aware, on that incdir line, there's an extra "../" (or two, I think) since SymbiYosys will first copy your file to a new directory, dmac/src, and then run Yosys and your script from within that directory.
<kc5tja>
OK, it passed.
<ZipCPU>
Cool! Now let's add some properties.
<ZipCPU>
Let's see ... it's illegal for A to be valid and D not ready, so let's create a section with `ifdef FORMAL ending with `endif at the bottom of your file.
<ZipCPU>
Within that section, let's add an: always @(*) assert((!o_a_valid)||(o_d_ready));
<ZipCPU>
Alternatively, you could've said, assert(! (o_a_valid && !o_d_read) ); Your call.
<kc5tja>
I was just about to ask. The latter is easier to read. ;)
<kc5tja>
For me, at least. :)
* ZipCPU
sheepishly admits that it's easier for him to read too.
<ZipCPU>
The stuff within the assert() is just a traditional Verilog expression. You can put any expression within there that you like.
<ZipCPU>
You can also put expressions depending upon $past() values, requiring values to be $stable() and more ... but we'll get to that.
<kc5tja>
OK, this failed. I'll need to investigate. Did you want to see the error message?
<ZipCPU>
No, I know the error message.
<ZipCPU>
I also know why it failed.
<ZipCPU>
It failed because you didn't provide any initial statements within your code. Hence, the solver was free to pick any initial values it wanted.
<ZipCPU>
It could pick initial values where o_a_valid was true and o_d_ready was false. Hence the proof failed immediately.
<ZipCPU>
Go ahead and put some initial values in your design.
<ZipCPU>
Here's the basic construct I use to test that initial values are properly assigned: https://imgur.com/1f8ZWp4
<ZipCPU>
Notice the f_past_valid. That's to keep the $past(X) operator from being evaluated on the initial timestep.
<ZipCPU>
So, if (f_past_valid) is _not_ true, then you must be on the initial time step and testing initial values.
<ZipCPU>
Likewise, on the clock following a reset, i.e. if the $past() value of reset, or $past(i_reset) was true, then you should've returned to your reset state as well.
<ZipCPU>
The construct is nice because it checks that the two states are synonymous.
<kc5tja>
It seems like it ought to be possible to write correct code without initial statements. I mean, ASICs won't have the benefit of initial configurations.
<ZipCPU>
I get no end of this feedback on twitter :)
<ZipCPU>
However, this follows the Verilog specification
<ZipCPU>
Unless/until a value is initialized, the solver can give it any value it wants.
* sorear
hasn't quite gotten to the point of understanding $past
<kc5tja>
I understand that.
<ZipCPU>
Really? $past is actually quite simple. $past(X) is the value of whatever X is, evaluated one clock ago.
<ZipCPU>
The "clock" in one clock ago is defined by the always block.
<kc5tja>
So, your imgur link -- am I correct in thinking that the code you wrote asserts the correct 'initial' settings?
<awygle>
kc5tja: I often assert that my properties only hold if the core has been reset, instead
<kc5tja>
Apologies if you already explained this.
<sorear>
that must interact in interesting ways with temporal induction
<ZipCPU>
The standard defines $past with four arguments. To my knowledge, yosys only understands two arguments, with the second one optional. $past(X,N) returns the value of X "N" clocks ago.
<ZipCPU>
kc5tja: Yes, those are the correct values for your dmac.v core.
<sorear>
now if let's say you're clifford and you're verifying a core which requires to be held in reset for at least 4 clock cycles
<ZipCPU>
sorear: Sure, go on.
<kc5tja>
I guess I just don't want to depend heavily on FPGA-specific behavior, is all.
<ZipCPU>
kc5tja: The block I showed you in the image is perfect for you then. It guarantees that the FPGA specific behavior is identical to the reset behavior.
<ZipCPU>
You'll no longer be able to change one without also changing the other.
<ZipCPU>
sorear: Your example is a good one. AXI requires 16 clocks with reset asserted initially before anything else can happen.
<ZipCPU>
It's not hard to do, I just make a 4-bit counter, initialize it to zero, and until 16-clocks have passed I assume S_AXI_ARESETN must be active (low)
<ZipCPU>
kc5tja: I don't remember what happens next, whether or not it will pass.
<ZipCPU>
In my own properties, I next went and assumed/asserted that your tilelink bus would be well behaved.
<kc5tja>
So, I added initializers for valid and ready, but it still fails. f_last_valid goes high, so it's failing on the 2nd or 3rd rising clock edge (not sure if initial rising clock edge at t=0 is considered 1st or not)
<ZipCPU>
Really? Ok. Do you know where to find the trace and pull it up? You should find a vcd file in dmac/engine_0/trace.vcd
<ZipCPU>
That's part 1 of diagnosis.
<kc5tja>
Yeah, I'm looking at the gtkwave otuput now.
<ZipCPU>
Part 2 is to look at the line that failed.
<ZipCPU>
Which assertion failed for you?
<kc5tja>
o_a_address == 0
<ZipCPU>
Did you give o_a_address an initial statement?
<ZipCPU>
Ok, I'm slowly running out of steam, so let me give you some instruction moving forward.
<ZipCPU>
There are two basic safety operators, assume() and assert().
<ZipCPU>
assume() restricts what the solver will even consider.
<ZipCPU>
assert() is the rule the solver tries to break. If he can break it, he wins. If he can't, you win. (Yes, this often feels very adversarial to me.)
<ZipCPU>
The rule you need to know is: make your assumptions about incoming variables *ONLY*.
<kc5tja>
OK, starting to get a hang of this maybe. I moved the assertion for o_a_address == 0 into a block that is covered only by if(!f_last_valid), but not last i_reset. Reason being, o_a_address *might* actually be set to 4 when i_reset is negated. I can't recall precisely. I'll change that back later.
<ZipCPU>
Assertions can be about anything else. You should always constrain outputs with an assertion, Induction will require you to constrain internal registers as well.
<kc5tja>
o_leds init is fixed.
<kc5tja>
o_a_address init is fixed.
<kc5tja>
Still failing, and still looking. More complex now; failed 4 clocks in. Progress!
<ZipCPU>
:D
<ZipCPU>
There's a third operator, cover() that can be important later. I found it very useful to get a valid trace quickly from your roma.v core.
<ZipCPU>
cover(X) will try to find any trace through your logic that will eventually lead to X being true. It requires a special .sby "mode cover" option, but other than that it's pretty straight forward.
<ZipCPU>
"cover()"ing your result is valid logic can be *very* useful--you get an instant trace through all your logic to get there.
<ZipCPU>
Ok, let's talk about that tilelink bus
<ZipCPU>
This isn't a rule of tilelink, but I've made it a rule on every bus I've worked with: if a request is being made (o*valid) and not yet accepted (i*ready) then the request should not change.
<ZipCPU>
This finds a *lot* of bugs in my code.
<ZipCPU>
So, basically, if (o_a_valid)&&(!i_a_ready) then o_a_valid should remain valid on the next clock.
<ZipCPU>
To write this, you'll need an always @(posedge i_clk) block. We'll need to use the $past() operator, and $past only works within a clocked block.
<ZipCPU>
So, you can write always @(posedge i_clk) if (($past(o_a_valid))&&(!$past(i_a_ready))) assert(o_a_valid);
<kc5tja>
OK, this is cool. The solver discovered an edge case which I didn't anticipate, single-cycle, back-to-back transactions on the A- and D-channels. (E.g., 100MT/s) I was explicitly building only for 50MT/s (one wait-state in between). So, I guess I'd need to introduce an *assumption* (not an assert) in the event that last(o_a_valid && i_a_ready && o_d_ready && i_d_valid), correct?
<ZipCPU>
Only make assumptions about the input.
<kc5tja>
OK, so then I'd have to introduce an if-clause around the assert in the always @(*) block then, yes?
<ZipCPU>
You can do that, yes.
<kc5tja>
Alternatively, alter the logic to support 100MT/s.
<kc5tja>
:)
<kc5tja>
Oh, but wait, that won't solve the problem.
<kc5tja>
(the if-statement, I mean)
<ZipCPU>
Go on.
<kc5tja>
Because during cycle N, where the transaction takes place, N+1 will have o_a_valid=1 and o_d_ready=0, which is the invalid condition. Sure, the if-clause will make sure it doesn't fail the test during cycle N+1, but it will still be an invalid condition.
<kc5tja>
Hmm, OK, I guess I have no choice but to tweak the logic no matter what.
<ZipCPU>
I didn't.
<ZipCPU>
You have choices.
<ZipCPU>
First, look at the trace. Do the valid and ready signals make sense?
<ZipCPU>
I'm going to wager they do not.
<ZipCPU>
You should not get a valid on D until you've had a valid && ready on A.
<ZipCPU>
(Yes, it might come on the same clock)
<kc5tja>
No, because what is happening is o_a_valid is immediately re-asserted during cycle N+1, but o_d_ready is not.
<kc5tja>
Hang on, let me tweak the code...
<ZipCPU>
kc5tja: I'm running on fumes here. How about this. Take a look and study what I did here: http://dpaste.com/3A3ZB4R and then we can re-engage on another night.
<ZipCPU>
Sound like a plan?
<kc5tja>
YES, I got it to pass!
* ZipCPU
smiles
<ZipCPU>
Now, try changing "mode bmc" to "mode prove"
<ZipCPU>
... and I'm headed to bed.
<ZipCPU>
n8!
<ZipCPU>
BTW ... "mode prove" is the induction mode, in case you are wondering what is different about it.
<ZipCPU>
You'll need that for your roma.v core.
<kc5tja>
Cool. Thanks for the help so far. I'm sure I'll have a lot more questions later on.
<awygle>
welcome to the fold lol
<awygle>
daveshah: if you happen to see this - i've added the other lm4k packages to icebox and the swg25tr works in arachne but the cm36 is failing _after_ placement with "terminate called after throwing an instance of 'std::out_of_range'". if you have any idea what that might be about, i'd appreciate the insight :)
<kc5tja>
And now my unit tests are broken.
<awygle>
:(
<kc5tja>
Hmm, OK, the good news is: I managed to get the unit tests working again *AND* it passes formal.
<kc5tja>
The bad news is that the code is impossible to look at and understand what's happening, because the only way to make it both pass unit and formal tests is to use some fairly sophisticated And-Or logic, which takes away entirely any ambition of human comprehension about how the core is supposed to work.
<kc5tja>
And now that it passes both unit and formal tests, it now no longer works at all in physical hardware.
<daveshah>
awygle: missing IeRen data by any chance?
seldridge has quit [Ping timeout: 244 seconds]
gekko7 has joined #yosys
kc5tja has quit [Ping timeout: 272 seconds]
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 272 seconds]
kraiskil has joined #yosys
NB0X-Matt-CA has quit [Excess Flood]
NB0X-Matt-CA has joined #yosys
NB0X-Matt-CA has quit [Excess Flood]
NB0X-Matt-CA has joined #yosys
indy has joined #yosys
<awygle>
daveshah: hm I'll check in the morning... All I did was add the pinlocdb entry
<awygle>
So if I was supposed to do something else I didn't
<daveshah>
awygle: you also need to add IeRen data for any pin locations not used by the package you had before
<awygle>
Ah OK. Could be that then. Or could be that the ieren was wrong before but never got used.
<awygle>
I'll fix that tomorrow. Thanks!
<daveshah>
It wasn't wrong before
<daveshah>
It's just it might have been missing locations that weren't covered by the script because you only looked at one package
kraiskil has quit [Ping timeout: 252 seconds]
AlexDaniel has joined #yosys
kraiskil has joined #yosys
develonepi3 has joined #yosys
zino has quit [Read error: Connection reset by peer]
zino has joined #yosys
bcoppens has joined #yosys
_florent_ has joined #yosys
kraiskil has quit [Ping timeout: 272 seconds]
Guest99708 is now known as ric96
<ZipCPU>
tinyfpga: Just a clueless user note ... I struggled to follow your on-line instructions for the TinyFPGA, that is until I realized I needed to use sudo on the installs.
maikmerten has joined #yosys
kraiskil has joined #yosys
develonepi3 has quit [Ping timeout: 264 seconds]
X-Scale has quit [Ping timeout: 272 seconds]
philtor has joined #yosys
kraiskil has quit [Ping timeout: 272 seconds]
flaviusb has quit [Ping timeout: 260 seconds]
kraiskil has joined #yosys
flaviusb has joined #yosys
X-Scale has joined #yosys
<tinyfpga>
ZipCPU: yeah, I actually want to release it under an anaconda installer
<tinyfpga>
ZipCPU: that could just take care of everything for you
<tinyfpga>
ZipCPU: some systems PIP is already configured to do local installs so you don’t need sudo, others don’t have that set up
<awygle>
daveshah: i can't find where the IeRen stuff is generated
<daveshah>
istr there's a script in icefuzz/tests
<daveshah>
Called ioctrl or something like that
<awygle>
i thought so but it must not actually use those terms...
<awygle>
daveshah: does the fact that i made *a* bitstream with the swg25tr package mean its ierens are right, or do i need to run that one as well?
<awygle>
i.e. is it possible i just didn't use a pin that was missing ierens?
<daveshah>
I think as soon as you have one bitstream you are OK
<daveshah>
But I can't exactly remember how arachne handles IeRens
<awygle>
mk. well it doesn't take too long, i guess i'll just run it
<awygle>
thanks as always
<awygle>
how are things going?
<daveshah>
Not bad, been somewhat busy though and moving back from my placement in Vienna to the UK tomorrow morning
<daveshah>
Hoping to get a ECP5 RAM done soon ish
<awygle>
oh dang
<awygle>
good luck with the move
m4ssi has quit [Remote host closed the connection]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
zino has quit [Remote host closed the connection]
zino has joined #yosys
mjoldfield has joined #yosys
digshadow has quit [Ping timeout: 268 seconds]
azonenberg_work has quit [Ping timeout: 252 seconds]
azonenberg_work has joined #yosys
digshadow has joined #yosys
pie_ has joined #yosys
kc5tja has joined #yosys
kc5tja has left #yosys [#yosys]
<mattvenn>
I'm having problems with formally proving a simple state machine is working
<mattvenn>
I'm using ZipCPU's basic setup, including assuming all inputs are stable and only change on clock rise
<mattvenn>
but the states are changing on negedge of clock
<mattvenn>
sometimes
<ZipCPU>
Hello mattvenn!
<awygle>
mattvenn: can you share the code and the counterexample trace?
<ZipCPU>
mattvenn: Is your design a multiclock or single clock design?
<mattvenn>
single clock with a clock enable
<mattvenn>
I need to make a version that I can share online
<ZipCPU>
mattvenn: Then get rid of the assumptions that the inputs are stable and only change on the clock rise.
<ZipCPU>
If it's only a single clock, then you shouldn't be using any $global_clock always blocks at all. That was one of the things I got messed up in my earlier work.
<mattvenn>
ok
<cr1901_modern>
if you're using a single clock as well, IIRC, the clock signal will _not_ show up as transitioning in traces; you'll need to check the smt_clock signal instead
<ZipCPU>
cr1901_modern: Clifford fixed that, but his fix is somewhat fragile. Sometimes the fix works, sometimes it doesn't. It's sort of design dependent which of the two it will be.
<mattvenn>
ok that helps
<mattvenn>
so do I not need to assume the inputs will only change on rising clock edge anymore for single clock designs?
<ZipCPU>
Correct.
<mattvenn>
ok
* shapr
hops cheerfully
* shapr
hugs ZipCPU
<shapr>
ZipCPU: thanks for writing awesome articles!
* ZipCPU
wonders why shapr is hopping cheerfully, and not doing cartwheels
<qu1j0t3>
i'll take either
tautologico has joined #yosys
seldridge has quit [Ping timeout: 252 seconds]
kc5tja has joined #yosys
seldridge has joined #yosys
maikmerten has quit [Quit: Ex-Chat]
xerpi has joined #yosys
xerpi has quit [Remote host closed the connection]
xerpi has joined #yosys
kraiskil has quit [Ping timeout: 276 seconds]
gekko7 has quit [Ping timeout: 268 seconds]
xerpi has quit [Remote host closed the connection]
<awygle>
trying to build nextpnr, i get "cannot open file" for the prjtrellis database? do i have to run something? download-latest-db.sh?
<awygle>
ah, yes
<awygle>
and i see that that is in the documentation
seldridge has quit [Ping timeout: 245 seconds]
<awygle>
running nextpnr-bench with -j$(nproc) in a VM is absolutely bringing my system to its knees, IRC is lagging almost a full second on each keypress
<ZipCPU>
Wow.
<shapr>
how do you run the benchmarks?
<awygle>
download nextpnr-bench, go to ice40 directory, run make
<awygle>
probably do not run make -j$(nproc) as you will get bad results and also IRC will lag
<shapr>
oh, separate repo
<awygle>
yup
<awygle>
hm i wonder if there's any way to know if these designs are functional. i guess i could do an equiv check between the nextpnr and the arachne output, but that sounds like work
<awygle>
mithro: weren't you doing this kind of thing?
<shapr>
ooh yeah, my laptop is a great heater now
<awygle>
as sorear pointed out to me running parallel jobs will skew the benchmark results. i just wanted to make sure nextpnr still ran with my changes. running the full benchmark was probably overkill.