<shapr>
one of these in particular kicked my fans way up
<kc5tja>
I'm here; I'm just finishing up some household chores. Hope to be finished within 30ish minutes.
<ZipCPU>
Hello!
<ZipCPU>
For those who might be interested, kc5tja and I will be working on formally verifying two of his modules from this repository: https://imgur.com/a/tRidKmS
<ZipCPU>
In general, we'll be verifying a flash controller. If you are interested in the basics, feel free to check out my article on how to build a flash controller here: http://zipcpu.com/blog/2018/08/16/spiflash.html
<ZipCPU>
kc5tja has a different controller from that one, but the basics will be the same.
<ZipCPU>
If all goes well, I hope to have the discussion here on this IRC forum.
<shapr>
yay!
<ZipCPU>
Welcome, shapr!
* awygle
lurks quietly
<ZipCPU>
To still set the background, if you run the formal tools on the dmac.v file, you get a result looking quite like this: https://imgur.com/a/tRidKmS
<ZipCPU>
The strange thing about this result is that it passes _trivially_. The .sby file calls for a BMC proof (bounded model check) of 100 clock cycles, yet the solver claims that it is done before finishing even the first clock cycle.
<ZipCPU>
So, when kc5tja comes back (and reads up on what I just said), we'll start in on the problem there.
* ZipCPU
recommends the popcorn to awygle
gundy has joined #yosys
pie_ has quit [Ping timeout: 272 seconds]
porglezomp has joined #yosys
<shapr>
I wonder if I can use python's mmap library to write to /dev/mem for gpmc access?
<ZipCPU>
I would imagine so.
<shapr>
ok, I'll try your suggestion from last week with python's mmap module
<ZipCPU>
I've thought about publishing the solution from a C++ standpoint. It'd be quite useful to those with SOC+FPGA's, just haven't gotten around to it. It'd be the same solution both ways.
<shapr>
hm, I just want to set the first four bits directly
<shapr>
I could write a byte of 1, but will that cause other problems?
<ZipCPU>
No, writing a byte of 1 should be fine.
<ZipCPU>
You'll have another problem though.
<shapr>
oh?
<ZipCPU>
The LED might only be on for 20ns or something--to short for your eye to see it.
<shapr>
er, oh
<shapr>
oh huh
<shapr>
so I need to write a byte of 1 in a loop?
<ZipCPU>
That's not how I'd do it.
<ZipCPU>
Try instead setting the FPGA any time csn1 is low, wein is low, *and* the data is 1
<ZipCPU>
Then clear it on the same criteria, but only when the data is zero.
<ZipCPU>
That should be your first experiment. Then repeat, but using different addresses.
<ZipCPU>
So, when using different addresses, writing a "1" to one address might adjust the LED, whereas writing it to another address shouldn't change a thing.
* shapr
looks up some terms
* ZipCPU
looks over shapr's code closer
<shapr>
oh, gpmc_csn1
<shapr>
and gpmc_wein
<shapr>
ok, that helps
* shapr
googles to see what those mean
<kc5tja>
Sorry, that took a lot longer than expected. Wife has strep-like symptoms, so I'm pretty much at her beck and call while she's home.
<ZipCPU>
Sounds too familiar.
<ZipCPU>
Tell me when you've read the back log.
<kc5tja>
done.
<ZipCPU>
Does my image match what you've seen?
<kc5tja>
I will revert my ROMA core modifications so we can start from the same page.
<ZipCPU>
We can start with dmac.v. There's plenty there to keep us busy for a bit.
<ZipCPU>
Our first step is going to be adding a "cover" statement to dmac.v, and then to switch the .sby file from "mode bmc" to "mode cover"
<kc5tja>
Let me double check, but IIRC, my verification goes through 100 steps before it finally passes.
<ZipCPU>
The purpose of a cover statement is to prove that something *can* happen. Right now, the design is passing trivially, suggesting that things *aren't* happening that should be.
digshadow has left #yosys [#yosys]
<ZipCPU>
With what I pulled from the repo, your .sby file asked for 100 steps, but SymbiYosys came back before running all of those 100 steps.
<ZipCPU>
Looks like it came back without even running a single step.
<ZipCPU>
Here's a quick scribble of some cover statements you might wish to add. https://imgur.com/MhvMpnB
<ZipCPU>
I think I've got them right. Haven't tried building with them yet.
<kc5tja>
ZipCPU: Yeah, your image looks very different from my results. My side goes through 100 assertion checks before declaring that it passes
<ZipCPU>
Go ahead and try the cover anyway. It'll be nice to know the design at least does the right thing.
<kc5tja>
What does it actually do?
<ZipCPU>
Cover is a formal mode where the tools will exhaustively search the state space of your design to see if they can find a way to make the cover statement true.
<ZipCPU>
The result is a trace, through the logic of your design, from the initial state to where the cover statement is valid.
<ZipCPU>
I find it *very* useful in things like a SPI controller to cover the result of a bus operation.
<ZipCPU>
Think of it this way ... if you cover the result, then the formal tools will give you an example trace showing the request from the bus, the request of the flash, the address, and then the data returned by the flash.
<ZipCPU>
... leading up to finally showing where the value was returned over the bus.
<kc5tja>
Still passes after 100 steps.
<ZipCPU>
It's a wonderful tool when you are first writing your code for that reason too. One cover statement can be equivalent to a *LOT* of lines of test bench.
<ZipCPU>
Still passes? Let's check the sby file. Did you change "mode bmc" to "mode cover"?
<kc5tja>
No.
<ZipCPU>
Try changing the mode to cover and running again.
<kc5tja>
OK, still passes, but looks like 4 new files were deposited in the workspace directory.
<ZipCPU>
Exactly!
<ZipCPU>
That's one trace for each of your cover statements.
<ZipCPU>
The very last step of the trace will contain logic that makes the respective cover statement true.
<ZipCPU>
I find the third trace quite useful. Let me paste a link to that one.
<ZipCPU>
Take a close look at the i_a_ready trace.
<ZipCPU>
Compare that to o_a_valid.
sorear has quit []
<ZipCPU>
The design is moving forward from one address to the next without waiting for the slave to accept the request that's being made.
<ZipCPU>
BTW ... this is one of those things that can trip folks up using formal verification for the first time.
sorear has joined #yosys
<ZipCPU>
An engineer might look at this trace and say, yeah, but the way I designed the slave, i_a_ready will always be true.
<ZipCPU>
This trace isn't valid, therefore.
<kc5tja>
OK, so here is my beef with this.
andi- has quit [*.net *.split]
<ZipCPU>
To which I would answer, does it follow the specification? Then it's valid. Making one-off interfaces is usually bad practice.
<ZipCPU>
Sorry, go on.
* ZipCPU
acknowledges that there's a couple beefs to be had
* ZipCPU
looks forward to hearing the one kc5tja brings up
<kc5tja>
Two things: (1) this DMAC exists to exercise the ROMA core and nothing else. It's not intended to be (at least as it is currently written) to become an integral part of the Kestrel-3. It's throw-away, in that sense.
<kc5tja>
But far more importantly, (2) I can't be expected to think of every possible edge case that might disprove a design.
<kc5tja>
I have no idea *why* you thought to use a cover statement like that.
<ZipCPU>
But, see, that's what makes the formal tools so valuable: they find all the edge cases for you.
<kc5tja>
But they didn't.
<ZipCPU>
Ahh ... I can explain the cover statement.
<kc5tja>
You found the edge case; all you did was automate the trace leading up to it.
<ZipCPU>
Want to do that next?
<ZipCPU>
I just used cover() to get an idea of what was going on.
<ZipCPU>
Cover is used to prove that some can happen, i.e. your design *could* work. It doesn't prove that your design will always work.
<ZipCPU>
It's like having a wrench in your toolbox.
<ZipCPU>
To tighten a bolt, though, you might need both the wrench (cover) and the screw driver (assert/assume).
<ZipCPU>
Can I share the beef I thought you'd have?
<kc5tja>
Sure. But just to clarify my frustration, I don't doubt the tools work. I doubt my own ability to use them in a meaningful way.
<ZipCPU>
Ahh ... okay, you wanted me to explain the cover. Why I chose the cover I did. That'd help there.
<ZipCPU>
I wanted to pick a cover() statement that would show a transaction completed.
<ZipCPU>
Hence, I picked a cover that would show i_d_valid and o_d_ready.
<ZipCPU>
I was worried that somehow there was a trivial solution, so I also insisted that o_a_valid be false.
<ZipCPU>
When the result came back, it just ... didn't satisfy me. I was still worried the design wasn't being exercised properly. Keep in mind, my focus isn't to provve the design works (yet), but rather that it could work.
<ZipCPU>
I also wanted to "see" what was going on within it.
<ZipCPU>
So, I tried to add an address to the cover. In order to get to address 64'h20, the design would need to execute several requests.
<kc5tja>
But, TileLink allows that same case to occur without completing the transaction. The cover statement doesn't cover the whole story -- to be a correct TileLink transaction, you _must_ have the address and opcode put out on the A-channel before the D-channel.
<kc5tja>
The cover statement is ambiguous because it doesn't provide the required history that the transaction occurs on A-channel first.
<ZipCPU>
You caught that! Good, that was the beef I thought you were going to bring up earlier.
<ZipCPU>
Yes, exactly!
<ZipCPU>
Shall we fix that?
* kc5tja
nods
<ZipCPU>
The problem is that ... we have inputs to our module that aren't behaving properly. They aren't acting like a tilelink interface should.
<ZipCPU>
To get them to behave, we'll need to make an assumption or two about them in order to describe their behavior.
* ZipCPU
searches for his notes
<ZipCPU>
Ok, I found my notes.
<kc5tja>
I was expecting $past() to be used here. Heh.
<ZipCPU>
So one of the things I do in all my bus interfaces is count requests, and insist that there be no responses without a request.
<ZipCPU>
This little code snippet does that.
<ZipCPU>
Once a request is made (a_valid and a_ready), it is marked as an accepted request.
<ZipCPU>
Then, later, if no request has been accepted, then there should be no response--hence we assume !i_d_valid
<ZipCPU>
Alternatively, i_d_valid could still be true if the response was being made to a request made on the same clock.
<ZipCPU>
This will fix the i_d_valid problem we had in the last trace, where i_d_valid was true even though i_a_ready was never (yet) high any time o_d_valid was true.
<ZipCPU>
That won't find another bug in your code (yet). It'll just give us a better looking i_d_valid signal.
<ZipCPU>
Now we need to add some assertions to your code. Specifically, let's make the assertion that while a request is outstanding (and !i_a_valid), that the request should not change.
<ZipCPU>
I'd like to be fairly dogmatic about this one, but tilelink is a strange protocol and says specifically that you can change a request before it has been accepted.
<ZipCPU>
To me that's a bug--it means your logic isn't working.
<ZipCPU>
However, it's not a failure to follow the tilelink protocol. Still, I'm going to call it a failure of purpose.
<ZipCPU>
I think in your design, you want to make certain that you don't go on to the next request until the last has been accepted, right?
<ZipCPU>
When you are ready.
<kc5tja>
Just to be clear, this chunk of code goes inside the ifdef FORMAL block, yes?
<ZipCPU>
Absolutely!
<ZipCPU>
That's to keep it from getting confused with the operational/synthesizable code.
<ZipCPU>
Sadly, Verilator doesn't support the $past operator. It supports a lot of other assertion-types of operators, it's just that .... I use $past() a lot, and it just doesn't support that.
<ZipCPU>
Oh, I almost forgot, did I mention that these formal operators can be used in simulation as well as with the formal tools?
<kc5tja>
"change a request before it's been accepted" -- that's how it supports prioritization on individual ports. If a higher priority transaction comes in from somewhere, and your current transaction has not yet been accepted, then you can preempt it.
<ZipCPU>
Do you intend to do that with this design?
<kc5tja>
You can actually do that on AXI too, it's just not explicitly written out. Because an exchange only occurs when valid & ready is true, when it's false anything goes.
<kc5tja>
No, that's a feature intended for switches. TileLink is not a bus, it's a point to point protocol, like RapidIO or HyperTransport.
<kc5tja>
It's unlikely to be used by endpoints.
<kc5tja>
I'm just clarifying, because it looks like you consider that feature a bug of TileLink, the specification, versus how I implemented it.
<ZipCPU>
You've attempted to implement it as I envision it should be implemented. I just disagree with this "feature" in the spec.
<ZipCPU>
So, here's the piece that will insist that nothing changes but on an accepted transaction.
<ZipCPU>
Let's talk our way through that, shall we?
<ZipCPU>
I think we discussed f_past_valid yesterday. f_past_valid keeps us from testing the value of $past() when it would reference something before time.
<ZipCPU>
Likewise, !$past(i_reset) just makes sure that this clock isn't following a reset.
<ZipCPU>
Those two conditions out of the way, the first assertion states that if o_d_ready was true and i_d_valid wasn't true, then o_d_ready should be true again.
<ZipCPU>
We can argue about whether that one was needed. For now, let's step to the next.
<ZipCPU>
The second assertion says that if o_a_valid was true on the last clock, but i_a_ready was false, then o_a_valid needs to remain true on the next clock.
<ZipCPU>
In other words, if we are waiting for a transaction to be accepted, then we need to keep waiting if it wasn't accepted on the last clock.
<ZipCPU>
The third assertion is very similar. If a request was outstanding on the last clock and i_a_ready wasn't true on that clock,
<ZipCPU>
then the address and mask should stay constant.
<ZipCPU>
$stable(x) by the way is equivalent to the statement (x == $past(x))
<ZipCPU>
It's just a bit of short hand.
digshadow has joined #yosys
<ZipCPU>
The second condition of the third set of assertions is sort of like the first assertion: not required by the bus, but I needed it to force the design into a valid state during induction.
esden has quit [*.net *.split]
<ZipCPU>
If you want to remove those for now you can, we can come back to them later.
<ZipCPU>
That should leave you with assertions about o_a_valid, o_a_address, and o_a_mask
* ZipCPU
pauses for a breath
<ZipCPU>
Any questions?
<kc5tja>
Still studying. This is a fair bit to take in, and I'm typing at the same time.
<kc5tja>
U stjklashd
<kc5tja>
I still have a question about the clause (o_a_valid && i_a_ready) in the previous imgur link.
<kc5tja>
That's saying, if no parcel has been accepted (f_accepted is false), then "assume" either no i_d_valid (in which case o_a_valid and i_a_ready can be in any state) or i_d_valid is true *and* both o_a_valid and i_a_ready is true at the same time. IS that correct?
<ZipCPU>
Yes. That's because f_accepted is registered.
<ZipCPU>
It takes a clock for f_accepted to take affect.
<ZipCPU>
*effect
<kc5tja>
Right.
<ZipCPU>
So there's two possibilities there.
<ZipCPU>
1. You are not waiting on a transaction at all, in which case i_d_valid should be false.
<ZipCPU>
2. You haven't had a chance to recognize a new transaction request, but a response is coming back on that same clock.
<ZipCPU>
We could also add an assertion there if we wanted: if (!f_accepted) assert(o_d_ready);
<ZipCPU>
Oops, that goes the other way: if (f_accepted) assert(o_d_ready);
<ZipCPU>
Of course, that's a property of your design, not necessarily a property of tilelink
<kc5tja>
I was about to say, that doesn't handle the single-cycle case.
<ZipCPU>
;)
<ZipCPU>
Is this starting to make some more sense?
<kc5tja>
Yes, but I'm finding having to consider it all extremely daunting. This is some of the hardest code I've ever written.
<ZipCPU>
Relax
<ZipCPU>
These are patterns
<ZipCPU>
You get used to patterns, they start to make more sense the more often you use them
<ZipCPU>
This is one of about 4 patterns I use with busses.
<kc5tja>
The other thing is I'm deeply afraid of interactions between rules, covers, asserts, and assumptions.
<ZipCPU>
There just aren't that many patterns necessary to prove a bus
<ZipCPU>
Yes :D ?
<ZipCPU>
Yes, they do interact.
<ZipCPU>
However, only the assumptions *make* things happen.
<ZipCPU>
The assumption restricts inputs to your design (don't use it on local logic or outputs)
<kc5tja>
I wish there were some way of compartmentalizing things in conveniently named (for lack of better term) "procedures" so that I can keep better track of them and isolate them.
<ZipCPU>
Well ... there is .... in the Verific enabled commercial version of Yosys.
<ZipCPU>
Basically, System Verilog allows you to define "properties"
<ZipCPU>
You can then assert that a property is true.
<awygle>
properties are one of two SV features i really, really miss in vanilla-yosys
<ZipCPU>
One problem with properties, however, if that they can get *MUCH* more complex than this.
<ZipCPU>
Hence, I recommend learning assertions and assumptions in this fashion first.
<awygle>
given that we don't have them, i strongly recommend big block comments grouping logical "properties" and describing them in plain english (or your native tongue) to help you keep track.
* ZipCPU
notes that neither "Haskell" nor "Python" are valid "native tongues"
<ZipCPU>
kc5tja: So there are two rules I'm insisting on within this code right now.
<ZipCPU>
1) A request once made (o_a_valid,o_address,o_mask,etc) should not change until the clock after (o_a_valid)&&(i_a_ready)
<ZipCPU>
2) For every request, there should be one and only one response
<ZipCPU>
This second one requires counting requests. In the case of this controller, you only need to count to one request.
<kc5tja>
Why assert($stable(o_a_valid)) and not just assert(o_a_valid)? The if-predicate already has $past(o_a_valid) as part of its expression, so isn't stable() superfluous here?
<ZipCPU>
Clifford calls this the parenthesis matching problem
<ZipCPU>
kc5tja: Yeah
<ZipCPU>
In hind sight I like assert(o_a_valid) better.
<kc5tja>
ZipCPU: Re: rules -- correct.
* ZipCPU
doesn't want to admit that, while pasting the code, he was wondering the same thing
<ZipCPU>
So f_accepted is my count of the number of requests that have been made. It counts to one, and returns to zero.
<ZipCPU>
Let me know 1) when you have finished typing, and 2) when you have no more questions and are ready to try these assertions and this assumption.
<kc5tja>
Just a second...
<kc5tja>
OK, I think I'm up to date.
digshadow has quit [Ping timeout: 260 seconds]
<ZipCPU>
You can run the cover trace again if you would like.
<kc5tja>
Oh, wait, I was always running the cover trace. I wasn't aware I should be running bmc or prove.
<ZipCPU>
That's fine.
<ZipCPU>
I hadn't said to switch yet.
<ZipCPU>
I was going to run cover here, get a trace like this one: https://imgur.com/IR1UQen and then recommend we switch to mode bmc
<ZipCPU>
Now that we have more assertions, mode bmc makes good sense.
<ZipCPU>
The problem with bmc is that, when things work, you don't get a trace
<ZipCPU>
With cover, if things are working, you always get a trace.
<kc5tja>
The design fails quickly with bmc. I'm going to have to rewrite all my modifications to dmac to try and make it pass again. I need to get rid of all that combinatorial logic anyway, as arachne-pnr will have none of it (fails to converge when routing)
<ZipCPU>
Pull up the trace.
<ZipCPU>
Does it look like a "valid bug"? Or did we get our properties wrong?
<ZipCPU>
"valid bug": a bug in the synthesizable logic, vs a bug in the formal properties.
<kc5tja>
Yeah, i_drq was asserted before a response on D-channel occurred.
<ZipCPU>
Is that a bug?
<ZipCPU>
We haven't done anything to constrain i_drq ... yet
<kc5tja>
For the purposes of the DMAC, yes. I'll need to just rewrite the DMAC from scratch, it seems.
<ZipCPU>
Why is that?
<kc5tja>
However, since this is just a debugging tool, I can rely on i_drq not being asserted more than once every second to two seconds.
<kc5tja>
Because it seems like it'd greatly simplify the design of the set of properties.
<kc5tja>
Right now, we're adding more and more and more edge-cases to the properties, and the total lines of code in properties matches the lines of code (comments notwithstanding) in unit tests.
<ZipCPU>
Oh, is i_drq your once a second strobe?
<kc5tja>
Yes. "Data Request".
<kc5tja>
brb -- bio-break.
<ZipCPU>
So ... you might want to say always @(*) if (o_d_ready) assume(!i_brq);
<ZipCPU>
Then let me bring up to speed anyone watching.
<ZipCPU>
When running BMC on this (now modified) design, you get the output shown here: https://imgur.com/ynGz0bp
<ZipCPU>
Specifically, you want to look for the location of the trace, dmac/engine_0/trace.vcd, as well as the assertion that failed, "Assert failed in dmac: dmac.v:267"
<ZipCPU>
This tells us where to find the assertion that failed, and where to find the trace to examine it.
<porglezomp>
Since there's a break going on for this particular project for a few minutes, do you mind if I ask an unrelated verification question?
<ZipCPU>
Welcome! Go ahead.
<porglezomp>
I'm doing some processor design stuff, and was wondering how I would approach writing properties that span several cycles, particularly for variable numbers of cycles.
<porglezomp>
Like: executing this add instruction should give a certain state several steps down the line.
<ZipCPU>
With the free version of Yosys, you may need to set up a state machine to describe that. Let me offer another example, though.
<ZipCPU>
When formally verifying an FFT butterfly, I was able to keep track of the input N clocks ago in an array of inputs.
gundy has quit [Ping timeout: 252 seconds]
<ZipCPU>
I could then assert that the operation on input_x[5 clocks ago] and input_y[5 clocks ago] had specific properties.
<ZipCPU>
While SV offers sequences to deal with this, my own work with the ZipCPU hasn't found these to be all that useful for longer operations.
<ZipCPU>
I found myself naturally wanting to describe things on a clock by clock basis.
<ZipCPU>
This includes the divide as well for example
<ZipCPU>
For most of the CPU, the reason was: Things can stall (or not) on a clock by clock basis. Hence, I enjoyed having properties that referenced my internal state on a clock by clock basis.
<porglezomp>
mhm. I've been thinking about pipelines today, so while asking that question I had the idea to write assertions about the behavior of pipeline stages.
<ZipCPU>
Does that help?
<porglezomp>
Yes, it does
<porglezomp>
Thank you
<ZipCPU>
Well, hold on, let's apply the lesson with kc5tja to pipelines
<ZipCPU>
The rule was nothing could change until the next stage was ready to accept it.
<ZipCPU>
I've found that rule *VERY* valuable when verifying pipeline stages of CPU's.
<ZipCPU>
You'll see that the o_d_ready line is dropped before any data was returned.
<ZipCPU>
This is a bug that kc5tja will need to work on.
<ZipCPU>
When he gets back, I'll point out that his code from yesterday midday didn't have this bug--it just needed some minor initial value tweaks.
<kc5tja>
back
<ZipCPU>
Let me know when you've read the backlog
guan has quit [*.net *.split]
Ristovski has quit [*.net *.split]
Max-P has quit [*.net *.split]
FL4SHK has quit [*.net *.split]
TD-Linux has quit [*.net *.split]
daveshah has quit [*.net *.split]
adamgreig has quit [*.net *.split]
jeandet has quit [*.net *.split]
grummel has quit [*.net *.split]
<kc5tja>
The version of dmac.v we started out with today had several bugs fixed (which I did not push), largely because of the combinatorial logic that arachne-pnr had such issues with. I'll need to rewrite all my fixes since then.
<kc5tja>
Because right now, even with all these properties, it will not elaborate the design into a bitstream.
<ZipCPU>
I think your problem are the (new) next_a_valid and next_d_ready signals.
<ZipCPU>
I'm not sure these were ever necessary.
<kc5tja>
So about those,
<kc5tja>
I started out by re-evaluating the state-machine that A-channel and D-channel ultimately describes.
<kc5tja>
(since I do not pipeline stages)
<kc5tja>
It turns out, after designing the state machine, the results of the internal state machine bits exactly matched the values of o_a_valid and o_d_ready.
<ZipCPU>
Must be in your copy, 'cause I'm getting something different here.
<kc5tja>
So what I did was just express those signals via a minimized sum-of-minterms.
<kc5tja>
Hence, next_a_valid, et. al. are the next states for o_a_valid, et. al.
<ZipCPU>
Ahh ... those are two-process state machine signals now?
<kc5tja>
What does two-process mean?
<ZipCPU>
Well, typically, in a two-process state machine you have two always blocks setting the variables. The first is an always @(*) or always_comb block. It's completely combinatorial. The second one is clocked and does little more than set the value of the register to be the result of the combinational logic.
<kc5tja>
I just used wire assignments instead of an always @(*).
<kc5tja>
But, yes.
<kc5tja>
I need to head to the store before it closes. I hate to cut it at this point, but it's also getting late for ZipCPU too. I don't want to keep you. :)
<ZipCPU>
Thank you
* ZipCPU
's wife thanks you
<kc5tja>
I'm going to try rewriting the DMAC, because it's clear that fixing what's here isn't going to work well.
<ZipCPU>
Shall we continue this another night?
<ZipCPU>
... but but but .... it worked yesterday!
<kc5tja>
It didn't though.
<kc5tja>
It refused to place/route.
<ZipCPU>
If you just reverted to yesterday mid-day, and add the formal properties, you'd just about have something working.
<ZipCPU>
The only real problem you had (as I recall) were just the initial states.
<kc5tja>
"Working" to me means it must pass unit tests, formal verification, *and* synthesize to a bitstream *and* work in hardware.
<kc5tja>
Maybe I'm being too perfectionist.
<ZipCPU>
Well, it 1) was synthesizing, 2) it passed the formal tests I just shared, 3) it had passed simulation, it just didn't pass the hardware problem.
<ZipCPU>
We isolated the hardware problem to another part of your design.
<kc5tja>
It was not synthesizing.
<ZipCPU>
I'm thinking of the code you had Monday morning, not after working on it last night.
<kc5tja>
Look above in the log -- I'd mentioned here and on Twitter that it failed to complete PNR.
<ZipCPU>
Back up another 12 hrs.
[Ristovski] has joined #yosys
<kc5tja>
Oh, yeah, if you go back to before exploring formal, then yes it worked fine. :)
<ZipCPU>
:D
<ZipCPU>
Let's chat some more later.
<kc5tja>
But, formal changes too many things for me.
<kc5tja>
OK, chat later. Thanks again for the help!
<ZipCPU>
Cheers!
<ZipCPU>
I'd also like to offer if anyone listening has a question before I sign off for the night?
<ZipCPU>
No? Ok. Night all!
Max-P has joined #yosys
_whitelogger has joined #yosys
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 240 seconds]
daveshah has joined #yosys
porglezomp has quit [Ping timeout: 252 seconds]
kraiskil has joined #yosys
m_w has joined #yosys
<kc5tja>
Well, that's downright disturbing. I've traced the failure of arachne-pnr to elaborate my design to ..... initial statements. If I pre-assign o_a_ready and o_d_valid so as to make formal verification happy, arachne-pnr will simply have none of it and refuse to elaborate no matter how many passes I allow it.
<kc5tja>
Note to self: never use initializers, and always put initial begin/end blocks under an `ifdef FORMAL guard.
<kc5tja>
and with that, bedtime for me too.
azonenberg_work has quit [Ping timeout: 252 seconds]
kraiskil has quit [Read error: Connection reset by peer]
kraiskil has joined #yosys
azonenberg_work has joined #yosys
kraiskil has quit [Read error: Connection reset by peer]
kraiskil has joined #yosys
kraiskil has quit [Remote host closed the connection]
seldridge has quit [Ping timeout: 252 seconds]
kc5tja has quit [Quit: leaving]
m4ssi has joined #yosys
[Ristovski] is now known as Ristovski
kbeckmann has joined #yosys
m_w has quit [Ping timeout: 246 seconds]
m4ssi has quit [Ping timeout: 245 seconds]
m4ssi has joined #yosys
maartenBE has joined #yosys
gundy has joined #yosys
adamgreig has joined #yosys
kraiskil has joined #yosys
gekko7 has joined #yosys
rohitksingh_work has joined #yosys
promach has quit [Quit: WeeChat 2.3-dev]
gundy has quit [Ping timeout: 250 seconds]
<mattvenn>
yay! found my first bug with formal methods
m4ssi has quit [Ping timeout: 240 seconds]
m4ssi has joined #yosys
gundy has joined #yosys
kraiskil has quit [Quit: Leaving]
<ZipCPU>
Yaayyyyy!!!
<ZipCPU>
mattvenn: What did you find?
fsasm has joined #yosys
<ZipCPU>
kc5tja: I was able to reproduce your arachne-pnr problem with the code you posted last night. I'm not quite sure what the problem is, but I'll note this: the design routes with nextpnr
pie_ has joined #yosys
seldridge has joined #yosys
seldridge has quit [Ping timeout: 246 seconds]
rohitksingh_work has quit [Read error: Connection reset by peer]
rohitksingh has joined #yosys
gundy has quit [Ping timeout: 240 seconds]
seldridge has joined #yosys
X-Scale has quit [Ping timeout: 244 seconds]
fsasm has quit [Ping timeout: 245 seconds]
develonepi3 has joined #yosys
rohitksingh has quit [Quit: Leaving.]
seldridge has quit [Ping timeout: 252 seconds]
rohitksingh has joined #yosys
seldridge has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
X-Scale has joined #yosys
develonepi3 has quit [Remote host closed the connection]
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
gekko7 has quit [Ping timeout: 252 seconds]
<mattvenn>
ZipCPU: something unexpected! minor really, not a show stopper but certainly worth fixing
<ZipCPU>
BTW .... I figured out the problem kc5tja had with his initial statements.
<awygle>
oh kermie
rohitksingh has quit [Quit: Leaving.]
<ZipCPU>
Lol
<shapr>
it ain't easy being green
<awygle>
something something rainbow connection
* shapr
tries not to sing
<shapr>
when I get into flow, I sing
<shapr>
I work in an open office :-(
<shapr>
NO FLOW FOR ME
* awygle
knows this struggle well
rohitksingh has joined #yosys
<qu1j0t3>
:/
<awygle>
at least we have cubes, but singing is probably still frowned upon
<ZipCPU>
Last time I was in a room of cubicles, it was considered fun to throw wads of paper over the walls. When done, the individual in the other cubicle would invariable cry out, "Ow! My eye!"
<awygle>
i recently moved cubes and immediately formed a power bloc with my new neighbors
<awygle>
we now only need to flip one vote from the six-cube island across the aisle to win any given meeting
azonenberg_work has quit [Ping timeout: 240 seconds]
<qu1j0t3>
LOL
rohitksingh has quit [Quit: Leaving.]
<awygle>
this isn't _actually_ how meetings work, but i did form a power bloc. it works out because it's five people on three different projects so our interests rarely conflict.
<qu1j0t3>
meetings as Thunderdome
azonenberg_work has joined #yosys
<awygle>
aren't they? a kind of Thunderdome for ideas.
<qu1j0t3>
ideally i suppose.
<awygle>
at least engineering design meetings. meetings with management are like... i dunno, the crying game? the prestige? a different movie in any case
seldridge has quit [Ping timeout: 245 seconds]
porglezomp has joined #yosys
m4ssi has quit [Remote host closed the connection]
seldridge has joined #yosys
AlexDaniel has quit [Read error: Connection reset by peer]
AlexDaniel has joined #yosys
m_w has joined #yosys
seldridge has quit [Ping timeout: 252 seconds]
porglezomp has quit [Ping timeout: 246 seconds]
seldridge has joined #yosys
<awygle>
shapr: just caught myself singing under my breath in the cubes :/
dxld has quit [Quit: Bye]
dxld has joined #yosys
<shapr>
hah
<shapr>
awygle: I work from home at least one day a week for that reason
<awygle>
i usually do, but this week i had a meeting that day
seldridge has quit [Ping timeout: 245 seconds]
* ZipCPU
can't hear ... he has talk radio blaring in his ears.
seldridge has joined #yosys
maikmerten has joined #yosys
TD-Linux has joined #yosys
kuldeep has quit [Ping timeout: 264 seconds]
kuldeep has joined #yosys
seldridge has quit [Ping timeout: 252 seconds]
maikmerten has quit [Quit: Ex-Chat]
azonenberg_work has quit [Ping timeout: 245 seconds]