| *** tpb has joined #symbiflow | 00:00 | |
| duck2 | hehe i just noticed the rapidsmith site is a .doc file saved as .html | 01:48 |
|---|---|---|
| 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 | 01:58 |
| duck2 | ex 4 takes 34mb in java heap). unfortunately not much information on this is given on the site. | 01:58 |
| mithro | duck2: I assume they expand the graph on demand | 01:59 |
| duck2 | looks like wires(nodes) are enhanced int objects which run queries on the file when they are asked about their edges | 01:59 |
| duck2 | only a guess | 02:00 |
| 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 | 02:04 |
| mithro | duck2: A lot of that data is de-duplicatable | 02:05 |
| mithro | duck2: I assume they store the data in a similar manner to tileconn | 02:08 |
| 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 | 02:08 |
| duck2 | ok. i should take a look at the rapidsmith source sometime. | 02:14 |
| duck2 | nextpnr also does not load a flattened graph in memory afaik | 02:16 |
| 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 | 02:18 |
| hackerfoo | I wrote a testbench. It works! | 02:29 |
| * hackerfoo uploaded an image: ram_test_tb.jpg (208KB) < http://sandbox.hackerfoo.com:8008/_matrix/media/v1/download/sandbox.hackerfoo.com/xmhDmyWtEFhkkjfXjnzpqzDO > | 02:30 | |
| * hackerfoo uploaded an image: ram_test_tb.jpg (195KB) < http://sandbox.hackerfoo.com:8008/_matrix/media/v1/download/sandbox.hackerfoo.com/lJztGzfzmZZTfKVohAxsNYWN > | 02:31 | |
| *** Bertl is now known as Bertl_zZ | 02:55 | |
| *** citypw has joined #symbiflow | 03:17 | |
| *** proteusguy has quit IRC | 04:30 | |
| *** proteusguy has joined #symbiflow | 06:10 | |
| *** OmniMancer has joined #symbiflow | 06:31 | |
| *** futarisIRCcloud has quit IRC | 07:56 | |
| *** futarisIRCcloud has joined #symbiflow | 07:57 | |
| *** swick has quit IRC | 08:09 | |
| *** citypw has quit IRC | 09:45 | |
| *** Bertl_zZ is now known as Bertl | 11:29 | |
| *** proteusguy has quit IRC | 11:55 | |
| *** GuzTech has joined #symbiflow | 11:58 | |
| 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 | 12:22 |
| sf-slack | it places the cluster in the equivalent tile. | 12:22 |
| tpb | Title: WIP: Equivalent tiles VTR feature by acomodi · Pull Request #36 · SymbiFlow/vtr-verilog-to-routing · GitHub (at github.com) | 12:22 |
| sf-slack | <acomodi> I still need to adapt the `swap` algorithm to look for more suitable location in equivalent tiles (if they exist) | 12:24 |
| *** futarisIRCcloud has quit IRC | 12:26 | |
| *** futarisIRCcloud has joined #symbiflow | 12:57 | |
| 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 | 14:05 |
| 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 | 14:06 |
| sf-slack | <kgugala> this option is pretty straight forward - it will add one step between xml merging and carry chains specialization | 14:07 |
| sf-slack | <kgugala> I'm not sure if this scales, though | 14:07 |
| sf-slack | <kgugala> the second option is to generate all the arch xmls from verilog (this is something @mithro mentioned some time ago) | 14:08 |
| sf-slack | <kgugala> this is much more work, because we'd need to reimplment all the arch.xml generation | 14:09 |
| sf-slack | <kgugala> but this would allow us to create verilog templates for every BEL and CLB structure | 14:09 |
| sf-slack | <kgugala> a separate script can use the verlilog templates and merge them with timings from sdf | 14:10 |
| sf-slack | <kgugala> in the end v2x tool can generate arch xml | 14:10 |
| sf-slack | <kgugala> this approach is much more versatile, but requires more work | 14:11 |
| sf-slack | <kgugala> what do you think | 14:11 |
| 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) | 14:16 |
| 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 | 14:55 |
| litghost | kgugala: I think we should proceed with a v2x solution, with the follow caveat: Let's write tests as we god | 14:58 |
| litghost | go* | 14:58 |
| litghost | kgugala: I am working on some FF tests, which also does a little combintorial testing | 14:58 |
| hackerfoo | litghost: I'm just getting started (ignore the formatting): https://github.com/HackerFoo/symbiflow-arch-defs/commit/f84b36f3e1ef9ed6b3a21b257ad94b2c394b53d1 | 14:59 |
| tpb | Title: WIP · HackerFoo/symbiflow-arch-defs@f84b36f · GitHub (at github.com) | 14:59 |
| sf-slack | <kgugala> HW tests, or some PnR tests? | 14:59 |
| sf-slack | <kgugala> HW :slightly_smiling_face: | 14:59 |
| litghost | kgugala: Kind of both | 14:59 |
| litghost | kgugala: equivilance tests | 14:59 |
| litghost | kgugala: Now that fasm2verilog is working, we can actually check logical equivilance | 15:00 |
| sf-slack | <kgugala> I see | 15:00 |
| hackerfoo | I'd like to somehow automatically generate a testbench for each type of memory, but I figured I'd start by just making a copy per type. | 15:00 |
| litghost | kgugala: We also have firm evidence in the scalable proc test that we already have a correctness issue | 15:00 |
| hackerfoo | And then I need to add some type of automatic verification, so the test just passes or fails without looking at the trace. | 15:01 |
| sf-slack | <kgugala> OK, I'll start working on the verilog models which can be used with v2x to generate the arch.xml | 15:01 |
| sf-slack | <kgugala> BTW I noticed we're missing a lot of delay definitions in arch.xml | 15:02 |
| litghost | kgugala: We'll likely need to fan out this work, so I'd focus on a small conversion and then pause for documentation | 15:02 |
| sf-slack | <kgugala> e.g in FFs we don't have a definition of any combinational path | 15:03 |
| sf-slack | <kgugala> the fuzzer actually gets those values | 15:03 |
| sf-slack | <kgugala> so we can include this info | 15:03 |
| sf-slack | <acomodi> I don't know if it can help, but here there's the PR relative to v2x I created a few months ago: https://github.com/SymbiFlow/symbiflow-arch-defs/pull/316 | 15:03 |
| tpb | Title: WIP: Improve the Verilog to XML conversion process by acomodi · Pull Request #316 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com) | 15:03 |
| 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. | 15:06 |
| litghost | mkurc: Is your latest stuff pushed to the PR? | 15:07 |
| sf-slack | <mkurc> @litghost Yes | 15:07 |
| sf-slack | <mkurc> @litghost But I still cannot find a solution of the problem with routing of const nets | 15:08 |
| litghost | mkurc: I just made a suggsetion | 15:08 |
| sf-slack | <mkurc> @litghost Thx, I'll try right away | 15:09 |
| *** GuzTech has quit IRC | 15:14 | |
| litghost | hackerfoo: https://github.com/SymbiFlow/symbiflow-arch-defs/blob/587f11d2d3124cb4fc22436a100e24aae655e64d/xc7/tests/ff_sr_ce/ff_ce_sr_testbench.v | 15:23 |
| tpb | Title: symbiflow-arch-defs/ff_ce_sr_testbench.v at 587f11d2d3124cb4fc22436a100e24aae655e64d · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com) | 15:23 |
| litghost | hackerfoo: I need to move the assert out of that testbench and into a library | 15:24 |
| sf-slack | <mkurc> @litghost: Adding --bb_factor 10 did not help. | 15:28 |
| sf-slack | <mkurc> @litghost I am inspecting the "routing resources" using the VPR gui and the global GND net is correctly connected to the GND tile. | 15:29 |
| sf-slack | <mkurc> @litghost But I cannot see a possible connection from the GND net to the CLB of interest. | 15:31 |
| litghost | mkurc: I recommend tracing with grep | 15:31 |
| litghost | mkurc: Or writing a tool to specifically walk the routing from source to sink | 15:32 |
| sf-slack | <mkurc> @litghost Yes, I was thinking of creating such a tool. I assume that there isn't any. | 15:33 |
| litghost | mkurc: There is something like it, but I would start from scratch and make a small simple one | 15:33 |
| *** OmniMancer has quit IRC | 15:33 | |
| litghost | mkurc: Focus on just doing 1 src to 1 sink | 15:33 |
| sf-slack | <mkurc> @litghost Yep | 15:35 |
| *** futarisIRCcloud has quit IRC | 15:36 | |
| litghost | hackerfoo: I've updated my PR with the tbassert in an include file, so you could use it (or make suggestions for improvements) | 15:50 |
| hackerfoo | litghost: Thanks, I'll look at it. | 15:52 |
| mithro | hackerfoo: I wonder if you need some init values for things there? | 15:53 |
| hackerfoo | mithro: In my testbench? It starts with `nrst` low, which should take care of it. | 15:59 |
| hackerfoo | I took most of the code out of top.v, and it does the same. | 16:02 |
| *** OmniMancer has joined #symbiflow | 16:06 | |
| *** OmniMancer has quit IRC | 16:07 | |
| litghost | mithro: https://github.com/SymbiFlow/symbiflow-arch-defs/pull/556#discussion_r274033131 Should we just remove the extra bash stuff, I don't see a need for it | 16:11 |
| tpb | Title: Enable kokoro on symbiflow-arch-defs by litghost · Pull Request #556 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com) | 16:11 |
| 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 | 16:15 |
| 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? | 16:20 |
| hackerfoo | Nevermind, I see "ifdef" in the code. | 16:20 |
| 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 | 16:23 |
| litghost | hackerfoo: Maybe two testbench's are needed for your purpose | 16:23 |
| mithro | litghost: We currently run out of io pins if you try and place and route the non-top.v module, right? | 16:24 |
| litghost | mithro: That is one problem, yes | 16:24 |
| litghost | mithro: ROI breakout would help with that | 16:24 |
| litghost | mithro: But in this case running the UART on both sides of the top module is probably a good idea | 16:25 |
| *** kc8apf has left #symbiflow | 16:26 | |
| mithro | litghost: I think we probably want a test helper with the uart then | 16:29 |
| litghost | mithro: Don't disagree | 16:29 |
| litghost | mithro: The UART module itself can serve that purpose, combined with a deframer/read queue | 16:30 |
| 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 | 16:31 |
| litghost | current UART module* | 16:31 |
| mithro | litghost: BTW - Have you seen ZipCPU's blog about formal stuff? https://zipcpu.com/formal/formal.html ? | 16:32 |
| tpb | Title: The ZipCPU by Gisselquist Technology (at zipcpu.com) | 16:32 |
| mithro | He has a Makefile for formal proofs with SymbiYosys at -> https://zipcpu.com/zipcpu/2018/12/20/sby-makefile.html | 16:33 |
| tpb | Title: Makefiles for formal proofs with SymbiYosys (at zipcpu.com) | 16:33 |
| mithro | Dunno if that is useful at all... | 16:33 |
| litghost | mithro: I think that is for build up of cumulative proofs | 16:34 |
| litghost | mithro: I think most of our proofs should be single instance | 16:34 |
| litghost | mithro: If we try to prove say, the picosoc, then that will be usefull | 16:35 |
| mithro | litghost: If the proofs work on the original verilog, they should still work on the verilog from the bitstream, right? | 16:35 |
| litghost | mithro: We haven't been proving the original verilog though | 16:35 |
| litghost | mithro: To date, we've been proving that pre-synthesis is equivilant to post-PnR | 16:35 |
| litghost | mithro: I believe those links are about proving verilog "assume" statements | 16:36 |
| litghost | mithro: Which would be lost through the PnR process | 16:36 |
| litghost | mithro: That being said the documentation (including that blog) on the Yosys proving process is pretty terrible | 16:36 |
| litghost | mithro: The Yosys documentation on $equiv cells is literally a TODO | 16:37 |
| *** proteusguy has joined #symbiflow | 16:39 | |
| mithro | litghost: You could try poking zipcpu and daveshah in #yosys | 16:39 |
| litghost | mithro: Nah, I think the problem I have is an actual error, either in our PnR or fasm2verilog | 16:40 |
| litghost | mithro: I was stuck for a bit, but the testbench will help prove to myself that the equivilance error is real | 16:40 |
| mithro | litghost: I think we should poke zipcpu about doing a tutorial about equivalence proving anyway | 16:40 |
| hackerfoo | litghost: Maybe it would be best to just use a single error signal pin for testbenches instead of a full UART. | 16:41 |
| litghost | mithro: If I find that I cannot replicate the equivalence failure in the TB, I'll poke upstream | 16:41 |
| *** ZipCPU has joined #symbiflow | 16:41 | |
| litghost | hackerfoo: Sure, and on hardware just have the pin connect to an LED? That will work | 16:41 |
| hackerfoo | One reason I want to avoid complexity is to make the FASM easier to analyze. | 16:42 |
| ZipCPU | Hello, mithro | 16:42 |
| mithro | ZipCPU: we were just chatting about formal equivalence proving | 16:42 |
| ZipCPU | Alright, wow, go on | 16:42 |
| mithro | ZipCPU: I was saying that your other formal tutorials / blog posts are pretty good | 16:43 |
| * ZipCPU is looking through the log for some context | 16:43 | |
| mithro | and litghost was complaining "The Yosys documentation on $equiv cells is literally a TODO" | 16:43 |
| litghost | ZipCPU: i was say that the equiv documentation in the yosys manual is pretty close to non-existant | 16:43 |
| ZipCPU | That's pretty close to reality | 16:43 |
| ZipCPU | It's not an "advertised" feature | 16:43 |
| litghost | lol | 16:44 |
| ZipCPU | I've tried to help coach some folks through it before, but it's always befuddled the both of us | 16:44 |
| mithro | ZipCPU: so, was wondering if we could persuade you to look into documentation :-P | 16:44 |
| ZipCPU | Supposedly SymbiYosys can do it, I just haven't been successful at it | 16:44 |
| litghost | e.g. it has the documentation? | 16:44 |
| ZipCPU | Well, back up a bit, what are you trying to do? | 16:44 |
| ZipCPU | What type of equivalence checking? | 16:44 |
| ZipCPU | Some types are doable, some not so much | 16:45 |
| 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 | 16:46 |
| hackerfoo | How many bits? Up to 32 bits of input + state is easy. | 16:46 |
| litghost | Relevant design: https://github.com/litghost/symbiflow-arch-defs/blob/76e136c1b290073b3176e46e763f5386527081f4/xc7/tests/ff_sr_ce/ff_ce_sr.v | 16:46 |
| tpb | Title: symbiflow-arch-defs/ff_ce_sr.v at 76e136c1b290073b3176e46e763f5386527081f4 · litghost/symbiflow-arch-defs · GitHub (at github.com) | 16:46 |
| litghost | Using the following yosys script: https://github.com/litghost/symbiflow-arch-defs/blob/76e136c1b290073b3176e46e763f5386527081f4/yosys/equiv_simple_opt_full.ys | 16:47 |
| ZipCPU | That looks like 16 FFs ;) | 16:47 |
| tpb | Title: symbiflow-arch-defs/equiv_simple_opt_full.ys at 76e136c1b290073b3176e46e763f5386527081f4 · litghost/symbiflow-arch-defs · GitHub (at github.com) | 16:47 |
| litghost | Indeed, sorry, trying to say 1 FF per input | 16:47 |
| hackerfoo | So, 32 bits then? | 16:47 |
| litghost | What is interesting is the led[9] led[10] and led[11] are failing to prove | 16:48 |
| litghost | If I change the xor reduce to say Q[5:0 | 16:48 |
| litghost | It proves | 16:48 |
| hackerfoo | Check all 4 billion cases. Should take a few minutes on hardware. | 16:48 |
| litghost | But Q[7:0] fails | 16:48 |
| litghost | hackerfoo: The goal is to have a test that runs without hardware | 16:49 |
| *** alexhw has joined #symbiflow | 16:49 | |
| 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 | 16:49 |
| litghost | ZipCPU: Or simply a case where the equiv check cannot prove the situation | 16:50 |
| hackerfoo | litghost: Oh, well then can you use Verilator? | 16:50 |
| ZipCPU | Heh, yeah, one of the reasons why the equivalency support isn't yet "advertised" ;) | 16:50 |
| *** bubble_buster has joined #symbiflow | 16:50 | |
| ZipCPU | So, there's a couple of basic types of equivalency checking | 16:51 |
| ZipCPU | One checks things from the top level inputs and outputs alone. | 16:51 |
| litghost | I'm currently use the equiv cells at top level inputs and outputs | 16:51 |
| ZipCPU | The second type does a check between FFs | 16:51 |
| litghost | You are refering to equiv_struct? | 16:51 |
| litghost | for the second type | 16:51 |
| 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 | 16:52 |
| litghost | Yosys was unable to add equiv cells using equiv_struct | 16:52 |
| litghost | I wasn't able to diagnose why that was the case | 16:52 |
| litghost | FYI, I am using latest Yosys master as of yesterday | 16:53 |
| * ZipCPU is browsing yosys doc's, for anything starting with "equiv" | 16:53 | |
| litghost | It's pretty sparse | 16:54 |
| * ZipCPU reads the "miter" page ... | 16:54 | |
| litghost | ZipCPU: miter might make this worse, it only adds the equiv cell for the 1 output yes? | 16:55 |
| ZipCPU | No, it's much more powerful than that | 16:55 |
| litghost | What is the relative utility of equiv_make and miter -equiv? | 16:55 |
| litghost | e.g. why choose one over the other? | 16:56 |
| 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 | 16:57 |
| ZipCPU | The miter_src is a file including both example logic files, asserting that their outputs are identical | 16:57 |
| ZipCPU | The outputs can be concatenated together, and so look for any output differences | 16:57 |
| litghost | fmcombine is not in the yosys documentation, presumably that is not in the open source version? | 16:59 |
| ZipCPU | No, it's there. You might find the most up to date yosys documentation by running: yosys -p "help fmcombine" | 17:00 |
| litghost | I guess http://www.clifford.at/yosys/files/yosys_manual.pdf hasn't been updated then | 17:00 |
| ZipCPU | I was looking at http://www.clifford.at/yosys/documentation.html and coming to the same conclusion | 17:01 |
| tpb | Title: Yosys Open SYnthesis Suite :: Documentation (at www.clifford.at) | 17:01 |
| litghost | ZipCPU: If I understand fmcombine, if I have two top-level sources, "miter -equiv" + "fmcombine" will do the job? | 17:02 |
| ZipCPU | In the example I have, you have three toplevel sources. The first is your original design. The second is your modified design. | 17:03 |
| ZipCPU | The third source is the miter_src file. The example I have, that I've started to work from, uses a hand-built miter_src file | 17:03 |
| ZipCPU | For example .... | 17:04 |
| litghost | ZipCPU: What I am suggesting is use "miter -equiv" to build the "third source" so to speak | 17:04 |
| litghost | ZipCPU: So that it doesn't need to be hand generated | 17:04 |
| ZipCPU | Here's the example of my "third source": https://gist.github.com/ZipCPU/cc707c81baa7b438f38b81608837e91e | 17:05 |
| tpb | Title: filter_miter.sv · GitHub (at gist.github.com) | 17:05 |
| ZipCPU | I haven't managed to get Clifford to teach me how this equivalency is supposed to work. I only have the one example to work from. | 17:05 |
| litghost | lol | 17:05 |
| *** OmniMancer has joined #symbiflow | 17:05 | |
| ZipCPU | I think it's on the to-do list, I just haven't had the opportunity to learn it yet | 17:06 |
| litghost | What you have written in that third source is pretty close to what I believe "miter -equiv" builds | 17:06 |
| ZipCPU | There was a recent reddit post on this topic though .... | 17:06 |
| litghost | I don't believe random reddit posts makes for good documentation ... | 17:06 |
| ZipCPU | This is why it isn't an "advertised" feature | 17:06 |
| ZipCPU | Check https://www.reddit.com/r/yosys The second item down is on equivalence checking | 17:07 |
| tpb | Title: Yosys Open SYnthesis Suite (at www.reddit.com) | 17:07 |
| litghost | ZipCPU: That example uses equiv_struct, which was unable to find places to add $equiv cells | 17:08 |
| litghost | in my case | 17:08 |
| ZipCPU | Do the two designs have different FF structures? | 17:09 |
| litghost | In theory no, one is the post-place and route version of the prior | 17:10 |
| ZipCPU | Do they have the same number of FF's? | 17:11 |
| litghost | ZipCPU: Yes. In fact of the led wires, all but 3 prove equivilant | 17:12 |
| ZipCPU | Do you have a trace showing the differences? | 17:12 |
| litghost | trace? | 17:13 |
| ZipCPU | VCD file? | 17:13 |
| litghost | You mean a testbench wave file? | 17:14 |
| 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 | 17:15 |
| litghost | ZipCPU: I'm not sure how that is done | 17:15 |
| ZipCPU | Can you post a tarball somewhere where I can set see if I can set it up for you? | 17:16 |
| litghost | Gimme a minute | 17:16 |
| litghost | FYI, you will need https://github.com/YosysHQ/yosys/pull/928 | 17:17 |
| tpb | Title: Add additional cells sim models for core 7-series primitives. by litghost · Pull Request #928 · YosysHQ/yosys · GitHub (at github.com) | 17:17 |
| litghost | ZipCPU: There should be two verilog files, in theory they are the same design https://usercontent.irccloud-cdn.com/file/iHYHJw73/ff_ce_sr_equiv.tgz | 17:19 |
| *** Bertl is now known as Bertl_oO | 17:36 | |
| ZipCPU | Hmm ... ERROR: Module \FDRE referenced in mo... is not part of the design ... | 17:37 |
| litghost | You need to run "read_verilog +/techlibs/cells_sim.v" | 17:38 |
| litghost | You need to run "read_verilog +/xilinx/cells_sim.v" | 17:38 |
| litghost | Then run a pass to lower from the xilinx tech library to the yosys primatives | 17:39 |
| ZipCPU | Now I think I need your pull update ... | 17:39 |
| litghost | You do, because I'm using primatives that were missing from cells_sim.v | 17:39 |
| ZipCPU | Got it ... on to the fmcombine step | 17:42 |
| * ZipCPU steps away, having been called to another task | 17:50 | |
| litghost | ZipCPU: Okay. If you have any hints, do tell. Otherwise I'll wait till your back | 17:51 |
| *** OmniMancer has quit IRC | 18:07 | |
| *** adjtm has joined #symbiflow | 18:19 | |
| * litghost mithro: https://github.com/SymbiFlow/prjxray/pull/773 | 19:05 | |
| ZipCPU | litghost: The two circuits you gave me are equivalent | 19:09 |
| litghost | ZipCPU: That's great! | 19:09 |
| litghost | ZipCPU: How did you prove it? | 19:09 |
| ZipCPU | I didn't use equiv at all, and threw out the fmcombine and miter stuff, etc | 19:09 |
| ZipCPU | I just created a design containing both, and then asserted that the outputs would always be identical | 19:10 |
| ZipCPU | When running with "abc pdr" as the engine, it was able to prove the two were equivalent | 19:10 |
| ZipCPU | Send me a PM with an e-mail address, and I'll send you a copy of the files I used | 19:11 |
| 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 | 19:14 |
| ZipCPU | Other than the middle file, I think that's what I offered | 19:31 |
| ZipCPU | The trick, though, is that "abc pdr" works on the simpler designs. It will struggle with more complex designs | 19:32 |
| 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 | 19:32 |
| litghost | ZipCPU: Thanks, I'll take a look. | 19:44 |
| litghost | ZipCPU: What is a sby file? | 19:54 |
| ZipCPU | A SymbiYosys configuration file | 19:54 |
| litghost | Is see the "[engine]" section, does that translate into a yosys script command? | 19:55 |
| ZipCPU | No | 19:56 |
| 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 | 19:57 |
| litghost | ZipCPU: FYI the miter.vs was not required, the following script is equivilent: | 20:11 |
| litghost | read_verilog +/xilinx/cells_sim.v | 20:11 |
| litghost | read_verilog -sv ff_ce_sr_4.v | 20:11 |
| litghost | rename top gold | 20:11 |
| litghost | read_verilog -sv top_bit.v | 20:11 |
| litghost | rename top gate | 20:11 |
| litghost | miter -equiv -make_assert gold gate miter | 20:11 |
| litghost | prep -top miter | 20:11 |
| ZipCPU | Ok | 20:11 |
| *** adjtm_ has joined #symbiflow | 20:27 | |
| *** adjtm has quit IRC | 20:30 | |
| litghost | ZipCPU: Thanks for pointing me to how to prove that circuit, I'll take that to my toolbelt for equivalence proving! | 21:02 |
| ZipCPU | ;) | 21:02 |
| *** kerel has joined #symbiflow | 21:16 | |
| litghost | ZipCPU: I just noticed a weird behavior in SymbiYosys, might be a bug | 21:24 |
| ZipCPU | Really? What's that? | 21:25 |
| litghost | ZipCPU: I intentionally broke equivilance, and SymbiYosys started to use other engines | 21:25 |
| litghost | ZipCPU: In particular ones I did not have installed | 21:25 |
| ZipCPU | Oh, dear | 21:25 |
| litghost | File an issue? | 21:25 |
| ZipCPU | What engines did you have installed? | 21:25 |
| ZipCPU | (Probably) | 21:25 |
| litghost | Right now just the ones that Yosys provides | 21:26 |
| litghost | I've make an issue and test case | 21:26 |
| ZipCPU | Which engine did it try to use? | 21:26 |
| 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. | 21:26 |
| ZipCPU | asserts are synthesizable? | 21:27 |
| litghost | hackerfoo: Why does it need to be synthesizable? I guess I don't know what you are trying to do | 21:27 |
| litghost | ZipCPU: abc, then yosys-smtbmc (which I have) and then yices-smt2, which I don't | 21:28 |
| hackerfoo | litghost: I'm trying to follow this approach to check where RAM32X1D fails: https://docs.google.com/document/d/11wJUvr2aVBkUiuYYsFN07jkoYr_ccWlLLLFH8YQw8uQ/edit?usp=sharing | 21:29 |
| litghost | hackerfoo: Which step are you on? | 21:30 |
| litghost | hackerfoo: FYI, the issue is almost certainly on Step 5, and step 5 is missing the really check | 21:31 |
| 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. | 21:32 |
| litghost | hackerfoo: Which is compare the bit2fasm output from both VPR and Vivado and check to see if things are different | 21:32 |
| hackerfoo | Heh, which step 5? There's two, apparently. | 21:32 |
| litghost | lol | 21:32 |
| litghost | hackerfoo: The second one, post PnR | 21:33 |
| litghost | hackerfoo: I actually think what is written there is incorrect | 21:33 |
| 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 | 21:33 |
| 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 | 21:34 |
| 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 | 21:35 |
| litghost | hackerfoo: Step 1/2 is worth doing to make sure the verilog isn't totally bonkers | 21:36 |
| hackerfoo | So then, can I use the testbench I wrote, or do I need one for top.v? | 21:36 |
| litghost | hackerfoo: I don't recommend a testbench at all for debugging VPR PnR errors when we are testing new primatives | 21:36 |
| hackerfoo | I don't have 100% confidence in my verilog yet, either. | 21:37 |
| litghost | hackerfoo: I would do step 2, e.g. make sure when compiled by vivado it works | 21:37 |
| litghost | hackerfoo: And step 1 is good hygien no matter what | 21:37 |
| litghost | hackerfoo: Steps 3/4 are overkill unless you have reason to believe there is a synthesis error, but can always be revisited | 21:37 |
| hackerfoo | I believe mithro recommended I remove the UART and error logic to make it easier to analyze the FASM. | 21:38 |
| litghost | hackerfoo: That was a misstep | 21:38 |
| litghost | hackerfoo: Because there is only 1 DRAM, you can filter the FASM down to the CLB that contains the DRAM | 21:38 |
| mithro | hackerfoo / litghost: I was suggesting that it was easier to write a test bench without the UART / error logic initially | 21:38 |
| litghost | mithro: Oh sure, but that is on the testbench side of thing | 21:39 |
| litghost | s | 21:39 |
| hackerfoo | Okay, I guess I misunderstood. Still, there wasn't a testbench that dumped to a VCD that I could look at. | 21:39 |
| 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 | 21:39 |
| litghost | mithro / hackerfoo : If there is a suspect routing error, then equivilance testing is a good tool, along with a testbench, e.g. what I'm doing in https://github.com/SymbiFlow/symbiflow-arch-defs/pull/570 | 21:40 |
| tpb | Title: Add asserts for combintorial output combiner. by litghost · Pull Request #570 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com) | 21:40 |
| litghost | hackerfoo: I think no matter what, fixing https://github.com/SymbiFlow/symbiflow-arch-defs/issues/558 is a good idea | 21:41 |
| litghost | hackerfoo: I believe it was working in the past, and helped me to debug a "Step 2" class issue, e.g. the verilog was just wrong | 21:41 |
| hackerfoo | It's worth fixing, but how will it help me? I already have a working testbench. | 21:43 |
| litghost | hackerfoo: Oh it won't, but I don't think a testbench will help either, depending on where the true problem lies | 21:44 |
| hackerfoo | My understanding is that autosim fuzzes the inputs? | 21:44 |
| litghost | hackerfoo: Autosim just provides a clk | 21:44 |
| litghost | hackerfoo: Which in the case of the dram test is enough | 21:44 |
| litghost | hackerfoo: I wrote the DRAM test to be completely automatic, so as long as there is a clock it will run without other input | 21:45 |
| hackerfoo | I want to focus on fixing https://github.com/SymbiFlow/symbiflow-arch-defs/issues/409 , then I can work on improving the general state of things. | 21:45 |
| tpb | Title: RAM32X1D not working · Issue #409 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com) | 21:45 |
| litghost | hackerfoo: If you want to fix https://github.com/SymbiFlow/symbiflow-arch-defs/issues/409 I recommend jumping straight to comparing FASM output from VPR and Vivado | 21:47 |
| tpb | Title: RAM32X1D not working · Issue #409 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com) | 21:47 |
| hackerfoo | Okay, thanks. I'll try that. | 21:47 |
| 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 | 21:48 |
| litghost | hackerfoo: Which resolves the "Step 2" question, e.g. is the verilog remotely correct | 21:48 |
| 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? | 21:48 |
| hackerfoo | Is there a documented way to get FASM output from Vivado? I don't think it runs when building *_bin or *_prog. | 21:48 |
| litghost | One minute | 21:49 |
| 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 | 21:51 |
| litghost | hackerfoo: I'm tarring up an example script for running the vivado flow and getting FASM out | 21:51 |
| hackerfoo | Thanks | 21:52 |
| litghost | hackerfoo: Here ya go https://usercontent.irccloud-cdn.com/file/qSucpnD1/test_dram.tgz | 21:53 |
| litghost | hackerfoo: Once you have prjxray checked out, run the shell script download-latest-db.sh | 21:53 |
| litghost | hackerfoo: And then source database/artix7/settings.sh and then source minitests/roi_harness/basys3-swbut.sh | 21:54 |
| litghost | hackerfoo: That will set up the required environment variables to make everything line up | 21:54 |
| litghost | hackerfoo: And you need to set XRAY_VIVADO_SETTINGS to point to the vivado settings.sh per the prjxray README | 21:54 |
| litghost | hackerfoo: Then run "runme.sh" and it will do the rest | 21:55 |
| 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 | 21:57 |
| hackerfoo | Thanks | 22:00 |
| 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 | 22:08 |
| 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 | 22:09 |
| litghost | hackerfoo: So greping each files for the relevant 10 or so lines is the right idea | 22:09 |
| *** gruetzkopf has joined #symbiflow | 22:10 | |
| hackerfoo | Do you think it would work if I just sort the lines? The order doesn't matter, right? | 22:12 |
| litghost | hackerfoo: Vivado and VPR will choose different CLBs, you'll need to narrow the output | 22:14 |
| litghost | hackerfoo: If you want, you could create a constrain on vivado for the CLB tile, but the difference is usually pretty obvious | 22:15 |
| hackerfoo | Okay | 22:15 |
| mithro | litghost: https://github.com/SymbiFlow/prjxray/issues/774 | 23:46 |
| tpb | Title: Figure out why prjxray database builds have gone up to 4h · Issue #774 · SymbiFlow/prjxray · GitHub (at github.com) | 23:46 |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!