clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
proteusguy has quit [Ping timeout: 272 seconds]
PyroPeter has quit [Ping timeout: 276 seconds]
PyroPeter has joined #yosys
citypw has joined #yosys
rohitksingh_work has joined #yosys
emeb_mac has joined #yosys
proteusguy has joined #yosys
jakobwenzel has joined #yosys
dys has joined #yosys
emeb_mac has quit [Ping timeout: 258 seconds]
GoldRin has quit [Ping timeout: 268 seconds]
GoldRin has joined #yosys
<pepijndevos> Oh no... are there any 25 series flash models that work with yosys?
<daveshah> Unlikely, I would guess most 25 series flash models are full of non-synthesisable constructs
<pepijndevos> basically read_verilog chokes on random weirdness and verific says ERROR: code/N25Qxxx.v:3712: memory size is larger than 2**23 bits
<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.
<pepijndevos> daveshah, I don't care to actually synthesize them, but I want to use them in my formal verification testbenches
<daveshah> Formal verification ≈ synthesis
<pepijndevos> Hrm, so I can only make testbenches with actual flash using say ickarus
<daveshah> Yes
<pepijndevos> But I remember ZipCPU talking about formal verification with an sdram model... I think
<daveshah> Yes, that was a custom made model
<pepijndevos> well shit... okay... hrmmmmm, I guess I'll do a "classical" testbench for this first
<daveshah> I am sure ZipCPU can explain this better once he is awake. But usually you will find
<daveshah> custom written assertions/assumptions for an interface more helpful
<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
<daveshah> With a decent simulator (probably not Icarus) assertions and assumptions work in simulation too
<daveshah> ZipCPU has definitely formally verified SPI flash controllers in the past
<pepijndevos> What's a decent simulator then?
<daveshah> Verilator
<pepijndevos> Eh, what makes it better?
<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 :/)
<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.
<daveshah> In a simulator, assumptions and assertions are considered the same
<daveshah> This allows you to check your assumptions are correct
<daveshah> In FV, assumptions limit the state space, as the solver won't consider anything that violates an assumption
<pepijndevos> Ah ok
<pepijndevos> I have no idea how to use this, but it seems interesting https://github.com/ZipCPU/zbasic/blob/master/sim/verilated/flashsim.h
<tpb> Title: zbasic/flashsim.h at master · ZipCPU/zbasic · GitHub (at github.com)
<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
<daveshah> That's a flash sim model for Verilator
SpaceCoaster has quit [Ping timeout: 244 seconds]
fevv8[m] has quit [Remote host closed the connection]
jryans has quit [Remote host closed the connection]
nrossi has quit [Remote host closed the connection]
fevv8[m] has joined #yosys
<ZipCPU> pepijndevos daveshah: You guys are up early this morning
<daveshah> Not really, that conversation was around 10am UK time for me
<ZipCPU> pepijndevos: When formally verifying anything with memory, verify a single address
<ZipCPU> ;)
<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
<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
<ZipCPU> pipijndevos: I've never used the "official" simulation models, choosing instead to verify things myself.
nrossi has joined #yosys
jryans has joined #yosys
<pepijndevos> ZipCPU, so how do your formally verify one of these flash things? You just make your own model from scratch?
<ZipCPU> Yes, I make my own model from scratch
<pepijndevos> hrm, and then hope your model is more or less correct hehe
<ZipCPU> Have you seen my article on building (and Verifying) a "Universal" Quad-SPI flash controller?
<ZipCPU> It's a bit long, but goes through the design (and proof) in a lot of detail
<pepijndevos> Eh... I think the one thing I saw about flash on you site was about verilator
<tpb> Title: Building a universal QSPI flash controller (at zipcpu.com)
<pepijndevos> Will do some reading... or actually, maybe I'll do that on the train later.
<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
citypw has quit [Ping timeout: 248 seconds]
<pepijndevos> haha, do you ever *not* write "a bit long" articles?
<ZipCPU> They're not usually *this* long
<ZipCPU> The length I struggle for is usually about a quarter of the length of that QSPI article
<pepijndevos> alright, time to pack and head for the bus. I'll have a read later
<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
<ZipCPU> Enjoy!
rohitksingh_work has quit [Read error: Connection reset by peer]
rohitksingh_work has joined #yosys
lutsabound has joined #yosys
rrika has quit [Ping timeout: 258 seconds]
rrika has joined #yosys
rohitksingh_work has quit [Read error: Connection reset by peer]
tlwoerner has quit [Quit: Leaving]
gmc has quit [Ping timeout: 245 seconds]
gmc has joined #yosys
emeb has joined #yosys
<GenTooMan> hmmm does Yosys use a verilog preprocessor?
<daveshah> GenTooMan: yes, it has one built in
<tpb> Title: yosys/preproc.cc at master · YosysHQ/yosys · GitHub (at github.com)
<GenTooMan> daveshah Thanks, that is a relief, it claims verilog 2005 compliance so I should be OK with the macros I am writing
lutsabound has quit [Quit: Connection closed for inactivity]
dys has quit [Ping timeout: 264 seconds]
dys has joined #yosys
GenTooMan has quit [Remote host closed the connection]
GenTooMan has joined #yosys
emeb_mac has joined #yosys
Strobokopp has joined #yosys
dys has quit [Ping timeout: 245 seconds]
dys has joined #yosys
emeb has left #yosys [#yosys]
tpb has quit [Remote host closed the connection]
tpb has joined #yosys