Thursday, 2018-06-28

*** tpb has joined #yosys00:00
*** m_w has joined #yosys00:02
*** m_w has quit IRC00:09
*** promach_ has joined #yosys00:44
*** AlexDani` has joined #yosys01:00
*** AlexDaniel has quit IRC01:02
*** AlexDani` has quit IRC01:05
*** AlexDani` has joined #yosys01:12
*** AlexDani` is now known as AlexDaniel01:14
*** emeb_mac has joined #yosys01:15
*** promach_ has quit IRC01:24
*** mobius has joined #yosys02:26
*** emeb has quit IRC02:34
*** proteus-guy has quit IRC03:16
*** seldridge has quit IRC03:48
*** X-Scale has quit IRC05:31
*** dxld has quit IRC05:51
*** dxld has joined #yosys05:52
*** xerpi has joined #yosys06:20
*** xerpi has quit IRC06:21
*** xerpi has joined #yosys06:21
*** leviathan has joined #yosys06:24
*** leviathan has quit IRC06:26
*** leviathan has joined #yosys06:26
*** kraiskil has joined #yosys06:32
*** pointfree1 has quit IRC06:43
*** maartenBE has quit IRC06:44
*** MatrixTraveler[m has quit IRC06:44
*** maartenBE has joined #yosys06:45
*** pointfree1 has joined #yosys06:49
*** MatrixTraveler[m has joined #yosys06:54
*** kraiskil has quit IRC07:03
*** kraiskil has joined #yosys07:07
*** emeb_mac has quit IRC07:08
*** kraiskil has quit IRC07:15
*** GuzTech has joined #yosys07:40
*** proteus-guy has joined #yosys07:54
*** fsasm has joined #yosys09:32
*** luismarques has joined #yosys09:39
*** proteus-guy has quit IRC09:58
*** jwhitmore has joined #yosys10:02
*** proteus-guy has joined #yosys10:24
*** proteus-guy has quit IRC10:26
*** proteus-guy has joined #yosys10:27
*** luismarques has quit IRC10:51
*** luismarques has joined #yosys10:53
*** luismarques has joined #yosys11:16
*** pie__ has joined #yosys11:37
*** pie_ has quit IRC11:41
*** luismarques has quit IRC11:48
*** X-Scale has joined #yosys11:54
*** xerpi has quit IRC11:57
*** kraiskil has joined #yosys12:22
*** nurelin has quit IRC13:14
*** luismarques has joined #yosys13:14
*** nurelin has joined #yosys13:22
*** luismarques has quit IRC13:43
*** luismarques has joined #yosys13:45
*** promach_ has joined #yosys13:45
*** nurelin has quit IRC13:47
*** luismarques has quit IRC14:00
*** nurelin has joined #yosys14:00
*** kraiskil has quit IRC14:15
*** seldridge has joined #yosys14:16
*** cr1901_modern has quit IRC14:16
*** luismarques has joined #yosys14:29
*** jwhitmore has quit IRC15:03
*** jwhitmore has joined #yosys15:03
*** seldridge has quit IRC15:06
*** maikmerten has joined #yosys15:37
*** GuzTech has quit IRC15:48
*** jwhitmore has quit IRC15:52
*** zkrx has quit IRC15:57
maikmertenturns out I don't have a firm grasp of Verilog yet. A seemingly trivial testbench of mine gives very unexpected simulation results (simulation done in iverilog), although the synthesis result works just fine on a FPGA.16:02
tpbTitle: Pasteboard Uploaded Image (at
maikmerten(okay, the testbench "misbehaving" is obviously not in itself contradicting that the module under test exhibits the proper behaviour)16:03
* ZipCPU|Laptop takes a look16:04
ZipCPU|LaptopI've never used that part of the Verilog language, sorry.16:05
ZipCPU|LaptopI have a rule which is to use only clocks within @(*edge) blocks (sometimes asynchronous resets too).  This violates my rule.  :)16:06
maikmertenthanks for having a look :)16:06
maikmertenthe complete testbench, btw:
tpbTitle: spu32/bus_wb8_tb.v at master · maikmerten/spu32 · GitHub (at
ZipCPU|LaptopEver tried formal verification?16:11
maikmertenthis is putting some predetermined input into the bus unit of my CPU design, waits until the bus unit finished operation (busy-signal goes low) and checks, if the proper values were read16:11
* ZipCPU|Laptop is working on formally verifying an FFT right now16:11
maikmertenno, sadly no formal verification :-(16:12
ZipCPU|LaptopWhy not?16:12
ZipCPU|LaptopI formally verify all of my bus components.16:12
ZipCPU|LaptopThe tools are free, and you find more bugs than with traditional test benches.16:12
maikmertenI guess a misguided lazyness on my part has for now prevented me looking into how to specify the constraints that formal verification check for16:13
ZipCPU|LaptopThat part is already done and posted.  You are using a wishbone interface, right?16:14
maikmertenyes, I'm using a silly perversion of Wishbone16:14
maikmerten(8 bit data bus, but 32 bit address... c'mon...)16:15
ZipCPU|LaptopHere's an article that discusses how to describe wishbone using formal properties:
tpbTitle: Building Formal Assumptions to Describe Wishbone Behaviour (at
ZipCPU|LaptopYou can find other formal related articles at:
tpbTitle: The ZipCPU by Gisselquist Technology (at
maikmertenZipCPU|Laptop, hey, cool, I've seen your site before. It actually triggered my move from Wishbone classic to pipelined operation16:16
maikmertenI may be misunderstanding that article, though: It seems you're checking that the bus cycle itself is progressing as specified (e.g., that the bus components behave properly and that the bus, e.g., doesn't get stuck) - which is of course all that the Wishbone specification can specify16:21
maikmertenmy testbench basically aims at gaining some confidence that the bus unit actually returns correct data16:23
ZipCPU|LaptopWhat is the unit under test?16:23
maikmertenof course, formal methods should be helpful here as well16:23
awyglewell, it works fine in the fpga because this code isn't synthesizable lol16:24
maikmertena bus unit, which on the "CPU side" is connected to the testbench (where I apply stimuli) - while on the "bus side" a 1KB RAM simulation with predetermined content is present16:24
srkZipCPU|Laptop: that's pretty cool!16:25
awygleso whatever issue you have is a simulation issue16:25
maikmertenawygle, indeed16:25
ZipCPU|LaptopI ask because ... 1) I have several examples of formal properties and wishbone slave components, and 2) the value returned may be constrained by properties appropriate to the component16:25
maikmertenawygle, the waveform of the module under test in simulation actually matches what I want - it's just that the testbench checks the module's output at the "wrong time"16:26
ZipCPU|LaptopFor example, three specific properties will constrain the proper functioning of any cache.16:26
awyglemaikmerten: i think it's because you can't delay like this in initial blocks, you have to do it in an always block. i could be wrong though.16:26
maikmertenand I just can't figure out why the check in the testbench doesn't wait for the busy signal to go low before doing the check16:26
awyglewhat are you using for simulation?16:26
maikmerten(okay, that last sentence was completely broken)16:26
awygleyeah, i think you want this to be a continuous check, so it probably wants to be [email protected](posedge clk)16:28
awygleor similar16:28
awyglebut this is a pretty infrequently used corner of the language (at least by people around here). maybe try ##fpga?16:29
maikmertenthanks for your input!16:29
maikmertenI guess that the non-synthesizable part of Verilog indeed is out-of-scope for this particular corner of freenode ;-)16:30
awygleformal is always fun though! and ZipCPU|Laptop swears it's useful :p16:31
maikmertenoh, I'm pretty sure formal is very useful in a lot of cases!16:32
ZipCPU|LaptopEspecially bus interactions ...16:32
maikmertenClifford likes formal verification as well, explaining the SAT-solver in yosys ;-)16:32
* ZipCPU|Laptop uses Yosys for all of his formal verification work16:32
awygleyes of course, i'm just giving ZipCPU a hard time16:33
* awygle hopes to get back to his formal work... someday16:33
maikmertenyeah - bus interactions should be a wonderful target - because there usually are very neat specifications to check against ;-)16:33
* awygle passes around a hat labeled "pay me to do formal work"16:33
ZipCPU|LaptopDefn: formal shame, verb, to apply formal methods to someone else's design and prove that the design they thought was working still had many bugs within it.  ;D16:33
maikmertendon't tell Intel or AMD ;-)16:34
awyglei'm currently looking at C code that locks a mutex, then immediately unlocks it, _then_ modifies a shared resource. lots of horrible things "work" :p16:34
* ZipCPU|Laptop will pray for awygle16:34
awygleit's cool, my solution to this is permitted to be "rm -f"16:35
ZipCPU|LaptopLooks like I'll be able to formally verify a second stage of an FFT ... I already managed to prove the penultimate stage, this would be the last stage.  (Neither require hardware accelerated multiplies)16:38
awyglesomehow i feel like i could go backwards in the log and find you expressing doubt about the possibility of such a thing somewhere16:39
ZipCPU|LaptopI have doubt about the possibility of proving the general butterfly, and I have doubt about proving the entire thing together, but at this point ... this works so far.16:40
awyglehave you done any experimenting with the more "advanced" (for lack of a better term) formal algorithms? beyond k-induction i mean16:41
ZipCPU|LaptopI've done a bunch of stuff with cover, although not with the liveness methods.16:41
ZipCPU|LaptopI've also used the concurrent assertions available in the commercial yosys version.16:41
awyglethose are all very cool16:42
awyglebut what i meant was things like "abc pdr"16:42
ZipCPU|LaptopI have used abc pdr.16:43
ZipCPU|LaptopThe first proof of the entire ZipCPU was using abc pdr.16:43
awyglealso the "aiger" solvers (avy and suprove, maybe others?)16:43
ZipCPU|LaptopYes, I've tried several of those as well.16:43
awyglei find these particularly interesting as they seem to be more powerful, or at least differently powerful, than straightforward k-induction16:44
ZipCPU|LaptopMy favorites are yices and boolector still.  While I like abc pdr, if my design would fail then it never returns.  On the other hand, if the design would succeed ... often abc pdr returns faster than other solvers.16:44
awyglec.f. your induction article16:44
awygleand, being a lazy sort, i am interested in anything that involves less fiddling around :p16:45
ZipCPU|LaptopWell ... you could be like Clifford and avoid induction entirely.16:46
awygleoh? what approach does clifford take?16:47
ZipCPU|LaptopHe uses bmc almost exclusively.  He and I seem to be quite different from that standpoint.16:48
ZipCPU|LaptopFor me, it isn't a proof unless k-induction passes.16:48
ZipCPU|LaptopAlthough, mathematically, it is possible to  prove a design with only BMC16:48
awyglehm. how? wouldn't you have to get into a provably repeating state?16:49
aiju17:25 < maikmerten> I guess that the non-synthesizable part of Verilog indeed is out-of-scope for this particular corner of freenode ;-)16:49
awygleor i guess exhaust the state space16:49
ZipCPU|LaptopHeheh ... Just tried "abc pdr" on the module I'm working on and it instantly passed.  I'll still need to do more to get yices or boolector to pass.16:49
aijui know this!16:50
maikmertenoh :)16:50
ZipCPU|Laptopawygle: All designs get into repeating states.  At issue is how many states it takes to get there.16:50
awygleZipCPU|Laptop: sure, but you have to prove that16:50
aijumaikmerten: it's a race condition16:51
maikmertenI hate those!16:51
ZipCPU|Laptopawygle: Not at all.  Someone else did.16:51
aijumaikmerten: '=' in clocked logic is bad news16:51
awygleZipCPU|Laptop: you don't have to prove that all designs repeat, you have to prove that you've reached a repeating state of your particular design16:52
awyglealso isn't this equivalent to solving the halting problem? lol16:52
aijumaikmerten: each initial/always block is a process; @(posedge clk) just means "wait until the clock rises"16:52
ZipCPU|LaptopAhh, no the paper had a different approach for that.  They had a means of determining the maximum depth for any given problem.  Apply BMC to that depth, and then you are guaranteed to be done.16:52
aijumaikmerten: '=' is an assgnment that updates the value immediately16:52
aijuso ti depends which two procsses run first :)16:53
aiju*which of the processes runs16:53
awygleah. interesting.16:53
aijuoversimplifying a bit, <= assignments are delayed until the current timestep is over16:53
awyglei can see how that would be a nice simple brute-force way to do it16:53
aiju17:47 < awygle> also isn't this equivalent to solving the halting problem? lol16:54
awygle$1 = yosys -how_deep_is_my_state_graph; bmc $116:54
aijuonly for things that are turing complete :)16:54
aijuverilog designs have a finite state space16:54
awyglei suppose that's true. they're not rewriteable.16:54
ZipCPU|LaptopEspecially for riscv-formal, where Clifford has been verifying multiple CPU's.  He doesn't have the ability to dive into each individually and create enough properties to ensure they each pass induction.16:55
awygleuntil/unless we get a self-partially-reconfiguring FPGA :p16:55
srkZipCPU|Laptop: what's your workflow like?16:55
ZipCPU|Laptopsrk: How do you mean?16:55
srkI would like to learn more about formal verif. but the learning curve is steeeep16:55
ZipCPU|LaptopIt's not that bad, but go on.16:55
* ZipCPU|Laptop does teach a course on the topic.16:55
*** seldridge has joined #yosys16:56
srkZipCPU|Laptop: well, when you work on a block what tools do you use for verification?16:56
ZipCPU|LaptopOk, sure ... I'm working on a block of an FFT right now.  I'm editing my design in GVIM, saving it, running SymbiYosys, and then examining the trace in gtkwave.16:57
aijui bought a book on formal verification and it taught you how to use secret intel tools that you will never be able to get your hands on16:57
ZipCPU|LaptopUnderstand ... I came to formal after doing a lot of test bench work.  When I found a bug in my first "working" design, I went around to see if I had bugs in others.  Invariably, the answer was always "yes" I had bugs in them that I hadn't found.16:58
ZipCPU|LaptopDesigning with formal methods is, IMHO, much easier than the alternative test bench method--you can go faster and be more sure of yourself along the way.16:58
srkI'm half-way thru, using ivory/tower and haskell to generate "better" C code for stm32s16:59
maikmertenaiju, I'm still at a loss of what happens there, though. To me it still appears that the check should take place after a negative edge of busy17:00
ZipCPU|LaptopOk, the 2-point stage of the FFT now passes formal ... ;)17:00
ZipCPU|Laptop(The 4-point stage and the bit reverse already pass)17:00
aijumaikmerten: are you sure it's not running at time 0?17:01
aijumaikmerten: you could try adding a $display("%T"); to print the current time before the dataout check17:01
maikmertenthat sounds plausible17:01
aijumaikmerten: x->0 is a negedge17:01
aijumaikmerten: @(negedge clk) will trigger on initial clk = 1'b0;17:02
aijudepending on the scheduling17:02
awygleoo that's a good point, yeah17:02
srkZipCPU|Laptop: thanks, this is pretty cool as well
tpbTitle: ZipCPU toolchain and initial test (at
ZipCPU|Laptopsrk: Hopefully I'll have the formally verified build up and ready soon.  I'm pretty close, although I just now got distracted by this FFT.17:07
srkare the course materials available possibly? :D17:07
ZipCPU|LaptopEvery now and then I'll tweet a slide.17:07
ZipCPU|LaptopYou might want to browse through the posts.  There's a lot of commonality between those and the courseware.17:08
srkthanks for these17:08
ZipCPU|LaptopMy expectation is that the courseware will eventually be released publicly.  Feedback from the students said that they wouldn't have understood the course from the slides alone though.17:09
ZipCPU|Laptop(I was hands on, over the shoulders of the students, quite often during the exercises--just to make sure they succeeded.)17:09
srkI'm out of uni for some years now so I'm ok with learning stuff by myself :)17:10
srkdoable when you have good foundations and extremely rewarding as you learn stuff which you actually need / want17:11
ZipCPU|LaptopI've been out for ... 15 yrs now?  Welcome to where learning is actually fun, and where you can learn what you want to learn.17:11
*** promach_ has quit IRC17:33
*** cr1901_modern has joined #yosys17:45
*** cr1901_modern1 has joined #yosys17:49
*** cr1901_modern has quit IRC17:50
*** cr1901_modern1 has quit IRC17:51
*** cr1901_modern has joined #yosys17:51
shapranyone jumped on board with the NeTV2 for yosys purposes?17:56
shaprbunnie huang product using a risc-v softcore:
tpbTitle: NeTV2 | Crowd Supply (at
shaprnot sure if bunnie is using yosys to build the softcore for that Xilinx chip17:56
*** maikmerten has quit IRC18:24
*** fsasm has quit IRC18:38
*** Ristovski has quit IRC19:14
*** [Ristovski] has joined #yosys19:17
*** m_w has joined #yosys19:19
*** sklv has joined #yosys19:23
*** [X-Scale] has joined #yosys20:11
*** X-Scale has quit IRC20:13
*** [X-Scale] is now known as X-Scale20:13
*** jhol has quit IRC20:43
*** jhol has joined #yosys20:56
*** seldridge has quit IRC21:01
*** leviathan has quit IRC21:17
*** sklv has quit IRC21:39
*** kristian1aul has joined #yosys21:39
*** sklv has joined #yosys21:41
*** kristianpaul has quit IRC21:42
*** m_w has quit IRC21:59
*** ZipCPU|Laptop has quit IRC22:37
*** m_w has joined #yosys23:52

Generated by 2.13.1 by Marius Gedminas - find it at!