<q3k>
so in this case pll packing is three main pieces of logic: unifying plloutcore/plloutglobal net names, pre-placing pll_*pad* plls in the required bels, and finally adding route-through LUTs for LOCK
seldridge has joined #yosys
emeb has joined #yosys
fsasm has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 252 seconds]
rohitksingh has joined #yosys
fsasm has quit [Ping timeout: 245 seconds]
gruetzkopf has quit [Read error: Connection reset by peer]
gruetzkopf has joined #yosys
rohitksingh has quit [Ping timeout: 246 seconds]
gruetzkopf has quit [Read error: Connection reset by peer]
gruetzkopf has joined #yosys
gruetzkopf has quit [Read error: Connection reset by peer]
gruetzkopf has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
fsasm has joined #yosys
azonenberg_work has quit [Ping timeout: 260 seconds]
kc5tja has joined #yosys
<kc5tja>
Does anyone have any kind of knowledge-base I could read through concerning designs which pass bmc and cover, but which fail inductive proof?
fsasm has quit [Ping timeout: 246 seconds]
<ZipCPU>
Yes.
<ZipCPU>
Have you checked out the inductive exercise on ZipCPU.com?
<kc5tja>
I'm at work (in the actual office), so unable to take action now.
<ZipCPU>
I try to discuss that very issue there, with a simple example showing why the problem exists and discussing how to deal with it.
<kc5tja>
But, last night, I was working on creating the TileLink interface to the SIA's register set, and got it "working", except for prove mode. It fails induction during time step 0 (so, after the entire depth).
<ZipCPU>
Induction will only ever fail at timestep zero.
<kc5tja>
I looked back at our earlier IRC chats, but nothing there seemed to help in any material way.
<ZipCPU>
If it fails at all, that's where it will fail.
<ZipCPU>
Yeah, we didn't get to discussing induction yet.
<ZipCPU>
It's an important topic, we just didn't get to it.
<kc5tja>
The other question I have is, how to work with proving modules with dependencies. Do you have to somehow synthesize all the proofs of the sub-modules? That seems like a lot of work, so I suspect there's something I'm missing.
<kc5tja>
For example, the SIA (so far!) has a transmitter-engine module, a register-set module, and a rate-generator module used to time out-going bits. When I bundle all these together, do I need to do anything special proof-wise?
<ZipCPU>
Quite possibly.
<ZipCPU>
You can prove them independently, or jointly. The difficulty you will have proving them jointly is induction. Induction will fail if you have any inconsistent state across your design.
<ZipCPU>
For example, imagine you have a bus slave and a bus master that you wish to jointly prove.
<ZipCPU>
If the proof starts and the bus slave is allowed to think it has 2-transactions in flight, while the bus master thinks there are five, then the bus master could hang.
<ZipCPU>
The solution is to assert that these two numbers are identical.
<ZipCPU>
This can be a bit of a problem, since neither of the two modules would normally reveal how many transactions it thinks are in flight to the parent module.
<ZipCPU>
However, if you want to formally verify the two together, then you'll want to do so at an upper level, and that's where you'll need to assert that these two transaction counters are identical.
<ZipCPU>
That can force items onto the portlist that wouldn't otherwise be present.
azonenberg_work has joined #yosys
kuldeep has quit [Ping timeout: 260 seconds]
kuldeep has joined #yosys
fsasm has joined #yosys
<cr1901_modern>
q3k: Dunno, if it's still in master, I have to recompile and check
<cr1901_modern>
I was mainly curious about the nature of the bug :)
<kc5tja>
I just read the induction-exercise article, but it's not clear to me what steps are required to resolve even those exercise problems, much less my own design.
<kc5tja>
Excepting for asserting sa==sb at all times.
rohitksingh has joined #yosys
<ZipCPU>
kc5tja: Ok, sure, let's walk through it.
<ZipCPU>
assert(sa==sb); solves the problem. It's not the only solution.
<ZipCPU>
Some designs include pipelines that will naturally flush. In those cases, you can often get by with ensuring an induction depth longer than the pipeline length.
<ZipCPU>
In the design of the induction exercise, you need to specifically force the pipeline to flush by assuming properties about the i_ce value.
<ZipCPU>
In bus interface designs, you often need to add a count of the outstanding operations to the portlist, to be asserted by the aggregating module.
fsasm has quit [Ping timeout: 244 seconds]
<kc5tja>
I tried something similar with my current design, where I upgraded z_last_valid from a simple bit to an up-counter. However, the meaning of this counter is non-sensical when using induction, and is frequently the source of the failure in subtle ways.
<kc5tja>
I wish I'd pushed my code. I'll do that when I get home.
<sorear>
at least for single-clock, it is always possible to do depth 1 with enough asserts
<kc5tja>
Long story short, I can't think of any other properties to assert which would cause induction to assume correct states.
<awygle>
sorear: really? Interesting
<q3k>
cr1901_modern: check the diff, should explain it well
<sorear>
but some of those asserts you would need are going to involve violating encapsulation in some way or another - ZipCPU's Fibonacci vs Galois example is a good one
<awygle>
Doesn't that make your asserts equivalent to your program though?
<awygle>
And therefore not any less error prone?
<sorear>
(although it helps if you understand what those terms mean, explaining them would take a whole separate post)
<sorear>
fundamentally, all testing is that
<sorear>
you say what you mean in two *very different* ways and count on not making the same mistake in both place
<ZipCPU>
sorear: +1
<sorear>
the more different the better. if your tests mirror your code line for line, they're nearly useless
<awygle>
I can see why your claim is true but it doesn't seem useful, I guess.
<awygle>
The power of the tool is letting *it* figure out that your state spaces are equivalent or whatever
<cr1901_modern>
q3k: Now why would I do that when someone could do all the work for me ;)? (Joke. Fair enough.)
<ZipCPU>
awygle: Yes, if only.
<ZipCPU>
I like to break things down this way ... every module should have a "contract" that it fills.
<sorear>
my background is infinitary mathematics, where proof tools struggle with anything substantially more complicated than "reduce these two formulae to lowest terms and see if they match"
<ZipCPU>
You specify the "contract" in formal speak first.
<sorear>
SMT is finite and the tools seem to work better
<ZipCPU>
Once you finish specifying the contract, you then add additional assertions in order to pass induction, or to reduce the depth of the proof.
<ZipCPU>
sorear: A fellow mathematician?
<ZipCPU>
You mean I'm not alone here? ;)
<sorear>
not by trade, but I like reading papers and I'm responsible for a fair chunk of us.metamath.org
rohitksingh has quit [Quit: Leaving.]
<ZipCPU>
kc5tja: sorear said it pretty well.
<awygle>
ZipCPU: i do that as well (although last time we talked about this you kept trying to get me to crack open the guts of all my modules :p)
<sorear>
(which doesn't use *any* fancy proof tools; i've spent a few days with isabelle and coq and found the state of the art automatic provers more annoying than actually helpful)
<sorear>
(it's possible my opinion could change with a lot more exposure)
<ZipCPU>
sorear: Have you tried SymbiYosys at all?
<sorear>
no
<ZipCPU>
i.e. formally verifying Verilog code?
<ZipCPU>
(with any solver)
<ZipCPU>
kc5tja: The bottom line regarding induction is that if the induction engine starts in an invalid state, you will need to form some kind of assertion to keep it from that state.
<ZipCPU>
As sorear mentioned, forming that assertion may require that you violate your favorite encapsulation principles.
<kc5tja>
sorear: Regarding breaking encapsulation -- I'm firmly convinced formal cannot work just at the interface boundaries. All of my "working" proofs involve white-box testing at some level. This is my #1 issue with formal right now. I abhore having to break the interface of a module just to get something to prove. Unit tests do not suffer from this deficiency.
<sorear>
what I would attempt to do, (and I am on much less firm footing here - i've just acquired potential lab space so hopefully this will stop being theoretical for me), is to add signals to your interface which (a) make sense in the context of the interface (b) will be optimized out (dead code elimination) in synthesis
<sorear>
e.g. for a bus master you might add a wire i_am_waiting_for_a_reply
<ZipCPU>
You can use `ifdef FORMAL and `endif if the code might not otherwise be optimized away.
<ZipCPU>
sorear: I added a counter, rather than a single signal wire, counting the number of requests that were outstanding
<kc5tja>
I already have those wires (just not exposed via an interface; for TileLink, they're fundamental to making a working interface, I'm finding).
<ZipCPU>
kc5tja: The other thing you need to be aware of are your assumptions.
<ZipCPU>
If you prove module A, given some assumptions, and then module A is made to be a submodule of B, the wires that come from B into A should no longer be assumed.
<kc5tja>
Anyway, my point isn't that I'm upset that I'm breaking encapsulation. As I said before, formal is *harder* than TDD, but there's a pay-off.
<ZipCPU>
Yes
<kc5tja>
I'm just flustered because I am hitting a dead-end when it comes to making induction pass.
<ZipCPU>
Want to spend some time digging into it tonight again?
maikmerten has quit [Quit: Ex-Chat]
<ZipCPU>
On this channel that is.
<kc5tja>
If we could, that would be great. Because, even after reading your blogs, I'm finding confirmation of the problem, but no path forward in finding a resolution.
<ZipCPU>
Sure! Let's take a look at your code, and some traces, and see what's going on.
<kc5tja>
Not now though. I have to push the code first.
<ZipCPU>
Got it
<kc5tja>
It's 1:36 here now, so in about 4 hours, wife permitting?
<ZipCPU>
I hope her health is doing better, but sure
<kc5tja>
She's getting better. 2nd time this year catching strep. 2nd time on antibiotics. 2nd time she's making a nice recovery. She has her voice back, at least.
<ZipCPU>
Sounds like my kids and family.
<ZipCPU>
Caught strep, recovering now the second time, on the second set of antibiotics, etc. Very familiar story.
<kc5tja>
Thankfully, we don't have kids. But my wife is a vet tech, so she interacts with the public a lot more than I do.
<ZipCPU>
Tell her we're praying for her quick recovery.
s1dev has joined #yosys
dxld has quit [Quit: Bye]
dxld has joined #yosys
s1dev has quit [Ping timeout: 252 seconds]
<cr1901_modern>
q3k: A different assertion failure re: the PLLs when I try to compile my design w/ nextpnr HEAD. I'll try to minimize the example, but right now I need to finish up something else
<cr1901_modern>
And of course nextpnr took an hour to compile b/c it had to regenerate all the ice40 dbs
<cr1901_modern>
At least it can route my design, unlike arachne
<q3k>
yeah, file a bug if you can
<cr1901_modern>
"Warning: PLL 'SB_PLL40_CORE' has unknown connected port 'PLLOUTGLOBAL' - ignoring" Curious warning though. I thought this was part of the primitives
<kc5tja>
ZipCPU: Just finished reading invariant.html article. I see you're defining lots of preprocessor symbols, but what controls them? E.g., what defines PHASE_ONE and PHASE_TWO et. al.?
<ZipCPU>
kc5tja: My symbiyosys script.
<ZipCPU>
I can show you how that works more later if you would like.
<cr1901_modern>
q3k: Waiting for a compile, so I'll see if I can crash it now :)
<q3k>
cr1901_modern: should be PLLOUTCORE iirc
<q3k>
yes.
<cr1901_modern>
Hmmm... /me checks manual anyway. I wonder if I've been doing it wrong all this time
<q3k>
i'll read through the manuals/datasheets as well
<q3k>
i might've implemented it wrong
<q3k>
so hm
<cr1901_modern>
q3k: I _have_ done clock multiplication successfully on ice40 before, I swear :)
<q3k>
so hm, PLLOUTGLOBAL is supposed to be used when you want to drive a global clock
<cr1901_modern>
Yes, that is my intent here
<cr1901_modern>
I then run the PLLOUTGLOBAL through an SB_GB
<q3k>
I usually just use PLLOUTCORE and let the pnr try to meet my timings without that sort of handholding :)
<kc5tja>
ZipCPU: Maybe later. I need to focus on getting a module proof-worthy first. Heh.
<q3k>
but I'll try to support PLLOUTGLOBAL, just have to check out how the routing bits for that look like
<cr1901_modern>
Well that's fair. At the time I didn't know whether PLLOUTGLOBAL actually meant a _real_ net, or it was just a hint to PNR to route to a GB
<kc5tja>
ZipCPU: Where have you found formal to be most valuable though? What was the one moment that convinced you to abandon unit tests all-together?
<cr1901_modern>
q3k: Lemme finish my example and I'll file a report.
<q3k>
cr1901_modern: that's the thing, I don't think I've seen any other bits than just the ones that route it into glb_netwk
<ZipCPU>
kc5tja: I found formal most valuable at the leaf module level. While you can aggregate it, it doesn't aggregate all that easily.
<ZipCPU>
kc5tja: Did you read about the list of CPU bugs I found when using formal?
<kc5tja>
That's what I'm finding as well. I'm thinking of using Verilator for integration testing, and formal for leaf testing.
<kc5tja>
A while ago.
<ZipCPU>
Yes, exactly
<ZipCPU>
I use Verilator for integration testing, and formal for leaf testing (with some aggregated testing)
<ZipCPU>
For example, I'd formally verify a CPU
<ZipCPU>
Were I to continue formally verifying a design, I'd replace the CPU with an arbitrary bus master.
<q3k>
cr1901_modern: sorry, not glbnetwk, but the silly loopback into the io buffers
<q3k>
cr1901_modern: lemme dig further..
<cr1901_modern>
ack, thanks
<kc5tja>
I'm disinclined to formally verify a full CPU. I'd just verify leaf components, but the configuration requirements for multi-level verification appears to not be worth it for me.
<ZipCPU>
kc5tja: Formally verifying the whole CPU was not my first formal verification task. I didn't even try it until I had formally verified all of the parts and pieces.
<ZipCPU>
I was rather intimidated by the task at first.
* kc5tja
nods
<ZipCPU>
I learned a lot by doing it, but ... I'm not going to dive into that task blindly again.
<ZipCPU>
This is also why my topic for ORCONF this year is going to be lessons I learned in the process.
* kc5tja
nods
<q3k>
cr1901_modern: yeah, I think if you use PLLOUTCORE and an SB_GB it's going to have more or less the same effect as if you used PLLOUTGLOBAL in the vendor suite
<ZipCPU>
Having done it once, I'd do it again, but not the same way.
<kc5tja>
I'd be interested in seeing that presentation.
<q3k>
cr1901_modern: i can't find another way into the global network apart from going through a normal SB_GB user input
<ZipCPU>
Some other tasks where I've formal very valuable include: Caches, oh yes, definitely cache implementations!
<ZipCPU>
Debugging caches is *PAINFUL*. With formal, it becomes quite easy. But .... this is a leaf module again.
<ZipCPU>
Another fascinating one: SDRAM's. I was surprised to find a buried bug in my "working" SDRAM controller
<ZipCPU>
That controller had already moved to hardware. It would've been next to impossible to find that bug without using formal.
<q3k>
cr1901_modern: I think the best course of action for me is to have the packer insert an SB_GB if the user outputs a signal via PLLOUTGLOBAL and they haven't inserted an SB_GB manually
* kc5tja
needs to go back and change all the SBY files over to use tasks. SInce I make it a habit of going through bmc, prove, and cover testing, this is just what I need to automate that process.
<cr1901_modern>
q3k: Well, take a look at my minimal example before that b/c I _did_ insert an SB_GB manually
<ZipCPU>
I'd also formally verify any future FIFO implementations I ever create.
<cr1901_modern>
I'm making a bug report now
<q3k>
cr1901_modern: yes, my point is that I'll have to implement this, not that it should work already ;P
<cr1901_modern>
oh... sorry :(
<q3k>
no need to apologize
<ZipCPU>
kc5tja: One of the more painful modules I had to debug was a bus component for an Altera (I mean intel) SOC+FPGA. One mistake on that bus, and the whole design would lock up *HARD*, and I only got out of that with a hard power reset.
<ZipCPU>
That kind of bug is too painful to debug any other way. I'd definitely use formal therefore on any bus component.
<q3k>
zynqs do that too
<q3k>
if you mess up your axi implementation :P
<ZipCPU>
kc5tja: I guess the reason why I've abandoned unit tests so completely is (practically) because my unit tests were never that good. In design after design, finding bugs in components via formal has left me wondering, why use unit tests?
<ZipCPU>
I still use Verilator for integration testing though.
<sorear>
isn't a unit test just formal where the assumptions completely constrain the inputs to the DUT
<cr1901_modern>
that's a gross way of looking at it ._.
<kc5tja>
sorear: If you're thorough enough in your testing methodology, which requires some discipline, it's equivalent to BMC verification. However, it's not capable (without outside help, at least) of doing the same job as induction proofs.
<kc5tja>
For the latter, you'll need something along the lines of QuickCheck adapted to Verilog somehow.
<sorear>
what i'm saying, tongue in cheek, is that formal methods encompass unit testing as a special case but go beyond (induction and being able to *not* constrain specific inputs and test all values of them simultaneously)
<sorear>
also "quickcheck for verilog" is "die hard in an office building"; constrained random verification is a hardware trick first
<kc5tja>
OK, sure, but I still claim it's a tradeoff. I do not find formal easier to use, nor do I find the prospect of proving integration between leaf modules appealing nor pleasant. It will certainly be a drain on my productivity.
<kc5tja>
*IS* a drain on my productivity.
<kc5tja>
The SIA core would be done by now if I were using Verilator for unit-testing.
<ZipCPU>
I've never been so thorough with my testing methodology that it was equivalent to BMC. That might just be me.
<ZipCPU>
kc5tja: I do find formal easier to use, but that might just be an experience thing. Having used it as much as I have, it's now my go to tool both for initial design as well as for debugging.
<kc5tja>
With only few exceptions, I find bmc roughly equal to unit testing. Remember, TDD is a rigorous process. Test-after methodology leads devs to test only for the happy path. Test-first optimizes development to cover edge cases too.
<awygle>
lol @ "die hard in an office building"
<kc5tja>
I don't care what came first. I care only for semantic equivalence.
<ZipCPU>
kc5tja: Here's an example for discussion: an instruction cache that would almost work. Upon a CPU request for an instruction, it would go and fill a cache line.
<ZipCPU>
All of this I tested. It returned the right value as well in all of my tests.
<ZipCPU>
The problem is, my unit tests didn't check all of the locations in the cache line.
<ZipCPU>
If you wanted to jump to the last element in a cache line, it might return the wrong value.
<ZipCPU>
That took me a *LONG* time to find, and its easy to prove it won't happen using formal.
<ZipCPU>
That might also just be my lack of "vision" when it comes to designing unit tests as well, but this particular design had a unit test and it had passed it.
<kc5tja>
Did it fail in bmc?
<ZipCPU>
With the I-cache, I found the bug before discovering formal. When I built a data cache, I went directly to formal for this purpose.
<kc5tja>
I find so far that induction is the source fo all my "oh, I didn't think of that case" situation. bmc comparatively rarely doesn't fail on unforeseen situations on me.
<ZipCPU>
+1
<ZipCPU>
Yes, it takes an additional level of assertions just to pass induction.
<kc5tja>
Gotta head out now.
<ZipCPU>
Assertions that aren't needed for BMC
<ZipCPU>
;)
<ZipCPU>
Chat again later.
kc5tja has quit [Quit: off to the gym]
mwk has quit [Ping timeout: 244 seconds]
<ZipCPU>
My biggest problem is that I keep finding "bugs" in all the code that I never formally verified.
<cr1901_modern>
I was under the impression that "PLLOUTGLOBAL" _must_ be followed by SB_GB to use it efficiently, precisely because it was so close to the global nets
<daveshah>
cr1901_modern: no, PLLOUTGLOBAL drives a global net by itself
<cr1901_modern>
But you're saying that the vendor tools will look at PLLOUTGLOBAL and know that it should be attached to a specific global net internally?
<cr1901_modern>
daveshah: ^^
<daveshah>
cr1901_modern: PLLOUTGLOBAL only dives a global net
<daveshah>
*drives
<cr1901_modern>
Right, so the vendor tools know to treat it specially, is what I'm asking; one you use PLLOUTGLOBAL and a PLL is chosen, that net is set for the duration of pnr
<cr1901_modern>
q3k: >I'll implement this properly and also add a warning if the design uses a PLLOUTGLOBAL followed by an SB_IO... can you also add a warning for using PLLOUTGLOBAL followed by SB_GB :)?
<cr1901_modern>
In any case, I've been basically wasting an SB_GB for 2 years then...
<daveshah>
cr1901_modern: and a LUT in fact
<cr1901_modern>
it's a LUT... there's a thousand more where that came from :)
<daveshah>
Might deteriorate clock quality a bit in some critical application
<cr1901_modern>
I guess the answer is "no", but would arachne have been smart enough to realize that two SB_GBs are in fact the same net if I routed PLLOUTGLOBAL through an SB_GB, and then choose the "nearest global net" (if there's such a thing)?
mwk has joined #yosys
<daveshah>
cr1901_modern: no, and that would be an incorrect solution
<daveshah>
Place and route tools aren't really supposed to remove cells imo
<q3k>
cr1901_modern: whoops, ment 'SB_GB'
kuldeep has quit [Ping timeout: 244 seconds]
<cr1901_modern>
In any case, good thing nextpnr can route tinyfpga BX, b/c arachne can't. And arachne simply gives a very helpful "fatal error: failed to route"
<ZipCPU>
I've found that adjusting the random seed can often help fix a "failed to route" bug
kuldeep has joined #yosys
<cr1901_modern>
ZipCPU: I haven't tried that and I should. I do worry that b/c a few very-similar-but-not-the-same designs have failed for BX, and b/c changing the design _also_ changes how arachne-pnr routes, changing the seed won't help.
<cr1901_modern>
But worth a shot
<cr1901_modern>
seed 0 doesn't work, so I'll start with 1 :P
<awygle>
hm, i wonder what causes failed to route errors then
<cr1901_modern>
In the worst case, I'll have to wait (2^32 - 1)*5 minutes :)
<ZipCPU>
Remember, arachne-pnr and nextpnr are both driven by a random number generator. The problem is just too complex to solve outright, so they randomly try to get close to an optimal solution.
<ZipCPU>
This is not that different from ISE
<ZipCPU>
Changing the random seed value once or twice is usually enough to fix a problem ... unless of course the design itself has a fault within it.
<awygle>
ah, it seems the router failed to route the placement given by the placer
<awygle>
so that's the failure you'll get on very congested designs, _or_ where arachne is wrongly informed about some placement constraint
<ZipCPU>
Both placer and router are driven by the same random number generator.
<awygle>
does nextpnr have any kind of congestion input to its cost function?
<cr1901_modern>
BX's PCF is significantly different from B2 (which _does_ work fine w/ arachne), except for the SPI flash for obvious reasons
<awygle>
looks like no
<awygle>
and indeed it almost can't because such a thing sort of implies a notion of "good enough" that nextpnr doesn't possess
<awygle>
as the optimium solution when trying to route for maximum speed is to pack logic as closely as possible right up until you're out of routing channels
<awygle>
so any sort of tension-based parameter to the cost function would be leaving performance on the table in a way that nextpnr can't know is "okay"
<awygle>
ZipCPU: how's your "relative clock net weights" project coming? :p
<ZipCPU>
It's ... coming. I just shared some spectacular failure slides with others.
<ZipCPU>
So, if success is measured by the number of failures, then ... I'm now closer to success than I was before. ;)
<awygle>
well good luck. i am occasionally working on a project which requires knowing when to stop in a different way than SA does
<awygle>
so incorporating your work would be helpful
* cr1901_modern
tries seed #2
* cr1901_modern
considers writing a script to try all the seeds until one works
<ZipCPU>
awygle: Thanks for the encouragement!
<awygle>
cr1901_modern: if you have cores to spare, check out what nextpnr-bench does to - yes do that
<ZipCPU>
cr1901_modern: if it fails for more than about 3 seeds, then it might be time to dig into what's going wrong within the design.
<awygle>
or, not do that, and decide arachne-pnr isn't worth playing with anymore. up to you lol
<cr1901_modern>
It's a mystery of life, probably
<ZipCPU>
Double check that you are not overcommitting the part.
<cr1901_modern>
it's ~3500 LUTs
<ZipCPU>
I was counseling someone recently whose design placed but failed to route
<ZipCPU>
The issue had to deal with a memory that wasn't getting properly recognized as block RAM
<ZipCPU>
3500 LUTs doesn't sound like it should be a problem though.
<ZipCPU>
Are you overcommitting your blcok RAMS?
<cr1901_modern>
31/32
<awygle>
that can cause routing pressure, for sure
<cr1901_modern>
awygle: Design also failed when I was using like 2kB of BRAM
<cr1901_modern>
(this is 10kB plus cache)
* awygle
shrugs
<cr1901_modern>
In any case, I guess arachne has no facility to dump it's internal state after placing is done, so I can see where it's getting stuck?
<ZipCPU>
That'd be a question for daveshah
<cr1901_modern>
(ALso, B2 _also_ failed w/ arachne until I removed a few non-essential I/Os)
<awygle>
you can dump a post-place netlist
<awygle>
and a post-place PCF, i guess in case you're not fully constrained?
<awygle>
beyond that it shouldn't be too hard to add some logging
<awygle>
do you get outputs that look like "pass #, # shared"?
<cr1901_modern>
awygle: No, I didn't even know arachne could do that
<cr1901_modern>
in any case, seed #2 suceeded
<awygle>
oh good
<cr1901_modern>
but it's disappointly slow... 22.94 MHz. My target was 32 MHz
* cr1901_modern
may run it anyway just to see what happens
<awygle>
my version of arachne's source has _tons_ of 3#if 0 and // around logging statements in route.cc, btw. so if you want to get more info, you can probably just uncomment those
<cr1901_modern>
Oh, they're commented. I don't spend much time looking at arachne's source, I value what little patience I have for debugging
<awygle>
yeah not unreasonable
<cr1901_modern>
That's hilarious... removing the extra used GB from PLLOUTCORE reduces speed from 22MHz to 18MHz
<cr1901_modern>
daveshah: Have any idea why that would happen? I thought it was supposedf to get faster :P
<daveshah>
cr1901_modern: I wouldn't base anything on one test given arachne-pnr results can change +/-20%
<cr1901_modern>
Can someone open a portal to a universe where quantum computing isn't a fraud so I can test all 4 billion seeds at once?
<sorear>
why stop there, why not just check all possible placements
<cr1901_modern>
B/c I assume the portal won't be open longer than 10 mins
dxld has quit [Quit: Bye]
dxld has joined #yosys
<cr1901_modern>
I've seen @posedge clk wrap a concurrent assertion, but I've never seen a concurrent assertion wrap a @posedge clk.