Wednesday, 2019-04-10

*** tpb has joined #symbiflow00:00
duck2hehe i just noticed the rapidsmith site is a .doc file saved as .html01:48
duck2mithro: 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 virt01:58
duck2ex 4 takes 34mb in java heap). unfortunately not much information on this is given on the site.01:58
mithroduck2: I assume they expand the graph on demand01:59
duck2looks like wires(nodes) are enhanced int objects which run queries on the file when they are asked about their edges01:59
duck2only a guess02:00
duck2mithro: 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 metadata02:04
mithroduck2: A lot of that data is de-duplicatable02:05
mithroduck2: I assume they store the data in a similar manner to tileconn02:08
mithroduck2: 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 tomorrow02:08
duck2ok. i should take a look at the rapidsmith source sometime.02:14
duck2nextpnr also does not load a flattened graph in memory afaik02:16
mithroduck2: 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 point02:18
hackerfooI 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_zZ02:55
*** citypw has joined #symbiflow03:17
*** proteusguy has quit IRC04:30
*** proteusguy has joined #symbiflow06:10
*** OmniMancer has joined #symbiflow06:31
*** futarisIRCcloud has quit IRC07:56
*** futarisIRCcloud has joined #symbiflow07:57
*** swick has quit IRC08:09
*** citypw has quit IRC09:45
*** Bertl_zZ is now known as Bertl11:29
*** proteusguy has quit IRC11:55
*** GuzTech has joined #symbiflow11: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 anymore12:22
sf-slackit places the cluster in the equivalent tile.12:22
tpbTitle: 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 IRC12:26
*** futarisIRCcloud has joined #symbiflow12: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 options14: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 fuzzer14:06
sf-slack<kgugala> this option is pretty straight forward - it will add one step between xml merging and carry chains specialization14:07
sf-slack<kgugala> I'm not sure if this scales, though14: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 generation14:09
sf-slack<kgugala> but this would allow us to create verilog templates for every BEL and CLB structure14:09
sf-slack<kgugala> a separate script can use the verlilog templates and merge them with timings from sdf14:10
sf-slack<kgugala> in the end v2x tool can generate arch xml14:10
sf-slack<kgugala> this approach is much more versatile, but requires more work14:11
sf-slack<kgugala> what do you think14: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
litghosthackerfoo: 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 kind14:55
litghostkgugala: I think we should proceed with a v2x solution, with the follow caveat: Let's write tests as we god14:58
litghostgo*14:58
litghostkgugala: I am working on some FF tests, which also does a little combintorial testing14:58
hackerfoolitghost: I'm just getting started (ignore the formatting): https://github.com/HackerFoo/symbiflow-arch-defs/commit/f84b36f3e1ef9ed6b3a21b257ad94b2c394b53d114:59
tpbTitle: WIP · HackerFoo/[email protected] · 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
litghostkgugala: Kind of both14:59
litghostkgugala: equivilance tests14:59
litghostkgugala: Now that fasm2verilog is working, we can actually check logical equivilance15:00
sf-slack<kgugala> I see15:00
hackerfooI'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
litghostkgugala: We also have firm evidence in the scalable proc test that we already have a correctness issue15:00
hackerfooAnd 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.xml15:01
sf-slack<kgugala> BTW I noticed we're missing a lot of delay definitions in arch.xml15:02
litghostkgugala: We'll likely need to fan out this work, so I'd focus on a small conversion and then pause for documentation15:02
sf-slack<kgugala> e.g in FFs we don't have a definition of any combinational path15:03
sf-slack<kgugala> the fuzzer actually gets those values15:03
sf-slack<kgugala> so we can include this info15: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/31615:03
tpbTitle: 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
litghostmkurc: Is your latest stuff pushed to the PR?15:07
sf-slack<mkurc> @litghost Yes15:07
sf-slack<mkurc> @litghost But I still cannot find a solution of the problem with routing of const nets15:08
litghostmkurc: I just made a suggsetion15:08
sf-slack<mkurc> @litghost Thx, I'll try right away15:09
*** GuzTech has quit IRC15:14
litghosthackerfoo: https://github.com/SymbiFlow/symbiflow-arch-defs/blob/587f11d2d3124cb4fc22436a100e24aae655e64d/xc7/tests/ff_sr_ce/ff_ce_sr_testbench.v15:23
tpbTitle: symbiflow-arch-defs/ff_ce_sr_testbench.v at 587f11d2d3124cb4fc22436a100e24aae655e64d · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)15:23
litghosthackerfoo: I need to move the assert out of that testbench and into a library15: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
litghostmkurc: I recommend tracing with grep15:31
litghostmkurc: Or writing a tool to specifically walk the routing from source to sink15:32
sf-slack<mkurc> @litghost Yes, I was thinking of creating such a tool. I assume that there isn't any.15:33
litghostmkurc: There is something like it, but I would start from scratch and make a small simple one15:33
*** OmniMancer has quit IRC15:33
litghostmkurc: Focus on just doing 1 src to 1 sink15:33
sf-slack<mkurc> @litghost Yep15:35
*** futarisIRCcloud has quit IRC15:36
litghosthackerfoo: I've updated my PR with the tbassert in an include file, so you could use it (or make suggestions for improvements)15:50
hackerfoolitghost: Thanks, I'll look at it.15:52
mithrohackerfoo: I wonder if you need some init values for things there?15:53
hackerfoomithro: In my testbench? It starts with `nrst` low, which should take care of it.15:59
hackerfooI took most of the code out of top.v, and it does the same.16:02
*** OmniMancer has joined #symbiflow16:06
*** OmniMancer has quit IRC16:07
litghostmithro: 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 it16:11
tpbTitle: Enable kokoro on symbiflow-arch-defs by litghost · Pull Request #556 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)16:11
litghosthackerfoo: 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 results16:15
hackerfooOkay. 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
hackerfooNevermind, I see "ifdef" in the code.16:20
litghosthackerfoo: 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 that16:23
litghosthackerfoo: Maybe two testbench's are needed for your purpose16:23
mithrolitghost: We currently run out of io pins if you try and place and route the non-top.v module, right?16:24
litghostmithro: That is one problem, yes16:24
litghostmithro: ROI breakout would help with that16:24
litghostmithro: But in this case running the UART on both sides of the top module is probably a good idea16:25
*** kc8apf has left #symbiflow16:26
mithrolitghost: I think we probably want a test helper with the uart then16:29
litghostmithro: Don't disagree16:29
litghostmithro: The UART module itself can serve that purpose, combined with a deframer/read queue16:30
litghostmithro: I avoided adding a queue to the current FIFO module because eventually we will want to use a BRAM FIFO or something, unclear16:31
litghostcurrent UART module*16:31
mithrolitghost: BTW - Have you seen ZipCPU's blog about formal stuff? https://zipcpu.com/formal/formal.html ?16:32
tpbTitle: The ZipCPU by Gisselquist Technology (at zipcpu.com)16:32
mithroHe has a Makefile for formal proofs with SymbiYosys at -> https://zipcpu.com/zipcpu/2018/12/20/sby-makefile.html16:33
tpbTitle: Makefiles for formal proofs with SymbiYosys (at zipcpu.com)16:33
mithroDunno if that is useful at all...16:33
litghostmithro: I think that is for build up of cumulative proofs16:34
litghostmithro: I think most of our proofs should be single instance16:34
litghostmithro: If we try to prove say, the picosoc, then that will be usefull16:35
mithrolitghost: If the proofs work on the original verilog, they should still work on the verilog from the bitstream, right?16:35
litghostmithro: We haven't been proving the original verilog though16:35
litghostmithro: To date, we've been proving that pre-synthesis is equivilant to post-PnR16:35
litghostmithro: I believe those links are about proving verilog "assume" statements16:36
litghostmithro: Which would be lost through the PnR process16:36
litghostmithro: That being said the documentation (including that blog) on the Yosys proving process is pretty terrible16:36
litghostmithro: The Yosys documentation on $equiv cells is literally a TODO16:37
*** proteusguy has joined #symbiflow16:39
mithrolitghost: You could try poking zipcpu and daveshah in #yosys16:39
litghostmithro: Nah, I think the problem I have is an actual error, either in our PnR or fasm2verilog16:40
litghostmithro: I was stuck for a bit, but the testbench will help prove to myself that the equivilance error is real16:40
mithrolitghost: I think we should poke zipcpu about doing a tutorial about equivalence proving anyway16:40
hackerfoolitghost: Maybe it would be best to just use a single error signal pin for testbenches instead of a full UART.16:41
litghostmithro: If I find that I cannot replicate the equivalence failure in the TB, I'll poke upstream16:41
*** ZipCPU has joined #symbiflow16:41
litghosthackerfoo: Sure, and on hardware just have the pin connect to an LED?  That will work16:41
hackerfooOne reason I want to avoid complexity is to make the FASM easier to analyze.16:42
ZipCPUHello, mithro16:42
mithroZipCPU: we were just chatting about formal equivalence proving16:42
ZipCPUAlright, wow, go on16:42
mithroZipCPU: I was saying that your other formal tutorials / blog posts are pretty good16:43
* ZipCPU is looking through the log for some context16:43
mithroand litghost was complaining "The Yosys documentation on $equiv cells is literally a TODO"16:43
litghostZipCPU: i was say that the equiv documentation in the yosys manual is pretty close to non-existant16:43
ZipCPUThat's pretty close to reality16:43
ZipCPUIt's not an "advertised" feature16:43
litghostlol16:44
ZipCPUI've tried to help coach some folks through it before, but it's always befuddled the both of us16:44
mithroZipCPU: so, was wondering if we could persuade you to look into documentation :-P16:44
ZipCPUSupposedly SymbiYosys can do it, I just haven't been successful at it16:44
litghoste.g. it has the documentation?16:44
ZipCPUWell, back up a bit, what are you trying to do?16:44
ZipCPUWhat type of equivalence checking?16:44
ZipCPUSome types are doable, some not so much16:45
litghostI'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 yet16:46
hackerfooHow many bits? Up to 32 bits of input + state is easy.16:46
litghostRelevant design: https://github.com/litghost/symbiflow-arch-defs/blob/76e136c1b290073b3176e46e763f5386527081f4/xc7/tests/ff_sr_ce/ff_ce_sr.v16:46
tpbTitle: symbiflow-arch-defs/ff_ce_sr.v at 76e136c1b290073b3176e46e763f5386527081f4 · litghost/symbiflow-arch-defs · GitHub (at github.com)16:46
litghostUsing the following yosys script: https://github.com/litghost/symbiflow-arch-defs/blob/76e136c1b290073b3176e46e763f5386527081f4/yosys/equiv_simple_opt_full.ys16:47
ZipCPUThat looks like 16 FFs ;)16:47
tpbTitle: symbiflow-arch-defs/equiv_simple_opt_full.ys at 76e136c1b290073b3176e46e763f5386527081f4 · litghost/symbiflow-arch-defs · GitHub (at github.com)16:47
litghostIndeed, sorry, trying to say 1 FF per input16:47
hackerfooSo, 32 bits then?16:47
litghostWhat is interesting is the led[9] led[10] and led[11] are failing to prove16:48
litghostIf I change the xor reduce to say Q[5:016:48
litghostIt proves16:48
hackerfooCheck all 4 billion cases. Should take a few minutes on hardware.16:48
litghostBut Q[7:0] fails16:48
litghosthackerfoo: The goal is to have a test that runs without hardware16:49
*** alexhw has joined #symbiflow16:49
litghostZipCPU: 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 code16:49
litghostZipCPU: Or simply a case where the equiv check cannot prove the situation16:50
hackerfoolitghost: Oh, well then can you use Verilator?16:50
ZipCPUHeh, yeah, one of the reasons why the equivalency support isn't yet "advertised" ;)16:50
*** bubble_buster has joined #symbiflow16:50
ZipCPUSo, there's a couple of basic types of equivalency checking16:51
ZipCPUOne checks things from the top level inputs and outputs alone.16:51
litghostI'm currently use the equiv cells at top level inputs and outputs16:51
ZipCPUThe second type does a check between FFs16:51
litghostYou are refering to equiv_struct?16:51
litghostfor the second type16:51
ZipCPUIt's the second check, the input->FF, FF->FF, and FF->output that's practically doable for the case you are interested in16:52
litghostYosys was unable to add equiv cells using equiv_struct16:52
litghostI wasn't able to diagnose why that was the case16:52
litghostFYI, I am using latest Yosys master as of yesterday16:53
* ZipCPU is browsing yosys doc's, for anything starting with "equiv"16:53
litghostIt's pretty sparse16:54
* ZipCPU reads the "miter" page ...16:54
litghostZipCPU: miter might make this worse, it only adds the equiv cell for the 1 output yes?16:55
ZipCPUNo, it's much more powerful than that16:55
litghostWhat is the relative utility of equiv_make and miter -equiv?16:55
litghoste.g. why choose one over the other?16:56
ZipCPUSo, 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 bmc16:57
ZipCPUThe miter_src is a file including both example logic files, asserting that their outputs are identical16:57
ZipCPUThe outputs can be concatenated together, and so look for any output differences16:57
litghostfmcombine is not in the yosys documentation, presumably that is not in the open source version?16:59
ZipCPUNo, it's there.  You might find the most up to date yosys documentation by running: yosys -p "help fmcombine"17:00
litghostI guess http://www.clifford.at/yosys/files/yosys_manual.pdf hasn't been updated then17:00
ZipCPUI was looking at http://www.clifford.at/yosys/documentation.html and coming to the same conclusion17:01
tpbTitle: Yosys Open SYnthesis Suite :: Documentation (at www.clifford.at)17:01
litghostZipCPU: If I understand fmcombine, if I have two top-level sources, "miter -equiv" + "fmcombine" will do the job?17:02
ZipCPUIn the example I have, you have three toplevel sources.  The first is your original design.  The second is your modified design.17:03
ZipCPUThe third source is the miter_src file.  The example I have, that I've started to work from, uses a hand-built miter_src file17:03
ZipCPUFor example ....17:04
litghostZipCPU: What I am suggesting is use "miter -equiv" to build the "third source" so to speak17:04
litghostZipCPU: So that it doesn't need to be hand generated17:04
ZipCPUHere's the example of my "third source": https://gist.github.com/ZipCPU/cc707c81baa7b438f38b81608837e91e17:05
tpbTitle: filter_miter.sv · GitHub (at gist.github.com)17:05
ZipCPUI 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
litghostlol17:05
*** OmniMancer has joined #symbiflow17:05
ZipCPUI think it's on the to-do list, I just haven't had the opportunity to learn it yet17:06
litghostWhat you have written in that third source is pretty close to what I believe "miter -equiv" builds17:06
ZipCPUThere was a recent reddit post on this topic though ....17:06
litghostI don't believe random reddit posts makes for good documentation ...17:06
ZipCPUThis is why it isn't an "advertised" feature17:06
ZipCPUCheck https://www.reddit.com/r/yosys  The second item down is on equivalence checking17:07
tpbTitle: Yosys Open SYnthesis Suite (at www.reddit.com)17:07
litghostZipCPU: That example uses equiv_struct, which was unable to find places to add $equiv cells17:08
litghostin my case17:08
ZipCPUDo the two designs have different FF structures?17:09
litghostIn theory no, one is the post-place and route version of the prior17:10
ZipCPUDo they have the same number of FF's?17:11
litghostZipCPU: Yes.  In fact of the led wires, all but 3 prove equivilant17:12
ZipCPUDo you have a trace showing the differences?17:12
litghosttrace?17:13
ZipCPUVCD file?17:13
litghostYou mean a testbench wave file?17:14
ZipCPUI mean a counter-example waveform file produced by the formal tools, such as by SymbiYosys when using the script I just mentiond using fmcombine17:15
litghostZipCPU: I'm not sure how that is done17:15
ZipCPUCan you post a tarball somewhere where I can set see if I can set it up for you?17:16
litghostGimme a minute17:16
litghostFYI, you will need https://github.com/YosysHQ/yosys/pull/92817:17
tpbTitle: Add additional cells sim models for core 7-series primitives. by litghost · Pull Request #928 · YosysHQ/yosys · GitHub (at github.com)17:17
litghostZipCPU: There should be two verilog files, in theory they are the same design https://usercontent.irccloud-cdn.com/file/iHYHJw73/ff_ce_sr_equiv.tgz17:19
*** Bertl is now known as Bertl_oO17:36
ZipCPUHmm ... ERROR: Module \FDRE referenced in mo... is not part of the design ...17:37
litghostYou need to run "read_verilog +/techlibs/cells_sim.v"17:38
litghostYou need to run "read_verilog +/xilinx/cells_sim.v"17:38
litghostThen run a pass to lower from the xilinx tech library to the yosys primatives17:39
ZipCPUNow I think I need your pull update ...17:39
litghostYou do, because I'm using primatives that were missing from cells_sim.v17:39
ZipCPUGot it ... on to the fmcombine step17:42
* ZipCPU steps away, having been called to another task17:50
litghostZipCPU: Okay. If you have any hints, do tell. Otherwise I'll wait till your back17:51
*** OmniMancer has quit IRC18:07
*** adjtm has joined #symbiflow18:19
* litghost mithro: https://github.com/SymbiFlow/prjxray/pull/77319:05
ZipCPUlitghost: The two circuits you gave me are equivalent19:09
litghostZipCPU: That's great!19:09
litghostZipCPU: How did you prove it?19:09
ZipCPUI didn't use equiv at all, and threw out the fmcombine and miter stuff, etc19:09
ZipCPUI just created a design containing both, and then asserted that the outputs would always be identical19:10
ZipCPUWhen running with "abc pdr" as the engine, it was able to prove the two were equivalent19:10
ZipCPUSend me a PM with an e-mail address, and I'll send you a copy of the files I used19:11
litghostThanks, 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 that19:14
ZipCPUOther than the middle file, I think that's what I offered19:31
ZipCPUThe trick, though, is that "abc pdr" works on the simpler designs.  It will struggle with more complex designs19:32
ZipCPUHowever, without some form of a full proof, you might only know that the first N clocks have identical outputs, and nothing about anything beyond that19:32
litghostZipCPU: Thanks, I'll take a look.19:44
litghostZipCPU: What is a sby file?19:54
ZipCPUA SymbiYosys configuration file19:54
litghostIs see the "[engine]" section, does that translate into a yosys script command?19:55
ZipCPUNo19:56
ZipCPUOnly the [script] command translates into a yosys script.  Even at that, it's not a complete script.  SymbiYosys will add more to it19:57
litghostZipCPU: FYI the miter.vs was not required,  the following script is equivilent:20:11
litghostread_verilog +/xilinx/cells_sim.v20:11
litghostread_verilog -sv ff_ce_sr_4.v20:11
litghostrename top gold20:11
litghostread_verilog -sv top_bit.v20:11
litghostrename top gate20:11
litghostmiter -equiv -make_assert gold gate miter20:11
litghostprep -top miter20:11
ZipCPUOk20:11
*** adjtm_ has joined #symbiflow20:27
*** adjtm has quit IRC20:30
litghostZipCPU: 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 #symbiflow21:16
litghostZipCPU: I just noticed a weird behavior in SymbiYosys, might be a bug21:24
ZipCPUReally?  What's that?21:25
litghostZipCPU: I intentionally broke equivilance, and SymbiYosys started to use other engines21:25
litghostZipCPU: In particular ones I did not have installed21:25
ZipCPUOh, dear21:25
litghostFile an issue?21:25
ZipCPUWhat engines did you have installed?21:25
ZipCPU(Probably)21:25
litghostRight now just the ones that Yosys provides21:26
litghostI've make an issue and test case21:26
ZipCPUWhich engine did it try to use?21:26
hackerfoolitghost: 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
ZipCPUasserts are synthesizable?21:27
litghosthackerfoo: Why does it need to be synthesizable?  I guess I don't know what you are trying to do21:27
litghostZipCPU: abc, then yosys-smtbmc (which I have) and then yices-smt2, which I don't21:28
hackerfoolitghost: I'm trying to follow this approach to check where RAM32X1D fails: https://docs.google.com/document/d/11wJUvr2aVBkUiuYYsFN07jkoYr_ccWlLLLFH8YQw8uQ/edit?usp=sharing21:29
litghosthackerfoo: Which step are you on?21:30
litghosthackerfoo: FYI, the issue is almost certainly on Step 5, and step 5 is missing the really check21:31
hackerfooI 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
litghosthackerfoo: Which is compare the bit2fasm output from both VPR and Vivado and check to see if things are different21:32
hackerfooHeh, which step 5? There's two, apparently.21:32
litghostlol21:32
litghosthackerfoo: The second one, post PnR21:33
litghosthackerfoo: I actually think what is written there is incorrect21:33
litghosthackerfoo: 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 features21:33
litghosthackerfoo: 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 behavior21:34
litghosthackerfoo: Step 3/4 is worth checking if you are messing with how yosys generates output, but I wouldn't suspect them at the outset21:35
litghosthackerfoo: Step 1/2 is worth doing to make sure the verilog isn't totally bonkers21:36
hackerfooSo then, can I use the testbench I wrote, or do I need one for top.v?21:36
litghosthackerfoo: I don't recommend a testbench at all for debugging VPR PnR errors when we are testing new primatives21:36
hackerfooI don't have 100% confidence in my verilog yet, either.21:37
litghosthackerfoo: I would do step 2, e.g. make sure when compiled by vivado it works21:37
litghosthackerfoo: And step 1 is good hygien no matter what21:37
litghosthackerfoo: Steps 3/4 are overkill unless you have reason to believe there is a synthesis error, but can always be revisited21:37
hackerfooI believe mithro recommended I remove the UART and error logic to make it easier to analyze the FASM.21:38
litghosthackerfoo: That was a misstep21:38
litghosthackerfoo: Because there is only 1 DRAM, you can filter the FASM down to the CLB that contains the DRAM21:38
mithrohackerfoo / litghost: I was suggesting that it was easier to write a test bench without the UART / error logic initially21:38
litghostmithro: Oh sure, but that is on the testbench side of thing21:39
litghosts21:39
hackerfooOkay, I guess I misunderstood. Still, there wasn't a testbench that dumped to a VCD that I could look at.21:39
litghostmithro / 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 problem21:39
litghostmithro / 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/57021:40
tpbTitle: Add asserts for combintorial output combiner. by litghost · Pull Request #570 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)21:40
litghosthackerfoo: I think no matter what, fixing https://github.com/SymbiFlow/symbiflow-arch-defs/issues/558 is a good idea21:41
litghosthackerfoo: I believe it was working in the past, and helped me to debug a "Step 2" class issue, e.g. the verilog was just wrong21:41
hackerfooIt's worth fixing, but how will it help me? I already have a working testbench.21:43
litghosthackerfoo: Oh it won't, but I don't think a testbench will help either, depending on where the true problem lies21:44
hackerfooMy understanding is that autosim fuzzes the inputs?21:44
litghosthackerfoo: Autosim just provides a clk21:44
litghosthackerfoo: Which in the case of the dram test is enough21:44
litghosthackerfoo: I wrote the DRAM test to be completely automatic, so as long as there is a clock it will run without other input21:45
hackerfooI 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
tpbTitle: RAM32X1D not working · Issue #409 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)21:45
litghosthackerfoo: 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 Vivado21:47
tpbTitle: RAM32X1D not working · Issue #409 · SymbiFlow/symbiflow-arch-defs · GitHub (at github.com)21:47
hackerfooOkay, thanks. I'll try that.21:47
litghosthackerfoo: As part of generating FASM output, you will have a vivado generated bitstream, which you can load and verify that it generates good UART output21:48
litghosthackerfoo: Which resolves the "Step 2" question, e.g. is the verilog remotely correct21:48
mithrobtw 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
hackerfooIs there a documented way to get FASM output from Vivado? I don't think it runs when building *_bin or *_prog.21:48
litghostOne minute21:49
litghosthackerfoo: Vivado doesn't get invoke from symbiflow at all, you'll need a prjxray tree checked out if you don't already have one21:51
litghosthackerfoo: I'm tarring up an example script for running the vivado flow and getting FASM out21:51
hackerfooThanks21:52
litghosthackerfoo: Here ya go https://usercontent.irccloud-cdn.com/file/qSucpnD1/test_dram.tgz21:53
litghosthackerfoo: Once you have prjxray checked out, run the shell script download-latest-db.sh21:53
litghosthackerfoo: And then source database/artix7/settings.sh and then source minitests/roi_harness/basys3-swbut.sh21:54
litghosthackerfoo: That will set up the required environment variables to make everything line up21:54
litghosthackerfoo: And you need to set XRAY_VIVADO_SETTINGS to point to the vivado settings.sh per the prjxray README21:54
litghosthackerfoo: Then run "runme.sh" and it will do the rest21:55
litghosthackerfoo: Just follow the startup steps in the README actually, it's mostly documented in there, minus sourcing minitests/roi_harness/basys3-swbut.sh21:57
hackerfooThanks22:00
litghosthackerfoo: 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 product22:08
litghosthackerfoo: However if you are generating from vivado, "diff" isn't useful because Vivado doesn't respect the way we have setup the ROI22:09
litghosthackerfoo: So greping each files for the relevant 10 or so lines is the right idea22:09
*** gruetzkopf has joined #symbiflow22:10
hackerfooDo you think it would work if I just sort the lines? The order doesn't matter, right?22:12
litghosthackerfoo: Vivado and VPR will choose different CLBs, you'll need to narrow the output22:14
litghosthackerfoo: If you want, you could create a constrain on vivado for the CLB tile, but the difference is usually pretty obvious22:15
hackerfooOkay22:15
mithrolitghost: https://github.com/SymbiFlow/prjxray/issues/77423:46
tpbTitle: 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!