clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
<Postmanmods> *Insert shocked pikachu meme here*
<ZipCPU> The other really cool thing about Verilator is that it's easy to integrate into your desktop environment
<Postmanmods> Genuine question: do they just not care about the software usability that much or what?
<ZipCPU> There's more to the story
<Postmanmods> The design is just... Blech.
<ZipCPU> For example, the Verilog spec says designs need to support 0, 1, x, and z. Verilator only supports 0 and 1
<ZipCPU> By only supporting 0 and 1, it makes it easier to be faster than the vendor sims
<ZipCPU> That's the big thing as I recall
<Postmanmods> How... Did they overlook that?
<Postmanmods> Wat
<Postmanmods> Just goes to show that simpler solutions are typically a good route.
<ZipCPU> Yes
<Postmanmods> Have learned that the hard way. Many many times.
<Postmanmods> So uh
<Postmanmods> I think I just programmed the NVCM with no lattice hardware programmer
<ZipCPU> Is that a good thing?
<Postmanmods> Not sure yet. At least I didnt spend $180 bucks on Lattice's!
<Postmanmods> Just thought it was cool that you can use any off the shelf FT2232 with the diamond programmer software without having to buy expensive firmware.
<Postmanmods> expensive hardware*
<ZipCPU> Yeah ... that's how I managed to program my Max-1000. The expensive software didn't work, the open source software did
<Postmanmods> My story with yosys, it's what brought me here!
<ZipCPU> You have a max-1000 board?
<Postmanmods> Oh no I meant the lattice software wasn't working but yosys did.
<ZipCPU> Oh, yeah
emeb_mac has joined #yosys
vonnieda has joined #yosys
<ZipCPU> Postmanmods: Do you do twitter at all?
<Postmanmods> Do not, but I do have an instagram!
<Postmanmods> I should probably get a twitter...
<ZipCPU> I would've invited you to join my twitter feed. There's been a lot of fun information there
<Postmanmods> @postmanmods on instagram if you are curious.
* ZipCPU doesn't do instragram :/
<Postmanmods> Ah dang. I should probably just use twitter, seems to be more useful.
<ZipCPU> I'm trying to keep a formal verification quiz going every Friday for anyone who wants to participate
<ZipCPU> Not quite sure what this weeks quiz will be (yet) though
<Postmanmods> Count me in! Is it at a certain time?
<ZipCPU> It's a tweet
<Postmanmods> Thats does it, I'm making a twitter.
<ZipCPU> If you want to see some of the quizes I've done so far, check out the last section of: http://zipcpu.com/tutorial/class-verilog.pdf
<ZipCPU> Be aware ... you might see questions (and answers) there that I haven't (yet) asked ... ;)
<Postmanmods> Ha, I have that pdf open in the next tab! I was taking a gander at it.
<ZipCPU> So I try to tweet the quiz on a Friday, and the answer to it on a Monday
<ZipCPU> Anyone who wants to try to answer it in between is welcome to it
<ZipCPU> I've promised not to be sarcastic on really wild guesses, but sometimes I do need to bite my tongue ;)
<ZipCPU> "Why is the sky blue"? "Because ducks have four legs" just doesn't make sense.
<ZipCPU> Some of the answers I've gotten have been just that crazy too ... but in general the quizzes are fun
<Postmanmods> Just made a twitter and followed ya, I'll keep a lookout for the quiz.
<ZipCPU> Look forward to you seeing you around!
<Postmanmods> Same to you! When I actually have money I am definitely subscribing to your patreon. It'll be worth every penny.
<ZipCPU> "When I actually have money" ... Lol! I've been saying that to myself for years too
<ZipCPU> Sure, though, enjoy!
Cerpin has quit [Ping timeout: 264 seconds]
emeb has quit [Quit: Leaving.]
gsi__ has joined #yosys
gsi_ has quit [Ping timeout: 246 seconds]
thasti has quit [Ping timeout: 245 seconds]
PyroPeter has quit [Ping timeout: 250 seconds]
jevinskie has joined #yosys
PyroPeter has joined #yosys
jevinskie has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
Cerpin has joined #yosys
jevinskie has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 255 seconds]
_whitelogger has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 245 seconds]
rohitksingh_work has joined #yosys
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 258 seconds]
jevinski_ has joined #yosys
jevinskie has quit [Ping timeout: 258 seconds]
emeb_mac has quit [Ping timeout: 245 seconds]
futarisIRCcloud has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 250 seconds]
attie has joined #yosys
mjacob has quit [Ping timeout: 276 seconds]
vid has joined #yosys
m4ssi has joined #yosys
fsasm has joined #yosys
vid has quit [Ping timeout: 244 seconds]
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
futarisIRCcloud has joined #yosys
rohitksingh has joined #yosys
vid has joined #yosys
jit10 has joined #yosys
jit10 has quit [Client Quit]
futarisIRCcloud has quit [Quit: Connection closed for inactivity]
rohitksingh has quit [Ping timeout: 246 seconds]
rohitksingh_work has quit [Read error: Connection reset by peer]
vid has quit [Ping timeout: 245 seconds]
vonnieda has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzz…]
rohitksingh has joined #yosys
vonnieda has joined #yosys
emeb has joined #yosys
Ultrasauce has quit [Quit: Ultrasauce]
vid has joined #yosys
rohitksingh has quit [Ping timeout: 268 seconds]
vid has quit [Ping timeout: 244 seconds]
m4ssi has quit [Remote host closed the connection]
rohitksingh has joined #yosys
gnufan_home has joined #yosys
MoeIcenowy has quit [Quit: ZNC 1.6.5+deb1+deb9u1 - http://znc.in]
MoeIcenowy has joined #yosys
voxadam has quit [Max SendQ exceeded]
voxadam has joined #yosys
jevinski_ has quit [Ping timeout: 246 seconds]
jevinskie has joined #yosys
<ZirconiumX> This is entirely the wrong channel for this, and I apologise, but ZipCPU, I think your ISA blog post is buggy.
<ZipCPU> ISA post? Which one was that?
<tpb> Title: A Quick Introduction to the ZipCPU Instruction Set (at zipcpu.com)
<ZipCPU> Ahh, okay, what problem have you found?
<ZirconiumX> You do comparisons through subtraction and setting flags from the result, right?
<ZipCPU> That's one of many ways, yes ... go on
<ZipCPU> Many of the instructions set flags, though, not just the comparison and test instructions, and not just through subtraction. But go on. If there's a bug, I'd like to fix it.
<ZirconiumX> But if you take a signed byte of minimum value (0x80 AKA -128) and subtract a byte of maximum value (0x7F AKA +127), you get +1.
<ZirconiumX> Which doesn't set the negative flag
<ZirconiumX> So -128 is greater than +127
<ZirconiumX> Assuming I've understood this correctly
Ultrasauce has joined #yosys
<ZirconiumX> If not, maybe it could use clarification anyway
<ZipCPU> You are assuming 8-bit values to simplify things, right? Since the ZipCPU only operates on 32-bit values. But I think I'm getting your point
<ZirconiumX> Yes, I am
<ZipCPU> I've been through this through several rounds of getting this right, and I think I have it right (now)
<ZipCPU> If you do an A-B subtraction, the negation flag is set to more than just the high order bit
<ZipCPU> It's the high order bit exclusively or'd to the overflow bit if I recall correctly
* ZipCPU pulls up the code to remind himself
<ZirconiumX> Yeah, that would work
<ZirconiumX> Because you want LT/GE to check that N == V/N != V, I think
<tpb> Title: zipcpu/cpuops.v at master · ZipCPU/zipcpu · GitHub (at github.com)
<ZipCPU> You have the problem on ADDs as well as CMPs and SUBs
<ZirconiumX> I realise it's a "quick introduction", but I found it a little confusing
<ZipCPU> Here' an addition example: 0x80 + 0x80 (i.e. -128 + -128) = 00 (with overflow). The sign bit should be negative in this case as well.
<ZipCPU> Let see what I said in the ALU article ...
<ZipCPU> Yeah, it's discussed here: http://zipcpu.com/zipcpu/2017/08/11/simple-alu.html
<tpb> Title: A Simple ALU, drawn from the ZipCPU (at zipcpu.com)
<ZipCPU> The penultimate section is devoted to flag calculation
<ZirconiumX> I will admit to finding your work on formal methods interesting, ZipCPU, but pretty far beyond me
<ZipCPU> Really? That's a shame. Would you like some simple examples to experiment with?
<ZirconiumX> I can give examples of properties I would like to prove, but I have no idea how to go about proving them. For example, in chess, pieces can't wrap around the chessboard.
<ZipCPU> That one's easy. Add a bit to the position on the chess board, and then do your comparisons
<ZirconiumX> But despite my course in predicate logic, I have no idea how to formalise that one.
<ZirconiumX> Yeah, I've wrote a chess program, so it's something I've had to solve through brute force
<ZipCPU> if (piece == ROOK) assert((ROOK.x - $past(ROOK.x)==1)||(ROOK.x-$past(ROOK.x)==-1)); assert(ROOK.x[4] == 0);
<ZipCPU> You could also do, assert(PIECE.x[4] == 0); assert(PIECE.y[4] == 0);
<ZirconiumX> But it gets progressively more difficult, at least in the software world
<ZirconiumX> I tried to formalise my chess program
<ZipCPU> Well, yeah, that's sort of the nature of formal. The more properties you add, the more challenging things get.
<ZipCPU> Formally verifying software is often harder than formally verifying hardware components
<ZipCPU> At least with hardware components, the size of the state space is fairly well bounded
<ZirconiumX> The main thing for me is that the solver often goes "I don't know how to solve this" without any more hints
<ZipCPU> So, with SymbiYosys, you can often find bugs even if the solver can't fully prove the core
<ZipCPU> Indeed, formally proving a core for all time takes ... some intrusive work into the internal structure of the core in question
<ZipCPU> Perhaps a story would help
<ZipCPU> I've been working on formally verifying an AXI interconnect. This has been quite the challenge for me, and it's now (mostly) verified
<ZipCPU> Then, someone handed me their own AXI interconnect to verify. The code within it was ... computer generated, and not necessarily easy or obvious to understand
<ZipCPU> Instead of trying to verify that core for all time, I was able to find several bugs that would take place in the first 20 timesteps
<ZipCPU> It's not a perfect proof, but it was enough to find some bugs
<ZipCPU> If your experience is with software formal verification, I'd encourage you to look again. You can often do much better with hardware verification--the state of the art matches there better.
<ZirconiumX> Thank you, I think I will
<ZipCPU> ;)
<ZirconiumX> Though writing in Verilog trips me up a little, I think
<ZipCPU> Have you found verilator -Wall or `default_nettype none yet?
<ZipCPU> Those two simple things find a *lot* of the Verilog issues for me
<ZirconiumX> I have, and Yosys catches some things too
<ZipCPU> It sure does
<tnt> I actually find yosys pretty tolerant to "invalid" things.
<tnt> (i.e. things not in the standard that verilator or iverilog choke on)
<ZirconiumX> Which is why I have a """lint""" pass which runs optimisations on my code, and then spits it back out as Verilog. If I'm doing something dumb the optimiser generally turns the code to garbage
<ZirconiumX> Probably not the smartest idea, but hey, I'm someone who stares at the output of their compiler
rohitksingh has quit [Ping timeout: 258 seconds]
rohitksingh has joined #yosys
maikmerten has joined #yosys
<maikmerten> seems Lattice needed to produce another batch of HX8K eval boards. The board I received last year has date codes from 2019, the one I received today seems to have a first week 2019 marking.
<maikmerten> err... the one I received last year has date codes from *2013*
<maikmerten> the FPGA device also now has Lattice markings, the jumpers are white - and look hand-soldered :-)
<tnt> Ah yeah, I think my first dev board was still marked Silicon Blue :)
fsasm has quit [Ping timeout: 244 seconds]
<maikmerten> yup - the board I received last year (from Mouser) also has those old markings. The FPGA has a date code "1230", so week 30 of 2012
<maikmerten> seems they had nice big batch produced in 2013 which lasted for years on some distribution channels
<maikmerten> (wow, the LT3030 LDO is a ~7$ part. Seems pretty expensive for two voltages at 750 and 250 mA)
<tnt> it's a fancy ldo :)
<tnt> Mmm .... I was giving formal a quick try, I figured I'd test a simple fifo I wrote. But looking athe examples in https://github.com/ZipCPU/wbuart32/blob/master/rtl/ufifo.v for instance, but I don't really see how it checks what I'd really expect from a FIFO ... i.e. what goes in, comes out in the same order ...
<tpb> Title: wbuart32/ufifo.v at master · ZipCPU/wbuart32 · GitHub (at github.com)
<ZipCPU> tnt: Let me suggest a different example for you
<ZipCPU> http://zipcpu.com/tutorial , lesson 10
<tpb> Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com)
<ZipCPU> The ufifo proof is one of my earlier ones, and as you've pointed out, it's not nearly as complete as some of my other ones
jevinskie has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
proteusguy has quit [Ping timeout: 258 seconds]
Jybz has joined #yosys
rohitksingh has quit [Remote host closed the connection]
maikmerten has quit [Remote host closed the connection]
<tnt> ZipCPU: mm, trying to replicate the same for my code, but so far I get 'PASS' even when trying to assert on obviously false property.
<tnt> but at least that example match more what I'd expect tx.
<ZipCPU> Are you working on a FIFO?
<ZipCPU> Are you assert()ing outputs and local state, while assume()ing any inputs?
<tpb> Title: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - Pastebin.com (at pastebin.com)
<tnt> "assert((f_used > 0) == rd_empty);" this should obviously be false.
<ZipCPU> Lines 131 and 132 belong in always blocks
* ZipCPU is still looking
<tnt> ok, I guess the 'assert' is also in a always.
<ZipCPU> Did you get the cover traces?
<ZipCPU> Yes, the free version of yosys only supports "immediate" assertions. "immediate" assertions must be in always blocks
<tnt> No, it's not generating any vcd
<ZipCPU> Are you using SymbiYosys?
<tnt> yup, pretty much copied the .sby from your example.
<tpb> Title: [tasks] prf cvr [options] prf: mode prove prf: depth 5 cvr: mode cover cvr: dep - Pastebin.com (at pastebin.com)
<ZipCPU> Are you sure you want assign f_empty == (f_used != 8'h00)? Shouldn't it be "f_empty == (f_used == 8'h00)"?
<tnt> Doh ... yeah, obviousy ...
<tnt> didn't really change anything though
<ZipCPU> Did it create two directories?
<tnt> How does it know to generate a clk/rst ?
<tnt> yes fifo_sync_shift_prf / fifo_sync_shift_cvr
<ZipCPU> The clock is automatic, you need to generate the reset
<tnt> same as when I run your example, except with yours I get a vcd .
<ZipCPU> You should find traces in the fifo_sync_shift_*/engine_0/ directories
<ZipCPU> If they aren't there, then check the fifo_sync_shift_*/logfile.txt files
<tnt> nope, no traces
<tnt> ## 0:00:00 Solver: yices
<tnt> ## 0:00:00 Status: PASSED
<ZipCPU> Which file was that one from?
<tnt> cover
<tnt> fifo_sync_shift_cvr/engine_0/logfile.txt
<ZipCPU> And yet no traces in fifo_sync_shift_cvr/engine_0/ ?
<tpb> Title: tnt@rei /tmp/formal/fifo $ cat fifo_sync_shift_prf/engine_0/logfile_* ## 0:00 - Pastebin.com (at pastebin.com)
<tnt> nope only the logfile
<ZipCPU> So, in the *_prf/ directory, no traces could mean that everything is working
<ZipCPU> In the *_cvr/ directory, no traces and PASS means that SymbiYosys didn't find any cover statements in your file
<ZipCPU> Can you post the logfile from the *_cvr directory?
<tnt> that's the 2 lines I posted above
<ZipCPU> Ok, time to roll up our sleeves. There should be a log file in *_*/model/design.log
<tnt> oh, you meant not the engine one. https://pastebin.com/VzwGAFzf
<tpb> Title: SBY 22:44:46 [fifo_sync_shift_prf] Removing direcory 'fifo_sync_shift_prf'. SBY - Pastebin.com (at pastebin.com)
<ZipCPU> Hmm ... yeah, that means it didn't find any cover statements in your design, so it ended quickly
<ZipCPU> Found the bug
<ZipCPU> You need an ifdef FORMAL not FORMAT
<tnt> ...
* tnt hides
<ZipCPU> (We've all done it)
* ZipCPU looks for sweets to coax tnt out of hiding
emeb_mac has joined #yosys
<tnt> now it indeed fails :) (like expected)
<ZipCPU> Yaaayy!!!
<ZipCPU> Makes more sense, now, huh? ;)
<tnt> yup. Now I probably need to generate a proper reset
<ZipCPU> initial assume(i_reset); often works
<tnt> indeed, thanks.
<tnt> it passes coverage now.
<ZipCPU> Nice
<dormando> is "logic design adn verification using systemverilog (revised)" as good as it sounds? looks like yosys supports a decent chunk of it
<dormando> all my verilog knowledge is based off super old materials
<ZipCPU> The free version of Yosys only supports some SV features. There's a commercial version that supports SV+VHDL+Verilog
<dormando> pretty sure I don't need the full stack.
<dormando> trying to arm myself a bit better for my next project, but reading material is hard to find. half of it are your blog posts :)
<ZipCPU> Thanks for the compliments!
<dormando> it's been a big help. wrote a fifo loosely based off your post for my last one
<ZipCPU> Is there something particular you are looking for that I might help you find?
<dormando> not really sure. I come from a background of "new language? read the spec!" but there's a huge variance within the tooling for fpga-land
* ZipCPU sighs heavily
<ZipCPU> That's one of the things I like about using Yosys. You can go from yosys to just about any back end
<dormando> and I haven't come to an understanding how different authors end up with their coding style. I landed in one that's explicit enough to me, but it feels like the style is tooling dependent too
<dormando> ie: how well the backend can decide to use FF's instead of latches, some convert *'s that can be shifts into shift's automatically, and so on
<ZipCPU> Have you seen my article about minimizing LUTs? That accounts for at least some of my coding style
<ZipCPU> FF's and latches though ... that's easy
<dormando> I may have but haven't read it yet? Culling LUT's is where I'll be starting next. I might have to hack a script to get nextpnr to visualize modules for me :)
<ZipCPU> If you set anything on the posedge of a clock, always @(posedge i_clk) a <= b; // it'll use a FF
<dormando> cool. so how do you... find that knowledge in the first place? or the rules around it?
<ZipCPU> Typically, latches are *bad*. Therefore you'll want to avoid them. That's easily done by making sure that any time you set something in an always @(*) block, you make sure it gets set a value other than it's current one
* ZipCPU sits back
<dormando> Yeah. so I aggressively destroy latches
<ZipCPU> I got schooled by Clifford when my stuff didn't work
<ZipCPU> ;D
<dormando> but I've tried to match some coding style to some of those who don't set much in combinatorial blocks
<dormando> and inevitably I stumbled on some combination of things that degraded into a latch (in ISE)
<ZipCPU> There's another way to avoid latches: use an always_comb @(*) block
<dormando> so I'm not sure how much of that is solved by just using yosys or the newer xilinx tooling
<dormando> always_comb is systemverilog right?
<ZipCPU> Yosys supports it
<dormando> right.
<ZipCPU> It also supports (IIRC) always_latch and always_ff
<dormando> it does
<dormando> this book I was asking about goes over these extensions. I wasn't finding much online :)
<dormando> I'm like dang, I really wish I had these months ago, haha
<ZipCPU> You should be able to find an SV spec on line. It's not much, but it might help
<ZipCPU> I did write a Verilog tutorial, but I'm not sure I went into that much depth
<dormando> Yeah I found it. it doesn't do much for style tho.
<tpb> Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com)
<ZipCPU> Try this, it might help (some): http://zipcpu.com/blog/2017/06/12/minimizing-luts.html
<tpb> Title: Minimizing FPGA Resource Utilization (at zipcpu.com)
<dormando> like golang has this huge page on what makes good golang style.. and (sorry I forgot his name) in verilog land has that huge paper on doing cross-domain clock stuff
<dormando> the specs need to be paired with more of those kinds of papers for people to really grok style
<ZipCPU> Ooohh, first rule: avoid cross-domain clocks like the plague
<tpb> Title: Rules for new FPGA designers (at zipcpu.com)
<ZipCPU> There's a time for them, but they aren't easy to work with--so I avoid them to the extent that I can
<dormando> haha.
<dormando> Yeah. I had a blast learning how to use them.
<dormando> think your blogs were in that process too
<ZipCPU> Glad I could help ;)
<dormando> I got my raycasting engine up to 20+ FPS at 320x240 on a tinfyga BX by cranking the SPI clock to 150mhz
<dormando> but rest of the design is still 16mhz
<dormando> it runs faster than an actual 386 would've run wolf3d
<ZipCPU> :)
<dormando> anyway sorry for the spam. appreciate the tips.
<ZipCPU> :D
<tnt> :/ "it might start processing from an unreachable state you aren’t expecting." ...
<tnt> arf
<ZipCPU> dormando: Let me know if there's something you are looking for, stuck with, or something I might help you find
<dormando> my next trick is porting the DOOM rendering engine to arduino + lp8k, so I need to cut LUT's down and improve testing
<ZipCPU> tnt: Yep!
<ZipCPU> You can fix that by adding assertions to prevent it from starting there
<dormando> but at the start of every project I also go hunting for new material to help with coding style.. so I'm not really sure what questions to ask yet
<ZipCPU> tnt: Remember: assume inputs, assert local state and outputs
<ZipCPU> dormando: You must learn the ways of formal :D
<dormando> I at very least need automated testing :) I miss "make test" so much
<dormando> verilator looks cool
<tnt> ZipCPU: I was kind of hoping this would be more "black box" than this.
<tpb> Title: Makefiles for formal proofs with SymbiYosys (at zipcpu.com)
<ZipCPU> tnt: Only BMC is black box. Formal in general is *very* white box
<tnt> (so I could change completely the underlying implementation and just check external properties)
<dormando> perfect :)
<ZipCPU> tnt: There is some ability to do that
<ZipCPU> *some*
gnufan_home has quit [Quit: Leaving.]
<tnt> \o/ it passed the induction step now.
<daveshah> IC3 solvers like abc pdr are truly "black box"
<daveshah> But they tend to suffer from combinational explosion more
<ZipCPU> daveshah: They also seem to be quite limited in their capability
<ZipCPU> You said it
<daveshah> And unlike smt they don't support memories
<daveshah> So those have to be blasted to logic first, not helping things performance wise either
<ZipCPU> tnt: o/
<tnt> atm the only property I'm checking is my empty flag, so it's not a super strong proof of validity :p
<ZipCPU> Yes, but consider how much work it takes to get hello world running. You've finally passed that threshold it seems.
<tnt> Some properties I'm not sure yet how to express. like "if there is no data, empty should be 1" that's easy. But if there is a least one data, empty should fall _eventually_ (but not at the next cycle, that could be implementation dependent)
<ZipCPU> Not necessarily
<ZipCPU> You might have a FIFO that never fully empties
<ZipCPU> So what you want to state is not that empty must fall, but rather that it is able to fall
<ZipCPU> Consider line 169 here: https://pastebin.com/PRZucVXj
<tpb> Title: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - Pastebin.com (at pastebin.com)
<ZipCPU> That proves that it is possible to empty the FIFO after it has been full
<tnt> yes, possible.
<tnt> but I was more thinking of the case where you push 1 single word and empty stays asserted for instance.
<ZipCPU> You mean, verify that after pushing a word empty falls?
<tnt> yes.
<tnt> but not at the next cycle ... pipeline delays could make it happens 1,2,3,... cycles later.
<tnt> (not in this implementation obviously but in general for a fifo)
Jybz has quit [Quit: Konversation terminated!]
<ZipCPU> So ... consider that the crossbar I've been working on is similar
<ZipCPU> Requests can be made by any of the bus masters, and then forwarded to the slaves
<ZipCPU> In the middle, there are a couple of stages of pipeline processing ... waiting for an channel grant, and a couple of skid buffers
<ZipCPU> I can verify that the slave has the right counts (ignoring the interconnect), and I can verify that the master does
<ZipCPU> To handle the interconnect, I assume a functioning slave and a functioning master, and then have to prove that they are each driven properly
<ZipCPU> That includes correlating the transaction counters in my formal property set between the masters and the slaves, so I have to account for every piece of data transiting through the pipeline in this task
<tnt> heh, yeah, that's a couple of difficulty notch above :p
<ZipCPU> It's not really all that much more difficult than managing a bunch of counters
<tnt> ZipCPU: anyway, time to sleep. Thanks for your help !
<ZipCPU> ;) Sleep well
vonnieda has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzz…]
emeb has quit [Quit: Leaving.]
tpb has quit [Remote host closed the connection]
tpb has joined #yosys