| *** tpb has joined #yosys | 00:00 | |
| *** proteusguy has quit IRC | 01:01 | |
| *** PyroPeter has quit IRC | 02:22 | |
| *** PyroPeter has joined #yosys | 02:35 | |
| *** citypw has joined #yosys | 02:59 | |
| *** rohitksingh_work has joined #yosys | 04:31 | |
| *** emeb_mac has joined #yosys | 05:03 | |
| *** proteusguy has joined #yosys | 06:12 | |
| *** jakobwenzel has joined #yosys | 07:27 | |
| *** dys has joined #yosys | 07:40 | |
| *** emeb_mac has quit IRC | 07:46 | |
| *** GoldRin has quit IRC | 08:05 | |
| *** GoldRin has joined #yosys | 08:17 | |
| pepijndevos | Oh no... are there any 25 series flash models that work with yosys? | 08:49 |
|---|---|---|
| daveshah | Unlikely, I would guess most 25 series flash models are full of non-synthesisable constructs | 08:56 |
| pepijndevos | basically read_verilog chokes on random weirdness and verific says ERROR: code/N25Qxxx.v:3712: memory size is larger than 2**23 bits | 08:57 |
| daveshah | Yes, that sounds likely. I wouldn't be surprised if Yosys gets stuck if the memory is implemented in a way that doesn't map to a sensible synthesisable memory, as it will convert the memory into loads of latches/registers in this case. | 08:58 |
| pepijndevos | daveshah, I don't care to actually synthesize them, but I want to use them in my formal verification testbenches | 08:58 |
| daveshah | Formal verification ≈ synthesis | 08:59 |
| pepijndevos | Hrm, so I can only make testbenches with actual flash using say ickarus | 09:00 |
| daveshah | Yes | 09:00 |
| pepijndevos | But I remember ZipCPU talking about formal verification with an sdram model... I think | 09:01 |
| daveshah | Yes, that was a custom made model | 09:01 |
| pepijndevos | well shit... okay... hrmmmmm, I guess I'll do a "classical" testbench for this first | 09:04 |
| daveshah | I am sure ZipCPU can explain this better once he is awake. But usually you will find | 09:06 |
| daveshah | custom written assertions/assumptions for an interface more helpful | 09:06 |
| pepijndevos | Right, I suppose you could "assume" the flash chip is there, but your formal proof is only as good as your assumptions, and assuming a whole flash chip... seems like it could use some testing with a hopefully more or less correct verilog model | 09:08 |
| daveshah | With a decent simulator (probably not Icarus) assertions and assumptions work in simulation too | 09:09 |
| daveshah | ZipCPU has definitely formally verified SPI flash controllers in the past | 09:09 |
| pepijndevos | What's a decent simulator then? | 09:09 |
| daveshah | Verilator | 09:10 |
| pepijndevos | Eh, what makes it better? | 09:12 |
| daveshah | Much faster and more SystemVerilog support (incl. assertions/assumptions). But at the expense of not supporting the full Verilog event model (so might not handle a vendor SPI flash model too :/) | 09:13 |
| pepijndevos | lol, if the goal is to run SPI flash models, that seems like a bad trade-off. But I should look at how assume works in sv. | 09:15 |
| daveshah | In a simulator, assumptions and assertions are considered the same | 09:16 |
| daveshah | This allows you to check your assumptions are correct | 09:16 |
| daveshah | In FV, assumptions limit the state space, as the solver won't consider anything that violates an assumption | 09:16 |
| pepijndevos | Ah ok | 09:22 |
| pepijndevos | I have no idea how to use this, but it seems interesting https://github.com/ZipCPU/zbasic/blob/master/sim/verilated/flashsim.h | 09:23 |
| tpb | Title: zbasic/flashsim.h at master · ZipCPU/zbasic · GitHub (at github.com) | 09:23 |
| daveshah | restrict has the same behaviour as an assumption in FV, but is ignored in simulation, for where you deliberately want to limit the state space beyond what the design is capable of | 09:23 |
| daveshah | That's a flash sim model for Verilator | 09:24 |
| *** SpaceCoaster has quit IRC | 09:31 | |
| *** jryans has quit IRC | 09:31 | |
| *** fevv8[m] has quit IRC | 09:31 | |
| *** nrossi has quit IRC | 09:32 | |
| *** fevv8[m] has joined #yosys | 09:43 | |
| ZipCPU | pepijndevos daveshah: You guys are up early this morning | 10:15 |
| daveshah | Not really, that conversation was around 10am UK time for me | 10:15 |
| ZipCPU | pepijndevos: When formally verifying anything with memory, verify a single address | 10:15 |
| ZipCPU | ;) | 10:15 |
| ZipCPU | Leave the address arbitrary using anyconst. You'll then know that if the design works for the single address, it will work for all addresses | 10:16 |
| ZipCPU | As for the flashsim component, ... I'm maintaining the one at https://github.com/ZipCPU/qspiflash/blob/master/bench/cpp/flashsim.* regularly. The other copies get updated to that one more sporadically | 10:17 |
| ZipCPU | pipijndevos: I've never used the "official" simulation models, choosing instead to verify things myself. | 10:19 |
| *** nrossi has joined #yosys | 10:28 | |
| *** jryans has joined #yosys | 10:28 | |
| pepijndevos | ZipCPU, so how do your formally verify one of these flash things? You just make your own model from scratch? | 10:42 |
| ZipCPU | Yes, I make my own model from scratch | 10:43 |
| pepijndevos | hrm, and then hope your model is more or less correct hehe | 10:44 |
| ZipCPU | Have you seen my article on building (and Verifying) a "Universal" Quad-SPI flash controller? | 10:44 |
| ZipCPU | It's a bit long, but goes through the design (and proof) in a lot of detail | 10:44 |
| pepijndevos | Eh... I think the one thing I saw about flash on you site was about verilator | 10:44 |
| ZipCPU | http://zipcpu.com/blog/2019/03/27/qflexpress.html | 10:45 |
| tpb | Title: Building a universal QSPI flash controller (at zipcpu.com) | 10:45 |
| pepijndevos | Will do some reading... or actually, maybe I'll do that on the train later. | 10:45 |
| ZipCPU | The controller optimizes reads from the flash, but also provides the capability to erase/program/or do whatever other capability the flash might have/offer | 10:46 |
| *** citypw has quit IRC | 10:46 | |
| pepijndevos | haha, do you ever *not* write "a bit long" articles? | 10:52 |
| ZipCPU | They're not usually *this* long | 10:54 |
| ZipCPU | The length I struggle for is usually about a quarter of the length of that QSPI article | 10:55 |
| pepijndevos | alright, time to pack and head for the bus. I'll have a read later | 10:55 |
| ZipCPU | The problem with the QSPI controller was that in order to make it "Universal" I had to keep adding more and more requirements to it | 10:55 |
| ZipCPU | Enjoy! | 10:55 |
| *** rohitksingh_work has quit IRC | 11:30 | |
| *** rohitksingh_work has joined #yosys | 11:32 | |
| *** lutsabound has joined #yosys | 12:23 | |
| *** rrika has quit IRC | 12:35 | |
| *** rrika has joined #yosys | 12:37 | |
| *** rohitksingh_work has quit IRC | 13:20 | |
| *** tlwoerner has quit IRC | 13:51 | |
| *** gmc has quit IRC | 14:23 | |
| *** gmc has joined #yosys | 14:25 | |
| *** emeb has joined #yosys | 14:37 | |
| GenTooMan | hmmm does Yosys use a verilog preprocessor? | 14:49 |
| daveshah | GenTooMan: yes, it has one built in | 14:53 |
| daveshah | https://github.com/YosysHQ/yosys/blob/master/frontends/verilog/preproc.cc | 14:53 |
| tpb | Title: yosys/preproc.cc at master · YosysHQ/yosys · GitHub (at github.com) | 14:53 |
| GenTooMan | daveshah Thanks, that is a relief, it claims verilog 2005 compliance so I should be OK with the macros I am writing | 15:07 |
| *** lutsabound has quit IRC | 15:32 | |
| *** dys has quit IRC | 17:12 | |
| *** dys has joined #yosys | 19:20 | |
| *** GenTooMan has quit IRC | 19:36 | |
| *** GenTooMan has joined #yosys | 19:36 | |
| *** emeb_mac has joined #yosys | 21:04 | |
| *** Strobokopp has joined #yosys | 21:34 | |
| *** dys has quit IRC | 22:08 | |
| *** dys has joined #yosys | 22:29 | |
| *** emeb has left #yosys | 23:56 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!