<duck2>
hehe i just noticed the rapidsmith site is a .doc file saved as .html
<duck2>
mithro: i threw more eye-time on the rapidsmith site and the terminology file. what i understand is they don't store a flattened rr_graph in the device file(won't fit into 539kb), but can somehow do routing. what i don't understand is how do they do it without storing or expanding into a flattened rr_graph(it's impressive if their rr_graph for virt
<duck2>
ex 4 takes 34mb in java heap). unfortunately not much information on this is given on the site.
<mithro>
duck2: I assume they expand the graph on demand
<duck2>
looks like wires(nodes) are enhanced int objects which run queries on the file when they are asked about their edges
<duck2>
only a guess
<duck2>
mithro: if we had magic implementation wand, would it be feasible in VPR? i expect an awful lot of such edge queries to be made. and then there are maps of metadata
<mithro>
duck2: A lot of that data is de-duplicatable
<mithro>
duck2: I assume they store the data in a similar manner to tileconn
<mithro>
duck2: I was hoping to get that Python example for you done both yesterday and today but I don't see it happening.... will try again tomorrow
<duck2>
ok. i should take a look at the rapidsmith source sometime.
<duck2>
nextpnr also does not load a flattened graph in memory afaik
<mithro>
duck2: It has a bunch of different modes - it is unclear to me which ones are being used - it definitely uses a flattened graph for ice40 at some point
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
futarisIRCcloud has joined #symbiflow
swick has quit [Quit: ZNC 1.6.5+deb1+deb9u1 - http://znc.in]
citypw has quit [Ping timeout: 244 seconds]
Bertl_zZ is now known as Bertl
proteusguy has quit [Ping timeout: 255 seconds]
GuzTech has joined #symbiflow
<sf-slack>
<acomodi> litghost, mithro: I have pushed the progress relative to the equivalent tiles (https://github.com/SymbiFlow/vtr-verilog-to-routing/pull/36). Pin mapping works fine (at least within the regression test I have added), and I have started working on the actual equivalent tiles placement in the placer. Right now the placer consumes all the locations of the original cluster type, and, if no locations are available anymore
<sf-slack>
it places the cluster in the equivalent tile.
<sf-slack>
<acomodi> I still need to adapt the `swap` algorithm to look for more suitable location in equivalent tiles (if they exist)
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
futarisIRCcloud has joined #symbiflow
<sf-slack>
<kgugala> @litghost @mithro I'm looking at the possibilities of adding the timing information to architecture definition and there seem to be two options
<sf-slack>
<kgugala> one is to implement a script to read the arch.merged.xml file and add/update timing entries basing on sdfs generated with timining fuzzer
<sf-slack>
<kgugala> this option is pretty straight forward - it will add one step between xml merging and carry chains specialization
<sf-slack>
<kgugala> I'm not sure if this scales, though
<sf-slack>
<kgugala> the second option is to generate all the arch xmls from verilog (this is something @mithro mentioned some time ago)
<sf-slack>
<kgugala> this is much more work, because we'd need to reimplment all the arch.xml generation
<sf-slack>
<kgugala> but this would allow us to create verilog templates for every BEL and CLB structure
<sf-slack>
<kgugala> a separate script can use the verlilog templates and merge them with timings from sdf
<sf-slack>
<kgugala> in the end v2x tool can generate arch xml
<sf-slack>
<kgugala> this approach is much more versatile, but requires more work
<sf-slack>
<kgugala> what do you think
<sf-slack>
<mkurc> I wonder whether it is possible in the second option to include the timings in Verilog models and use them for simulation. (just a random thought)
<litghost>
hackerfoo: What changed? I'm also working on writing a testbench for the FF SR/CE test should we should probably commonize some things, at a minimum an assert of some kind
<litghost>
kgugala: I think we should proceed with a v2x solution, with the follow caveat: Let's write tests as we god
<litghost>
go*
<litghost>
kgugala: I am working on some FF tests, which also does a little combintorial testing
<tpb>
Title: WIP: Improve the Verilog to XML conversion process by acomodi · Pull Request #316 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)
<sf-slack>
<mkurc> My status update: I changed the grid location map implementation to use foreign keys. There are two tile grid tables in the database and a mapping table which references their pkeys.
<litghost>
mkurc: Is your latest stuff pushed to the PR?
<sf-slack>
<mkurc> @litghost Yes
<sf-slack>
<mkurc> @litghost But I still cannot find a solution of the problem with routing of const nets
<litghost>
mkurc: I just made a suggsetion
<sf-slack>
<mkurc> @litghost Thx, I'll try right away
GuzTech has quit [Remote host closed the connection]
<tpb>
Title: Enable kokoro on symbiflow-arch-defs by litghost · Pull Request #556 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)
<litghost>
hackerfoo: There is an advantage to using a testbench with the "top" of the design, you can run testbinch to run against the fasm2verilog version of the design. I recommend using the "top" module if you want to check the post-PnR results
<hackerfoo>
Okay. I'd rather avoid duplication, but top included UART logic that I didn't want in the testbench. Is there something like CPP for Verilog?
<hackerfoo>
Nevermind, I see "ifdef" in the code.
<litghost>
hackerfoo: I specifically was suggesting you test with the UART, so you can run the testbench against both the pre-synthesis and post-PnR design. Adding #ifdef's for testing would undo that
<litghost>
hackerfoo: Maybe two testbench's are needed for your purpose
<mithro>
litghost: We currently run out of io pins if you try and place and route the non-top.v module, right?
<litghost>
mithro: That is one problem, yes
<litghost>
mithro: ROI breakout would help with that
<litghost>
mithro: But in this case running the UART on both sides of the top module is probably a good idea
kc8apf has left #symbiflow [#symbiflow]
<mithro>
litghost: I think we probably want a test helper with the uart then
<litghost>
mithro: Don't disagree
<litghost>
mithro: The UART module itself can serve that purpose, combined with a deframer/read queue
<litghost>
mithro: I avoided adding a queue to the current FIFO module because eventually we will want to use a BRAM FIFO or something, unclear
<tpb>
Title: Makefiles for formal proofs with SymbiYosys (at zipcpu.com)
<mithro>
Dunno if that is useful at all...
<litghost>
mithro: I think that is for build up of cumulative proofs
<litghost>
mithro: I think most of our proofs should be single instance
<litghost>
mithro: If we try to prove say, the picosoc, then that will be usefull
<mithro>
litghost: If the proofs work on the original verilog, they should still work on the verilog from the bitstream, right?
<litghost>
mithro: We haven't been proving the original verilog though
<litghost>
mithro: To date, we've been proving that pre-synthesis is equivilant to post-PnR
<litghost>
mithro: I believe those links are about proving verilog "assume" statements
<litghost>
mithro: Which would be lost through the PnR process
<litghost>
mithro: That being said the documentation (including that blog) on the Yosys proving process is pretty terrible
<litghost>
mithro: The Yosys documentation on $equiv cells is literally a TODO
proteusguy has joined #symbiflow
<mithro>
litghost: You could try poking zipcpu and daveshah in #yosys
<litghost>
mithro: Nah, I think the problem I have is an actual error, either in our PnR or fasm2verilog
<litghost>
mithro: I was stuck for a bit, but the testbench will help prove to myself that the equivilance error is real
<mithro>
litghost: I think we should poke zipcpu about doing a tutorial about equivalence proving anyway
<hackerfoo>
litghost: Maybe it would be best to just use a single error signal pin for testbenches instead of a full UART.
<litghost>
mithro: If I find that I cannot replicate the equivalence failure in the TB, I'll poke upstream
ZipCPU has joined #symbiflow
<litghost>
hackerfoo: Sure, and on hardware just have the pin connect to an LED? That will work
<hackerfoo>
One reason I want to avoid complexity is to make the FASM easier to analyze.
<ZipCPU>
Hello, mithro
<mithro>
ZipCPU: we were just chatting about formal equivalence proving
<ZipCPU>
Alright, wow, go on
<mithro>
ZipCPU: I was saying that your other formal tutorials / blog posts are pretty good
* ZipCPU
is looking through the log for some context
<mithro>
and litghost was complaining "The Yosys documentation on $equiv cells is literally a TODO"
<litghost>
ZipCPU: i was say that the equiv documentation in the yosys manual is pretty close to non-existant
<ZipCPU>
That's pretty close to reality
<ZipCPU>
It's not an "advertised" feature
<litghost>
lol
<ZipCPU>
I've tried to help coach some folks through it before, but it's always befuddled the both of us
<mithro>
ZipCPU: so, was wondering if we could persuade you to look into documentation :-P
<ZipCPU>
Supposedly SymbiYosys can do it, I just haven't been successful at it
<litghost>
e.g. it has the documentation?
<ZipCPU>
Well, back up a bit, what are you trying to do?
<ZipCPU>
What type of equivalence checking?
<ZipCPU>
Some types are doable, some not so much
<litghost>
I'm trying to prove a simple design pre-synthesis matches post-PnR. It has some combintorial elements and 1 FF. I believe there is a true equivilance failure, but I haven't been able to find the problem as of yet
<hackerfoo>
How many bits? Up to 32 bits of input + state is easy.
<litghost>
Indeed, sorry, trying to say 1 FF per input
<hackerfoo>
So, 32 bits then?
<litghost>
What is interesting is the led[9] led[10] and led[11] are failing to prove
<litghost>
If I change the xor reduce to say Q[5:0
<litghost>
It proves
<hackerfoo>
Check all 4 billion cases. Should take a few minutes on hardware.
<litghost>
But Q[7:0] fails
<litghost>
hackerfoo: The goal is to have a test that runs without hardware
alexhw has joined #symbiflow
<litghost>
ZipCPU: It's unclear at this time if the equiv check is failing because of an actually PnR bug (very possible) or a bug in the newly written 7-series fasm2verilog code
<litghost>
ZipCPU: Or simply a case where the equiv check cannot prove the situation
<hackerfoo>
litghost: Oh, well then can you use Verilator?
<ZipCPU>
Heh, yeah, one of the reasons why the equivalency support isn't yet "advertised" ;)
bubble_buster has joined #symbiflow
<ZipCPU>
So, there's a couple of basic types of equivalency checking
<ZipCPU>
One checks things from the top level inputs and outputs alone.
<litghost>
I'm currently use the equiv cells at top level inputs and outputs
<ZipCPU>
The second type does a check between FFs
<litghost>
You are refering to equiv_struct?
<litghost>
for the second type
<ZipCPU>
It's the second check, the input->FF, FF->FF, and FF->output that's practically doable for the case you are interested in
<litghost>
Yosys was unable to add equiv cells using equiv_struct
<litghost>
I wasn't able to diagnose why that was the case
<litghost>
FYI, I am using latest Yosys master as of yesterday
* ZipCPU
is browsing yosys doc's, for anything starting with "equiv"
<litghost>
It's pretty sparse
* ZipCPU
reads the "miter" page ...
<litghost>
ZipCPU: miter might make this worse, it only adds the equiv cell for the 1 output yes?
<ZipCPU>
No, it's much more powerful than that
<litghost>
What is the relative utility of equiv_make and miter -equiv?
<litghost>
e.g. why choose one over the other?
<ZipCPU>
So, the example I have uses: read_verilog -sv miter_src.v; prep -top miter_src; fmcombine miter ref uut; flatten; opt -fast; and it runs in SymbiYosys under mode bmc
<ZipCPU>
The miter_src is a file including both example logic files, asserting that their outputs are identical
<ZipCPU>
The outputs can be concatenated together, and so look for any output differences
<litghost>
fmcombine is not in the yosys documentation, presumably that is not in the open source version?
<ZipCPU>
No, it's there. You might find the most up to date yosys documentation by running: yosys -p "help fmcombine"
<tpb>
Title: Yosys Open SYnthesis Suite (at www.reddit.com)
<litghost>
ZipCPU: That example uses equiv_struct, which was unable to find places to add $equiv cells
<litghost>
in my case
<ZipCPU>
Do the two designs have different FF structures?
<litghost>
In theory no, one is the post-place and route version of the prior
<ZipCPU>
Do they have the same number of FF's?
<litghost>
ZipCPU: Yes. In fact of the led wires, all but 3 prove equivilant
<ZipCPU>
Do you have a trace showing the differences?
<litghost>
trace?
<ZipCPU>
VCD file?
<litghost>
You mean a testbench wave file?
<ZipCPU>
I mean a counter-example waveform file produced by the formal tools, such as by SymbiYosys when using the script I just mentiond using fmcombine
<litghost>
ZipCPU: I'm not sure how that is done
<ZipCPU>
Can you post a tarball somewhere where I can set see if I can set it up for you?
<ZipCPU>
litghost: The two circuits you gave me are equivalent
<litghost>
ZipCPU: That's great!
<litghost>
ZipCPU: How did you prove it?
<ZipCPU>
I didn't use equiv at all, and threw out the fmcombine and miter stuff, etc
<ZipCPU>
I just created a design containing both, and then asserted that the outputs would always be identical
<ZipCPU>
When running with "abc pdr" as the engine, it was able to prove the two were equivalent
<ZipCPU>
Send me a PM with an e-mail address, and I'll send you a copy of the files I used
<litghost>
Thanks, ideally I'm looking for a solution that just consumes the top level verilog files, and says "yep those are the same". I'll take a look at your approach and think about how to achieve that
<ZipCPU>
Other than the middle file, I think that's what I offered
<ZipCPU>
The trick, though, is that "abc pdr" works on the simpler designs. It will struggle with more complex designs
<ZipCPU>
However, without some form of a full proof, you might only know that the first N clocks have identical outputs, and nothing about anything beyond that
<litghost>
ZipCPU: Thanks, I'll take a look.
<litghost>
ZipCPU: What is a sby file?
<ZipCPU>
A SymbiYosys configuration file
<litghost>
Is see the "[engine]" section, does that translate into a yosys script command?
<ZipCPU>
No
<ZipCPU>
Only the [script] command translates into a yosys script. Even at that, it's not a complete script. SymbiYosys will add more to it
<litghost>
ZipCPU: FYI the miter.vs was not required, the following script is equivilent:
<litghost>
ZipCPU: Thanks for pointing me to how to prove that circuit, I'll take that to my toolbelt for equivalence proving!
<ZipCPU>
;)
kerel has joined #symbiflow
<litghost>
ZipCPU: I just noticed a weird behavior in SymbiYosys, might be a bug
<ZipCPU>
Really? What's that?
<litghost>
ZipCPU: I intentionally broke equivilance, and SymbiYosys started to use other engines
<litghost>
ZipCPU: In particular ones I did not have installed
<ZipCPU>
Oh, dear
<litghost>
File an issue?
<ZipCPU>
What engines did you have installed?
<ZipCPU>
(Probably)
<litghost>
Right now just the ones that Yosys provides
<litghost>
I've make an issue and test case
<ZipCPU>
Which engine did it try to use?
<hackerfoo>
litghost: I need a synthesizable assert, right? Something that just takes a register and sets it high? I don't think `tbassert` is what I need.
<ZipCPU>
asserts are synthesizable?
<litghost>
hackerfoo: Why does it need to be synthesizable? I guess I don't know what you are trying to do
<litghost>
ZipCPU: abc, then yosys-smtbmc (which I have) and then yices-smt2, which I don't
<litghost>
hackerfoo: FYI, the issue is almost certainly on Step 5, and step 5 is missing the really check
<hackerfoo>
I did the first one yesterday, but I would like to have only one testbench that I can use for all steps, and then be able to automate all the steps in the future.
<litghost>
hackerfoo: Which is compare the bit2fasm output from both VPR and Vivado and check to see if things are different
<hackerfoo>
Heh, which step 5? There's two, apparently.
<litghost>
lol
<litghost>
hackerfoo: The second one, post PnR
<litghost>
hackerfoo: I actually think what is written there is incorrect
<litghost>
hackerfoo: The first place to look for a problem if it doesn't work on hardware (after step 2) is to compare bit2fasm output from both VPR and Vivado, especially for new features
<litghost>
hackerfoo: fasm2v is only as good as our understanding of how the FASM features is. If there is a bug in how we understand the FASM features, that will be mirrored in both the arch def and fasm2verilog behavior
<litghost>
hackerfoo: Step 3/4 is worth checking if you are messing with how yosys generates output, but I wouldn't suspect them at the outset
<litghost>
hackerfoo: Step 1/2 is worth doing to make sure the verilog isn't totally bonkers
<hackerfoo>
So then, can I use the testbench I wrote, or do I need one for top.v?
<litghost>
hackerfoo: I don't recommend a testbench at all for debugging VPR PnR errors when we are testing new primatives
<hackerfoo>
I don't have 100% confidence in my verilog yet, either.
<litghost>
hackerfoo: I would do step 2, e.g. make sure when compiled by vivado it works
<litghost>
hackerfoo: And step 1 is good hygien no matter what
<litghost>
hackerfoo: Steps 3/4 are overkill unless you have reason to believe there is a synthesis error, but can always be revisited
<hackerfoo>
I believe mithro recommended I remove the UART and error logic to make it easier to analyze the FASM.
<litghost>
hackerfoo: That was a misstep
<litghost>
hackerfoo: Because there is only 1 DRAM, you can filter the FASM down to the CLB that contains the DRAM
<mithro>
hackerfoo / litghost: I was suggesting that it was easier to write a test bench without the UART / error logic initially
<litghost>
mithro: Oh sure, but that is on the testbench side of thing
<litghost>
s
<hackerfoo>
Okay, I guess I misunderstood. Still, there wasn't a testbench that dumped to a VCD that I could look at.
<litghost>
mithro / hackerfoo : I suspect the error has to do with which FASM features are emitted by VPR, in which case just doing "grep <CLB tile> bit2fasm_VPR.fasm" and "grep <CLB tile> bit2fasm_vivado.fasm" will reveal the problem
<tpb>
Title: RAM32X1D not working · Issue #409 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)
<hackerfoo>
Okay, thanks. I'll try that.
<litghost>
hackerfoo: As part of generating FASM output, you will have a vivado generated bitstream, which you can load and verify that it generates good UART output
<litghost>
hackerfoo: Which resolves the "Step 2" question, e.g. is the verilog remotely correct
<mithro>
btw litghost, hackerfoo was suggesting we add a build target to run the verilog through vivado and produce a .bit + .fasm files, what do you think?
<hackerfoo>
Is there a documented way to get FASM output from Vivado? I don't think it runs when building *_bin or *_prog.
<litghost>
One minute
<litghost>
hackerfoo: Vivado doesn't get invoke from symbiflow at all, you'll need a prjxray tree checked out if you don't already have one
<litghost>
hackerfoo: I'm tarring up an example script for running the vivado flow and getting FASM out
<litghost>
hackerfoo: Once you have prjxray checked out, run the shell script download-latest-db.sh
<litghost>
hackerfoo: And then source database/artix7/settings.sh and then source minitests/roi_harness/basys3-swbut.sh
<litghost>
hackerfoo: That will set up the required environment variables to make everything line up
<litghost>
hackerfoo: And you need to set XRAY_VIVADO_SETTINGS to point to the vivado settings.sh per the prjxray README
<litghost>
hackerfoo: Then run "runme.sh" and it will do the rest
<litghost>
hackerfoo: Just follow the startup steps in the README actually, it's mostly documented in there, minus sourcing minitests/roi_harness/basys3-swbut.sh
<hackerfoo>
Thanks
<litghost>
hackerfoo: One additional thing, the output from bit2fasm has some additional pretty grouping that the output from VPR doesn't. If you want to compare files with "diff", I recommend generating the FASM from the VPR bitstream. The ${target}_bit_v will do this automatically as a side product
<litghost>
hackerfoo: However if you are generating from vivado, "diff" isn't useful because Vivado doesn't respect the way we have setup the ROI
<litghost>
hackerfoo: So greping each files for the relevant 10 or so lines is the right idea
gruetzkopf has joined #symbiflow
<hackerfoo>
Do you think it would work if I just sort the lines? The order doesn't matter, right?
<litghost>
hackerfoo: Vivado and VPR will choose different CLBs, you'll need to narrow the output
<litghost>
hackerfoo: If you want, you could create a constrain on vivado for the CLB tile, but the difference is usually pretty obvious