Monday, 2019-07-29

*** tpb has joined #yosys00:00
*** proteusguy has quit IRC01:01
*** PyroPeter has quit IRC02:22
*** PyroPeter has joined #yosys02:35
*** citypw has joined #yosys02:59
*** rohitksingh_work has joined #yosys04:31
*** emeb_mac has joined #yosys05:03
*** proteusguy has joined #yosys06:12
*** jakobwenzel has joined #yosys07:27
*** dys has joined #yosys07:40
*** emeb_mac has quit IRC07:46
*** GoldRin has quit IRC08:05
*** GoldRin has joined #yosys08:17
pepijndevosOh no... are there any 25 series flash models that work with yosys?08:49
daveshahUnlikely, I would guess most 25 series flash models are full of non-synthesisable constructs08:56
pepijndevosbasically read_verilog chokes on random weirdness and verific says ERROR: code/N25Qxxx.v:3712: memory size is larger than 2**23 bits08:57
daveshahYes, 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
pepijndevosdaveshah, I don't care to actually synthesize them, but I want to use them in my formal verification testbenches08:58
daveshahFormal verification ≈ synthesis08:59
pepijndevosHrm, so I can only make testbenches with actual flash using say ickarus09:00
pepijndevosBut I remember ZipCPU talking about formal verification with an sdram model... I think09:01
daveshahYes, that was a custom made model09:01
pepijndevoswell shit... okay... hrmmmmm, I guess I'll do a "classical" testbench for this first09:04
daveshahI am sure ZipCPU can explain this better once he is awake. But usually you will find09:06
daveshahcustom written assertions/assumptions for an interface more helpful09:06
pepijndevosRight, 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 model09:08
daveshahWith a decent simulator (probably not Icarus) assertions and assumptions work in simulation too09:09
daveshahZipCPU has definitely formally verified SPI flash controllers in the past09:09
pepijndevosWhat's a decent simulator then?09:09
pepijndevosEh, what makes it better?09:12
daveshahMuch 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
pepijndevoslol, 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
daveshahIn a simulator, assumptions and assertions are considered the same09:16
daveshahThis allows you to check your assumptions are correct09:16
daveshahIn FV, assumptions limit the state space, as the solver won't consider anything that violates an assumption09:16
pepijndevosAh ok09:22
pepijndevosI have no idea how to use this, but it seems interesting
tpbTitle: zbasic/flashsim.h at master · ZipCPU/zbasic · GitHub (at
daveshahrestrict 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 of09:23
daveshahThat's a flash sim model for Verilator09:24
*** SpaceCoaster has quit IRC09:31
*** jryans has quit IRC09:31
*** fevv8[m] has quit IRC09:31
*** nrossi has quit IRC09:32
*** fevv8[m] has joined #yosys09:43
ZipCPUpepijndevos daveshah: You guys are up early this morning10:15
daveshahNot really, that conversation was around 10am UK time for me10:15
ZipCPUpepijndevos: When formally verifying anything with memory, verify a single address10:15
ZipCPULeave the address arbitrary using anyconst.  You'll then know that if the design works for the single address, it will work for all addresses10:16
ZipCPUAs for the flashsim component, ... I'm maintaining the one at* regularly.  The other copies get updated to that one more sporadically10:17
ZipCPUpipijndevos: I've never used the "official" simulation models, choosing instead to verify things myself.10:19
*** nrossi has joined #yosys10:28
*** jryans has joined #yosys10:28
pepijndevosZipCPU, so how do your formally verify one of these flash things? You just make your own model from scratch?10:42
ZipCPUYes, I make my own model from scratch10:43
pepijndevoshrm, and then hope your model is more or less correct hehe10:44
ZipCPUHave you seen my article on building (and Verifying) a "Universal" Quad-SPI flash controller?10:44
ZipCPUIt's a bit long, but goes through the design (and proof) in a lot of detail10:44
pepijndevosEh... I think the one thing I saw about flash on you site was about verilator10:44
tpbTitle: Building a universal QSPI flash controller (at
pepijndevosWill do some reading... or actually, maybe I'll do that on the train later.10:45
ZipCPUThe controller optimizes reads from the flash, but also provides the capability to erase/program/or do whatever other capability the flash might have/offer10:46
*** citypw has quit IRC10:46
pepijndevoshaha, do you ever *not* write "a bit long" articles?10:52
ZipCPUThey're not usually *this* long10:54
ZipCPUThe length I struggle for is usually about a quarter of the length of that QSPI article10:55
pepijndevosalright, time to pack and head for the bus. I'll have a read later10:55
ZipCPUThe problem with the QSPI controller was that in order to make it "Universal" I had to keep adding more and more requirements to it10:55
*** rohitksingh_work has quit IRC11:30
*** rohitksingh_work has joined #yosys11:32
*** lutsabound has joined #yosys12:23
*** rrika has quit IRC12:35
*** rrika has joined #yosys12:37
*** rohitksingh_work has quit IRC13:20
*** tlwoerner has quit IRC13:51
*** gmc has quit IRC14:23
*** gmc has joined #yosys14:25
*** emeb has joined #yosys14:37
GenTooManhmmm does Yosys use a verilog preprocessor?14:49
daveshahGenTooMan: yes, it has one built in14:53
tpbTitle: yosys/ at master · YosysHQ/yosys · GitHub (at
GenTooMandaveshah Thanks, that is a relief, it claims verilog 2005 compliance so I should be OK with the macros I am writing15:07
*** lutsabound has quit IRC15:32
*** dys has quit IRC17:12
*** dys has joined #yosys19:20
*** GenTooMan has quit IRC19:36
*** GenTooMan has joined #yosys19:36
*** emeb_mac has joined #yosys21:04
*** Strobokopp has joined #yosys21:34
*** dys has quit IRC22:08
*** dys has joined #yosys22:29
*** emeb has left #yosys23:56

Generated by 2.13.1 by Marius Gedminas - find it at!