| *** tpb has joined #yosys | 00:00 | |
| *** m_w has joined #yosys | 00:02 | |
| *** m_w has quit IRC | 00:09 | |
| *** promach_ has joined #yosys | 00:44 | |
| *** AlexDani` has joined #yosys | 01:00 | |
| *** AlexDaniel has quit IRC | 01:02 | |
| *** AlexDani` has quit IRC | 01:05 | |
| *** AlexDani` has joined #yosys | 01:12 | |
| *** AlexDani` is now known as AlexDaniel | 01:14 | |
| *** emeb_mac has joined #yosys | 01:15 | |
| *** promach_ has quit IRC | 01:24 | |
| *** mobius has joined #yosys | 02:26 | |
| *** emeb has quit IRC | 02:34 | |
| *** proteus-guy has quit IRC | 03:16 | |
| *** seldridge has quit IRC | 03:48 | |
| *** X-Scale has quit IRC | 05:31 | |
| *** dxld has quit IRC | 05:51 | |
| *** dxld has joined #yosys | 05:52 | |
| *** xerpi has joined #yosys | 06:20 | |
| *** xerpi has quit IRC | 06:21 | |
| *** xerpi has joined #yosys | 06:21 | |
| *** leviathan has joined #yosys | 06:24 | |
| *** leviathan has quit IRC | 06:26 | |
| *** leviathan has joined #yosys | 06:26 | |
| *** kraiskil has joined #yosys | 06:32 | |
| *** pointfree1 has quit IRC | 06:43 | |
| *** maartenBE has quit IRC | 06:44 | |
| *** MatrixTraveler[m has quit IRC | 06:44 | |
| *** maartenBE has joined #yosys | 06:45 | |
| *** pointfree1 has joined #yosys | 06:49 | |
| *** MatrixTraveler[m has joined #yosys | 06:54 | |
| *** kraiskil has quit IRC | 07:03 | |
| *** kraiskil has joined #yosys | 07:07 | |
| *** emeb_mac has quit IRC | 07:08 | |
| *** kraiskil has quit IRC | 07:15 | |
| *** GuzTech has joined #yosys | 07:40 | |
| *** proteus-guy has joined #yosys | 07:54 | |
| *** fsasm has joined #yosys | 09:32 | |
| *** luismarques has joined #yosys | 09:39 | |
| *** proteus-guy has quit IRC | 09:58 | |
| *** jwhitmore has joined #yosys | 10:02 | |
| *** proteus-guy has joined #yosys | 10:24 | |
| *** proteus-guy has quit IRC | 10:26 | |
| *** proteus-guy has joined #yosys | 10:27 | |
| *** luismarques has quit IRC | 10:51 | |
| *** luismarques has joined #yosys | 10:53 | |
| *** luismarques has joined #yosys | 11:16 | |
| *** pie__ has joined #yosys | 11:37 | |
| *** pie_ has quit IRC | 11:41 | |
| *** luismarques has quit IRC | 11:48 | |
| *** X-Scale has joined #yosys | 11:54 | |
| *** xerpi has quit IRC | 11:57 | |
| *** kraiskil has joined #yosys | 12:22 | |
| *** nurelin has quit IRC | 13:14 | |
| *** luismarques has joined #yosys | 13:14 | |
| *** nurelin has joined #yosys | 13:22 | |
| *** luismarques has quit IRC | 13:43 | |
| *** luismarques has joined #yosys | 13:45 | |
| *** promach_ has joined #yosys | 13:45 | |
| *** nurelin has quit IRC | 13:47 | |
| *** luismarques has quit IRC | 14:00 | |
| *** nurelin has joined #yosys | 14:00 | |
| *** kraiskil has quit IRC | 14:15 | |
| *** seldridge has joined #yosys | 14:16 | |
| *** cr1901_modern has quit IRC | 14:16 | |
| *** luismarques has joined #yosys | 14:29 | |
| *** jwhitmore has quit IRC | 15:03 | |
| *** jwhitmore has joined #yosys | 15:03 | |
| *** seldridge has quit IRC | 15:06 | |
| *** maikmerten has joined #yosys | 15:37 | |
| *** GuzTech has quit IRC | 15:48 | |
| *** jwhitmore has quit IRC | 15:52 | |
| *** zkrx has quit IRC | 15:57 | |
| maikmerten | turns 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 |
|---|---|---|
| maikmerten | https://pasteboard.co/Hs0jOP1.png | 16:02 |
| tpb | Title: Pasteboard Uploaded Image (at pasteboard.co) | 16:02 |
| 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 look | 16:04 | |
| maikmerten | :-) | 16:05 |
| ZipCPU|Laptop | I've never used that part of the Verilog language, sorry. | 16:05 |
| ZipCPU|Laptop | I have a rule which is to use only clocks within @(*edge) blocks (sometimes asynchronous resets too). This violates my rule. :) | 16:06 |
| maikmerten | thanks for having a look :) | 16:06 |
| maikmerten | the complete testbench, btw: https://github.com/maikmerten/spu32/blob/master/cpu/tests/bus_wb8_tb.v | 16:10 |
| tpb | Title: spu32/bus_wb8_tb.v at master · maikmerten/spu32 · GitHub (at github.com) | 16:10 |
| ZipCPU|Laptop | Ever tried formal verification? | 16:11 |
| maikmerten | this 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 read | 16:11 |
| * ZipCPU|Laptop is working on formally verifying an FFT right now | 16:11 | |
| maikmerten | no, sadly no formal verification :-( | 16:12 |
| ZipCPU|Laptop | Why not? | 16:12 |
| ZipCPU|Laptop | I formally verify all of my bus components. | 16:12 |
| ZipCPU|Laptop | The tools are free, and you find more bugs than with traditional test benches. | 16:12 |
| maikmerten | I guess a misguided lazyness on my part has for now prevented me looking into how to specify the constraints that formal verification check for | 16:13 |
| ZipCPU|Laptop | That part is already done and posted. You are using a wishbone interface, right? | 16:14 |
| maikmerten | yes, I'm using a silly perversion of Wishbone | 16:14 |
| maikmerten | (8 bit data bus, but 32 bit address... c'mon...) | 16:15 |
| ZipCPU|Laptop | Here's an article that discusses how to describe wishbone using formal properties: http://zipcpu.com/zipcpu/2017/11/07/wb-formal.html | 16:15 |
| tpb | Title: Building Formal Assumptions to Describe Wishbone Behaviour (at zipcpu.com) | 16:15 |
| ZipCPU|Laptop | You can find other formal related articles at: https://zipcpu.com/formal/formal.html | 16:15 |
| tpb | Title: The ZipCPU by Gisselquist Technology (at zipcpu.com) | 16:15 |
| maikmerten | ZipCPU|Laptop, hey, cool, I've seen your site before. It actually triggered my move from Wishbone classic to pipelined operation | 16:16 |
| ZipCPU|Laptop | ;) | 16:18 |
| maikmerten | I 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 specify | 16:21 |
| maikmerten | my testbench basically aims at gaining some confidence that the bus unit actually returns correct data | 16:23 |
| ZipCPU|Laptop | What is the unit under test? | 16:23 |
| maikmerten | of course, formal methods should be helpful here as well | 16:23 |
| awygle | well, it works fine in the fpga because this code isn't synthesizable lol | 16:24 |
| maikmerten | a 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 present | 16:24 |
| srk | ZipCPU|Laptop: that's pretty cool! | 16:25 |
| awygle | so whatever issue you have is a simulation issue | 16:25 |
| maikmerten | awygle, indeed | 16:25 |
| ZipCPU|Laptop | I 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 component | 16:25 |
| maikmerten | awygle, 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|Laptop | For example, three specific properties will constrain the proper functioning of any cache. | 16:26 |
| awygle | maikmerten: 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 |
| maikmerten | and 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 check | 16:26 |
| awygle | what are you using for simulation? | 16:26 |
| maikmerten | (okay, that last sentence was completely broken) | 16:26 |
| maikmerten | iverilog | 16:27 |
| awygle | yeah, i think you want this to be a continuous check, so it probably wants to be always@(posedge clk) | 16:28 |
| awygle | or similar | 16:28 |
| awygle | but this is a pretty infrequently used corner of the language (at least by people around here). maybe try ##fpga? | 16:29 |
| maikmerten | thanks for your input! | 16:29 |
| maikmerten | I guess that the non-synthesizable part of Verilog indeed is out-of-scope for this particular corner of freenode ;-) | 16:30 |
| awygle | formal is always fun though! and ZipCPU|Laptop swears it's useful :p | 16:31 |
| ZipCPU|Laptop | LP | 16:31 |
| ZipCPU|Laptop | :P | 16:31 |
| maikmerten | oh, I'm pretty sure formal is very useful in a lot of cases! | 16:32 |
| ZipCPU|Laptop | Especially bus interactions ... | 16:32 |
| maikmerten | Clifford likes formal verification as well, explaining the SAT-solver in yosys ;-) | 16:32 |
| * ZipCPU|Laptop uses Yosys for all of his formal verification work | 16:32 | |
| awygle | yes of course, i'm just giving ZipCPU a hard time | 16:33 |
| * awygle hopes to get back to his formal work... someday | 16:33 | |
| maikmerten | yeah - 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|Laptop | Defn: 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. ;D | 16:33 |
| maikmerten | don't tell Intel or AMD ;-) | 16:34 |
| awygle | i'm currently looking at C code that locks a mutex, then immediately unlocks it, _then_ modifies a shared resource. lots of horrible things "work" :p | 16:34 |
| maikmerten | yummy. | 16:34 |
| * ZipCPU|Laptop will pray for awygle | 16:34 | |
| awygle | it's cool, my solution to this is permitted to be "rm -f" | 16:35 |
| ZipCPU|Laptop | Looks 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 |
| awygle | nice! | 16:38 |
| awygle | somehow i feel like i could go backwards in the log and find you expressing doubt about the possibility of such a thing somewhere | 16:39 |
| ZipCPU|Laptop | I 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 |
| awygle | have you done any experimenting with the more "advanced" (for lack of a better term) formal algorithms? beyond k-induction i mean | 16:41 |
| ZipCPU|Laptop | I've done a bunch of stuff with cover, although not with the liveness methods. | 16:41 |
| ZipCPU|Laptop | I've also used the concurrent assertions available in the commercial yosys version. | 16:41 |
| awygle | those are all very cool | 16:42 |
| awygle | but what i meant was things like "abc pdr" | 16:42 |
| ZipCPU|Laptop | I have used abc pdr. | 16:43 |
| ZipCPU|Laptop | The first proof of the entire ZipCPU was using abc pdr. | 16:43 |
| awygle | also the "aiger" solvers (avy and suprove, maybe others?) | 16:43 |
| ZipCPU|Laptop | Yes, I've tried several of those as well. | 16:43 |
| awygle | i find these particularly interesting as they seem to be more powerful, or at least differently powerful, than straightforward k-induction | 16:44 |
| ZipCPU|Laptop | My 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 |
| awygle | c.f. your induction article | 16:44 |
| awygle | and, being a lazy sort, i am interested in anything that involves less fiddling around :p | 16:45 |
| ZipCPU|Laptop | Well ... you could be like Clifford and avoid induction entirely. | 16:46 |
| awygle | oh? what approach does clifford take? | 16:47 |
| ZipCPU|Laptop | He uses bmc almost exclusively. He and I seem to be quite different from that standpoint. | 16:48 |
| ZipCPU|Laptop | For me, it isn't a proof unless k-induction passes. | 16:48 |
| ZipCPU|Laptop | Although, mathematically, it is possible to prove a design with only BMC | 16:48 |
| awygle | hm. how? wouldn't you have to get into a provably repeating state? | 16:49 |
| aiju | 17:25 < maikmerten> I guess that the non-synthesizable part of Verilog indeed is out-of-scope for this particular corner of freenode ;-) | 16:49 |
| awygle | or i guess exhaust the state space | 16:49 |
| ZipCPU|Laptop | Heheh ... 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 |
| aiju | i know this! | 16:50 |
| maikmerten | oh :) | 16:50 |
| ZipCPU|Laptop | awygle: All designs get into repeating states. At issue is how many states it takes to get there. | 16:50 |
| awygle | ZipCPU|Laptop: sure, but you have to prove that | 16:50 |
| aiju | maikmerten: it's a race condition | 16:51 |
| maikmerten | ewww | 16:51 |
| maikmerten | I hate those! | 16:51 |
| ZipCPU|Laptop | awygle: Not at all. Someone else did. | 16:51 |
| aiju | maikmerten: '=' in clocked logic is bad news | 16:51 |
| awygle | ZipCPU|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 design | 16:52 |
| awygle | also isn't this equivalent to solving the halting problem? lol | 16:52 |
| aiju | maikmerten: each initial/always block is a process; @(posedge clk) just means "wait until the clock rises" | 16:52 |
| ZipCPU|Laptop | Ahh, 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 |
| aiju | maikmerten: '=' is an assgnment that updates the value immediately | 16:52 |
| aiju | so ti depends which two procsses run first :) | 16:53 |
| aiju | *which of the processes runs | 16:53 |
| awygle | ah. interesting. | 16:53 |
| aiju | oversimplifying a bit, <= assignments are delayed until the current timestep is over | 16:53 |
| awygle | i can see how that would be a nice simple brute-force way to do it | 16:53 |
| aiju | 17:47 < awygle> also isn't this equivalent to solving the halting problem? lol | 16:54 |
| awygle | $1 = yosys -how_deep_is_my_state_graph; bmc $1 | 16:54 |
| aiju | only for things that are turing complete :) | 16:54 |
| aiju | verilog designs have a finite state space | 16:54 |
| awygle | i suppose that's true. they're not rewriteable. | 16:54 |
| ZipCPU|Laptop | Especially 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 |
| awygle | until/unless we get a self-partially-reconfiguring FPGA :p | 16:55 |
| srk | ZipCPU|Laptop: what's your workflow like? | 16:55 |
| ZipCPU|Laptop | srk: How do you mean? | 16:55 |
| srk | I would like to learn more about formal verif. but the learning curve is steeeep | 16:55 |
| ZipCPU|Laptop | It's not that bad, but go on. | 16:55 |
| * ZipCPU|Laptop does teach a course on the topic. | 16:55 | |
| *** seldridge has joined #yosys | 16:56 | |
| srk | ZipCPU|Laptop: well, when you work on a block what tools do you use for verification? | 16:56 |
| ZipCPU|Laptop | Ok, 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 |
| aiju | i 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 on | 16:57 |
| ZipCPU|Laptop | Understand ... 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|Laptop | Designing 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 |
| srk | I'm half-way thru, using ivory/tower and haskell to generate "better" C code for stm32s | 16:59 |
| maikmerten | aiju, 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 busy | 17:00 |
| ZipCPU|Laptop | Ok, 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 |
| aiju | maikmerten: are you sure it's not running at time 0? | 17:01 |
| aiju | maikmerten: you could try adding a $display("%T"); to print the current time before the dataout check | 17:01 |
| maikmerten | oooooooooooh | 17:01 |
| maikmerten | that sounds plausible | 17:01 |
| aiju | maikmerten: x->0 is a negedge | 17:01 |
| aiju | maikmerten: @(negedge clk) will trigger on initial clk = 1'b0; | 17:02 |
| aiju | depending on the scheduling | 17:02 |
| awygle | oo that's a good point, yeah | 17:02 |
| srk | ZipCPU|Laptop: thanks, this is pretty cool as well http://zipcpu.com/zipcpu/2018/01/31/cpu-build.html | 17:06 |
| tpb | Title: ZipCPU toolchain and initial test (at zipcpu.com) | 17:06 |
| ZipCPU|Laptop | srk: 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 |
| srk | are the course materials available possibly? :D | 17:07 |
| ZipCPU|Laptop | Every now and then I'll tweet a slide. | 17:07 |
| ZipCPU|Laptop | You might want to browse through the zipcpu.com/formal/formal.html posts. There's a lot of commonality between those and the courseware. | 17:08 |
| srk | thanks for these | 17:08 |
| ZipCPU|Laptop | My 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 |
| srk | I'm out of uni for some years now so I'm ok with learning stuff by myself :) | 17:10 |
| srk | doable when you have good foundations and extremely rewarding as you learn stuff which you actually need / want | 17:11 |
| ZipCPU|Laptop | I'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 |
| srk | :D | 17:11 |
| srk | this! | 17:11 |
| *** promach_ has quit IRC | 17:33 | |
| *** cr1901_modern has joined #yosys | 17:45 | |
| *** cr1901_modern1 has joined #yosys | 17:49 | |
| *** cr1901_modern has quit IRC | 17:50 | |
| *** cr1901_modern1 has quit IRC | 17:51 | |
| *** cr1901_modern has joined #yosys | 17:51 | |
| shapr | anyone jumped on board with the NeTV2 for yosys purposes? | 17:56 |
| shapr | bunnie huang product using a risc-v softcore: https://www.crowdsupply.com/alphamax/netv2 | 17:56 |
| tpb | Title: NeTV2 | Crowd Supply (at www.crowdsupply.com) | 17:56 |
| shapr | not sure if bunnie is using yosys to build the softcore for that Xilinx chip | 17:56 |
| *** maikmerten has quit IRC | 18:24 | |
| *** fsasm has quit IRC | 18:38 | |
| *** Ristovski has quit IRC | 19:14 | |
| *** [Ristovski] has joined #yosys | 19:17 | |
| *** m_w has joined #yosys | 19:19 | |
| *** sklv has joined #yosys | 19:23 | |
| *** [X-Scale] has joined #yosys | 20:11 | |
| *** X-Scale has quit IRC | 20:13 | |
| *** [X-Scale] is now known as X-Scale | 20:13 | |
| *** jhol has quit IRC | 20:43 | |
| *** jhol has joined #yosys | 20:56 | |
| *** seldridge has quit IRC | 21:01 | |
| *** leviathan has quit IRC | 21:17 | |
| *** sklv has quit IRC | 21:39 | |
| *** kristian1aul has joined #yosys | 21:39 | |
| *** sklv has joined #yosys | 21:41 | |
| *** kristianpaul has quit IRC | 21:42 | |
| *** m_w has quit IRC | 21:59 | |
| *** ZipCPU|Laptop has quit IRC | 22:37 | |
| *** m_w has joined #yosys | 23:52 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!
