Wednesday, 2018-04-04

*** tpb has joined #yosys00:00
*** ZipCPU|Laptop has joined #yosys00:05
*** svenn has quit IRC00:07
*** svenn has joined #yosys00:07
*** promach__ has joined #yosys00:07
*** ZipCPU|Laptop has quit IRC00:47
*** cemerick has joined #yosys00:56
*** seldridge has quit IRC01:24
*** promach__ has quit IRC01:34
*** xrexeon has quit IRC01:40
*** emeb_mac has joined #yosys01:45
*** ZipCPU|Laptop has joined #yosys02:01
*** ZipCPU|Laptop has quit IRC02:28
*** digshadow has quit IRC02:29
*** jkiv has joined #yosys02:36
*** emeb has quit IRC02:47
*** promach_ has joined #yosys03:01
*** jkiv has quit IRC03:11
*** digshadow has joined #yosys03:32
*** AlexDaniel has quit IRC03:45
*** promach_ has quit IRC04:31
*** X-Scale has quit IRC04:51
*** pie___ has joined #yosys04:52
*** digshadow has quit IRC05:04
*** cemerick has quit IRC05:20
*** philtor has quit IRC05:44
*** philtor has joined #yosys05:44
*** promach_ has joined #yosys06:03
*** emeb_mac has quit IRC06:29
*** sklv has quit IRC06:44
*** GuzTech has joined #yosys06:55
*** pie___ has quit IRC07:00
*** pie_ has joined #yosys07:01
*** digshadow has joined #yosys07:59
*** promach_ has quit IRC09:12
*** promach_ has joined #yosys09:42
*** svenn_ has joined #yosys10:10
*** shapr_ has joined #yosys10:18
*** Max`P has joined #yosys10:18
*** indy_ has joined #yosys10:18
*** svenn has quit IRC10:19
*** indy has quit IRC10:19
*** fouric has quit IRC10:19
*** quigonjinn has quit IRC10:19
*** philtor has quit IRC10:19
*** Max-P has quit IRC10:19
*** shapr has quit IRC10:19
*** Max`P is now known as Max-P10:19
*** philtor has joined #yosys10:21
*** promach_ has quit IRC10:25
*** fouric has joined #yosys10:27
*** leviathan has joined #yosys10:43
*** eduardo_ has joined #yosys11:11
*** eduardo__ has quit IRC11:12
*** indy_ is now known as indy11:25
*** indy has quit IRC11:34
*** indy has joined #yosys11:41
*** proteusguy has quit IRC12:11
*** xrexeon has joined #yosys12:46
*** maartenBE has quit IRC12:47
*** cemerick has joined #yosys12:49
*** maartenBE has joined #yosys12:51
*** leviathan has quit IRC12:58
*** leviathan has joined #yosys12:58
*** cemerick_ has joined #yosys13:41
*** cemerick has quit IRC13:44
*** seldridge has joined #yosys13:47
*** pie_ has quit IRC13:52
cr1901_modernZipCPU: The TLDR to where I'm stuck is basically "verifying a design for a parametric module w/ arbitrary value for the parameter". I don't have time right now to go into detail, but >>13:52
*** pie_ has joined #yosys13:52
cr1901_modernsomeone on birdsite recommended an optimization _I believe is analogous_ to what clifford uses for riscv formal to reduce the state space to check:
cr1901_modern(emphasis on _I believe is analogous_. When I have more time I could come up with a minimal example and corresponding visual aid lol.)13:54
ZipCPUcr1901_modern: I haven't gotten there yet, but I do know Clifford's solution which I intend to apply soon.14:00
ZipCPUClifford's solution is based around "task"s within SymbiYosys.14:00
ZipCPUYou can create a SymbiYosys file that sets parameters to a particular solution, and then split that file further into "tasks"--each of which sets the parameter values to a different value.14:01
ZipCPUI've also used a different approach for my multiply: I've created an abstract multiply that returns a result in 1-8 clocks.  (My true multiply returns a result in 1, 2, 3, or 4 clocks--never changing)14:02
ZipCPUBy using this abstract multiply, I can prove that *all* of the parameter based multiplies will work.14:02
ZipCPU(Incidentally, the result of the abstract multiply is ... random--part of the abstraction)14:02
* cr1901_modern is trying to remember how to code verilog... please stand by14:04
cr1901_modernZipCPU: Ack, I'll have to read into that later, but here's my contrived example:
cr1901_modernThis is a crappy verilog counter that outputs a signal when the counter overflows14:08
cr1901_modern(there is a missing ov <= 0 under the rst block)14:08
ZipCPUI like { ov, cnt } <= cnt + 1; for that, but ... okay14:09
cr1901_modernOh that works? TIL14:09
ZipCPUSo ... what would you like to prove?14:10
ZipCPUassert(ov == (cnt == 0)); ?14:10
cr1901_modern"assuming rst=1 initially, ov eventually becomes 1"14:10
ZipCPUThat'd be a fun assertion, and you'd find some failures in your code as well.14:10
ZipCPUTo prove that "ov eventually becomes 1", use a cover statement and cover(ov);14:11
cr1901_modernThen I want to prove for arbitrary width14:11
ZipCPUHmm, that means we'd need to change the assert as well, how about: assert(($past(i_reset)(||(ov == (cnt == 0))); ?14:11
cr1901_moderndoesn't take much brain power for me to realize "no matter what the width", ov => 114:12
cr1901_modern"ov will eventually => 1"*14:12
cr1901_modernHow do I prove that14:12
cr1901_modernwhat is prefix-||?14:12
ZipCPUTo prove "ov will eventually => 1", use cover(ov);14:13
ZipCPUOh, sorry, there is no "prefix-||" ... just a typo on my part while trying to maintain a property you weren't interested in proving.14:13
cr1901_modernBut I want to do that for arbitrary width. I.e. "the parameter width is allowed to vary."14:13
cr1901_modern(I may have screwed up the Verilog. I almost never write it anymore.)14:14
ZipCPUSuppose you make width an arbitrary constant instead?14:14
ZipCPUAnd then allow your internal width to be 32 or some maximum value?14:14
ZipCPUThen, you can adjust your logic so that: always @(posedge i_clk) if (i_reset) ov <= 0; else if (&cnt[width-1:0]) ov <= 1;14:15
ZipCPUTo prove "ov" is eventually set, cover(ov);14:16
ZipCPUThe next question, though, is how do you do this for a 32-bit width without taking 2^32 steps?  That's where abstraction comes into play.14:16
*** cemerick has joined #yosys14:16
cr1901_modernWhat do you mean by "internal width"?14:17
cr1901_modernversus an "arbitrary constant"14:17
ZipCPUArbitrary constant: wire [5:0] width = $anyconst;14:18
ZipCPUThat's also what I mean by "internal width"14:18
ZipCPUThis is slightly different from: parameter width = 4;14:18
ZipCPUI suppose you might do: `ifdef FORMAL\n wire [4:0] width = $anyconst;\n`else\nparameter width = 4;\n`endif14:19
*** cemerick_ has quit IRC14:19
cr1901_modernOkay, so I forgot about $anyconst. Also I didn't know this was possible:14:19
cr1901_modernwire [5:0] width = $anyconst; wire [width-1:0] my_wire;14:20
cr1901_modernI thought you could only do that with, well, parameters14:20
ZipCPUNo, it's not possible.  Let me clarify:14:22
ZipCPUwire [5:0] width = $anyconst; wire [63:0] my_wire;  // is possible however.14:22
ZipCPUThen, you can choose to only pay attention to the lower width bits of my_wire.14:22
* cr1901_modern is thinking14:25
cr1901_modernI'm guessing cover can't be used w/ induction14:25
ZipCPUSigh.  No, it cannot.14:25
ZipCPUHowever, you could do the assertion: "assert(!|my_wire[63:width] || ov);"14:26
ZipCPUThat'd pass induction nicely.14:26
cr1901_modern>Then, you can choose to only pay attention to the lower width bits of my_wire.14:27
cr1901_modernDid you mean higher width bits?14:27
cr1901_modernB/c that's what that assert does afaik- only considers the higher width bits14:27
ZipCPUNo, I meant lower bits when I said it, the higher bits idea was only a more recent one.14:28
cr1901_modernZipCPU: Oh sorry, I can't do OR to save my life14:30
cr1901_modern!| == "if any of the bits are 1, the whole expression is 0"?14:30
ZipCPUThat's what I meant, yes.14:31
ZipCPUI haven't actually tried that expression through a Verilog parser to know that it works though ....14:31
cr1901_modernOkay, this approach assumes you've put an upper limit to the counter width you want to check. What I had intended to check for in my counter example w/ the parameter was:14:32
cr1901_modernNo upper limit. Prove for finite-"n"14:32
ZipCPUYeah ... I'm not sure how to do that.14:32
cr1901_moderncounter could be 1 bit, 64 bits, 1024 bits, 65536 bits14:32
ZipCPUFor a fixed counter, it's easy.14:33
cr1901_modernWe both know that no matter how big the counter is, it will eventually overflow for all finite values of parameter "width"14:33
ZipCPUYeah, but the proof for 65536 bits isn't trivial.  :P14:33
cr1901_modernI simply wonder if there is a way to express this without e.g. actually having to check the 65536 bit proof14:34
ZipCPUAt this point in our discussion, I do not know of a way.  I know of a way to check counters of width 1-N, for fixed N, but not 1-infinity.14:34
cr1901_modernZipCPU: Well, I need some time to think before we continue (I understand the convo isn't done- you were about to discuss abstractions). Is that okay?14:35
ZipCPUWell, okay, sure, let's move on to abstractions then.14:35
ZipCPUThe idea behind abstractions is that if you can prove "A -> B", then it must also be true that "(AC) -> B"14:36
ZipCPUI would need to use abstractions to cover your 65536 bit case, otherwise cover (which must start at init, as currently written) would never get there.14:36
ZipCPUTo do that, we make an abstract counter instead, and then step by an amount chosen by the formal solver subject to your constraints.14:37
ZipCPUThe abstract counter doesn't step by one, in other words, but it might step by one.14:37
ZipCPUHence, the case that you are interested in is one of many cases described by the abstraction.14:37
ZipCPUIf the formal properties you choose still succeed, then you know they will succeed even if the counter only steps by one.14:38
*** seldridge has quit IRC14:38
ZipCPUHence, if "(counter monotonically increases) -> B" is true, then so also must be if "(counter increments by one) -> B"14:39
ZipCPUOn the other hand, it might be true that "(counter monotonically increases)" doesn't imply B, but "(counter increments by one)" does.14:40
ZipCPUIn other words, if "A -> B" is false, it might still be true that "(AC)->B".  So failing to prove "A -> B" (the abstract version) doesn't really tell you that "(AC)-> B" will fail to prove as well.14:41
*** cemerick_ has joined #yosys14:41
* cr1901_modern is plugging "(A -> B) -> ((AC) -> B)" into z314:42
cr1901_modern Yup, "(A -> B) -> ((AC) -> B)" is true, cool14:45
*** cemerick has quit IRC14:46
cr1901_modernso (counter monotonically increases) is "A" in your example and (counter increments by one), being more specific is "(AC)" in your example?14:46
*** proteusguy has joined #yosys14:47
*** AlexDaniel has joined #yosys14:47
cr1901_modernThis is really weird (and profound), and messing w/ my head14:49
*** shapr_ is now known as shapr14:50
*** shapr has joined #yosys14:50
ZipCPUWould you like me to share an example that I'm currently using?14:51
cr1901_modernNot right now, I would prefer to struggle/sit on this some more if that's okay :)14:52
*** cr1901_modern has quit IRC14:52
*** cemerick_ has quit IRC14:53
ZipCPUOk, I'll post it to my dev branch of the ZipCPU then if anyone else requests it.14:53
*** cr1901_modern has joined #yosys14:53
*** cemerick_ has joined #yosys14:54
*** promach__ has joined #yosys14:54
cr1901_modernIt seems like to take advantage of "(A -> B) -> ((AC) -> B)", you not only have to prove "A" holds, but also that "AC" holds14:55
*** quigonjinn has joined #yosys14:56
cr1901_modernZipCPU: I have to go right, now. Would you be willing to paste a link to your example?14:56
ZipCPUExactly.  However, I think the formalism is getting to you.  My formal proof is going the other way.14:57
ZipCPUOk, sure, I'll paste the link ... one moment ....14:57
cr1901_modern(Well I assume proving "A -> C" is enough to show that "AC" holds)14:59
ZipCPUAhh, sorry about my criticism starting with "Exactly.  However, ..." ... looking over it again, I think you got it right.15:00
* ZipCPU is reminded never to do (predicate) math in public ...15:00
cr1901_modernNo worries, I didn't even notice what you meant the first readthru :P15:01
cr1901_modernThe reason I bring that up is because you could choose a "C" that has no relation to the truth value of "A" whatsoever and make "(A -> B) -> ((AC) -> B)" hold.15:01
cr1901_modernBut choosing a "C" that's not derived from "A" is useless for the proof I want to do15:01
ZipCPUNot quite.  In the example I gave of (counter is monotincally increasing), (counter increments by one) was not derived from "A"15:02
cr1901_modern(Perhapos I meant you need to show C -> A15:03
ZipCPUOk, that makes sense.15:03
ZipCPUI like to think of C as a subset of A, but in predicate math C -> A might be just as equivalent.15:03
cr1901_moderne.g. A = (counter is monotincally increasing) and C = (true) satisfies "(A -> B) -> ((AC) -> B)"15:03
cr1901_modernerr, crap15:04
cr1901_modernI'm gonna stop while I'm ahead and think more15:04
cr1901_modernignore the last few msgs15:04
* ZipCPU just posted his abstract multiply at
cr1901_moderntyvm, I'll take a look when I have more time :)15:05
* cr1901_modern splits for a bit15:05
cr1901_modernthanks for the help as always15:06
awygleI never thought of using $anyconst like that! Great idea15:23
*** maartenBE has quit IRC15:25
*** seldridge has joined #yosys15:26
*** maartenBE has joined #yosys15:29
*** seldridge has quit IRC15:30
*** maartenBE has quit IRC15:51
*** maartenBE has joined #yosys15:55
keesjdo you guys also use gtkwave for looking at change value dumps or are you using..somethine else?16:16
ZipCPUI personally use gtkwave all over the place.16:17
*** GuzTech has quit IRC16:21
awygleI use gtkwave but I'm sad about it16:22
*** cemerick_ is now known as cemerick16:22
*** promach__ has quit IRC16:32
*** emeb has joined #yosys16:40
*** AlexDani` has joined #yosys16:44
*** AlexDaniel has quit IRC16:44
*** cr1901_modern1 has joined #yosys16:47
*** cr1901_modern has quit IRC16:49
*** cr1901_modern1 has quit IRC16:50
*** cr1901_modern has joined #yosys16:52
*** digshadow has quit IRC17:02
*** sklv has joined #yosys17:03
*** seldridge has joined #yosys17:08
*** digshadow has joined #yosys17:25
*** GuzTech has joined #yosys17:31
*** seldridge has quit IRC17:33
*** cemerick_ has joined #yosys17:34
*** cemerick has quit IRC17:38
keesjawygle: why?17:39
keesjI have some asserts in my test code (and quite happy about it) but do use gtkwave to view stuff. There are small things I would like changed (and like sigrok's puslveview ) would like logic analysers17:41
keesj(but sigrok/pulseview currently are not ... 100% ready for handling many singals)17:42
keesjand ... just out of curiosity... what do you use when it does not work on the "real" hardware?17:45
kc8apfI use when I'm on a Mac17:52
tpbTitle: Scansion (at
awyglekeesj: it's not well integrated on windows, the UI is unintuitive, and it doesn't support real time streaming afaict17:56
awygleon real hardware I currently use vendor tools, but hope to develop a suite of tools along the lines of what ZipCPU discussed on his blog in the future17:56
*** seldridge has joined #yosys17:57
ravenexpwhat's wrong with good old procedural testbenches?17:59
ravenexpit's been quite a while since I've last stared on the marching waves18:00
keesjI have only limited experience but on the papilio pro I used sump / ols (e.g. only  32 channels and 200Mhz ) but did get the job done) but it did not feel a professional as some vendor tools18:04
awygleI am astonished that no one has yet implemented a live debugger for FPGAs18:04
tpbTitle: Papilio FPGA Platform (at
ravenexpdoes chipscope count as a live debugger?18:05
ravenexpnot to speak of the soft cpu trace ports18:05
keesjravenexp: what do you mean by procedural testbenches?18:05
awygleravenexp: can you single step the clock? Can you modify the HDL on the fly?18:05
awygle(no and no)18:05
ravenexpI can't thing of why it would be a good idea to single step an fpga18:06
keesjI mean: testing works fine .. but ... what do you do when it does not18:06
ravenexpkeesj: I stop and think about my tests18:06
ravenexpthen I fix them and it works both in tests and on the live hw18:06
awygleGranted something like that is more often useful in a simulator but it doesn't exist even there18:07
awygleI want to step through my state machines and figure out why the valid signal is getting asserted one cycle before the data is actually valid18:07
*** cemerick has joined #yosys18:07
ravenexpyou can do that in like 10 lines of verilog18:08
awygleBut every time I bring this up I get the same "just be perfect" response, so... *shrug*18:08
ravenexpand one you've written this test, it stays there18:08
ravenexpso you won't ever regress on it18:08
awygleyou can verify correctness in 10 lines, but determining the cause of incorrectness is still done with very blunt tools18:09
ravenexpmany small module-level tests are way better at catching logic errors than whole system debuggers could ever be18:09
awygleFPGA debugging sucks primarily because of how comically long the feedback loops are18:09
awyglewhy not both?18:10
ravenexppls, some people do asics18:10
keesjwell. I think I have written decent tests and (this is my first real project) and I felt happy about it. I even had some kind of confidence. building up tests and seeing it pass was awesome. using gtkwave was only a basic ..  visualisation but I needed real... failing? tests18:10
awygleI imagine Asic debugging sucks worse. Doesn't mean fpga debugging doesn't suck.18:10
*** cemerick_ has quit IRC18:10
ravenexpcomplaining about fpga loopback cycles is somehat...18:10
keesjbut I feel there is still a distance between that and .. the real thing18:11
ravenexpkeesj: I use verilog models for things both inside and outside the fpga18:11
keesjbecause of bad simulation?18:11
ravenexpyou can do board level debugging before you can even get your hands on the real hw18:12
ravenexpwhen I was an fpga noob I used chipscope and real logic analyzers a lot18:13
ravenexpnowadays I mostly do "make ; make program" and things just work...18:13
* keesj did use a real logic analyzer today18:14
ravenexpyou can't do CI with people with logic analyzers18:15
ravenexpwith good test suites you actually can18:15
*** GuzTech_ has joined #yosys18:33
*** GuzTech has quit IRC18:35
*** jkiv has joined #yosys18:38
*** seldridge has quit IRC18:39
*** GuzTech_ has quit IRC18:43
*** GuzTech_ has joined #yosys18:43
*** seldridge has joined #yosys18:59
*** dys has joined #yosys19:17
*** GuzTech__ has joined #yosys19:21
*** GuzTech_ has quit IRC19:24
keesjare there travis/github type hosted CI projects I might want to look into ?19:26
keesj(example stuff)19:26
ZipCPUWhat sort of stuff are you looking for?19:27
*** cemerick_ has joined #yosys19:31
*** cemerick has quit IRC19:35
ZipCPUawygle: I've single stepped my FPGA designs before.19:39
ZipCPUIt's not all that hard to do, but you do need to plan to be able to do so from the beginning.19:40
ZipCPUFurther, I think a lot of ASIC engineers single-step their designs once the ASIC comes back from the fab--usually they have a logic chain of some type (can't remember the name off the top of my head) that allows them to see everything and then step everything.19:41
keesjZipCPU: I don't really know what I am looking for sorry, I guess information on how others deal with this type of issues and good examples19:42
keesj(but ... I won't start doing it today so mostly out of interest)19:43
ZipCPUI have a lot of example designs at feel free to browse and then come back with questions if you would like.19:43
tpbTitle: ZipCPU (Dan Gisselquist) ยท GitHub (at
sorearthose are called scan chains, and they are primarily used to test the chip as manufactured against the netlist, not for finding new problems in the netlist19:44
ZipCPUAhh ... that's the word I was looking for.  Thank you, sorear!  Thank you for the clarification as well.19:44
awygleZipCPU: yes, it doesn't seem difficult, but it's very uncommon. and even when it is done, the surrounding tooling doesn't support it well (most vcd renderers won't do live update for example)19:46
ZipCPUThat makes sense.  When I did it last, I used a WB bus to read the internal state back off of the device, and then dumped the data into a file I could read and process using Octave.19:48
ZipCPUIt worked really well when stepping through signal processing algorithms19:48
ZipCPUIndeed, I never used any simulation on that project at all--it was all HITL testing.19:48
*** Kensan has joined #yosys20:07
*** milkii has joined #yosys20:25
*** jkiv has quit IRC20:56
*** cemerick_ is now known as cemerick21:01
*** jkiv has joined #yosys21:19
*** leviathan has quit IRC21:58
*** GuzTech__ has quit IRC22:23
*** cemerick_ has joined #yosys22:45
*** cemerick has quit IRC22:49
*** AlexDani` is now known as AlexDaniel23:15
*** dys has quit IRC23:19
*** jkiv has quit IRC23:49
*** digshadow has quit IRC23:52
*** digshadow has joined #yosys23:53
*** seldridge has quit IRC23:58

Generated by 2.13.1 by Marius Gedminas - find it at!