Thursday, 2019-05-16

*** tpb has joined #yosys00:00
PostmanmodsIts. The. WORST!00:00
ZipCPUNah, it's not nearly that bad ... but you need to learn the ways of the formal methods00:00
PostmanmodsSo I have been only dealing in Lattice thus far. Which FPGA would you say is the best in general?00:00
PostmanmodsOr your preferred?00:01
ZipCPUThat's a hard question00:01
PostmanmodsI know,  different pros and cons, but what is your go to?00:01
ZipCPUI tend to prefer Digilent as a source for my boards.  They tend to be well documented.  That puts me often in the Xilinx camp.  The problem is ... the open source tools don't work with Xilinx (much) yet00:01
ZipCPUSo I've got a bunch of iCE40 and ECP5 boards on my desk that I'm working with as well00:01
ZipCPUThey aren't nearly as well documented as the Xilinx ones are--or if they are I haven't found the key documents (yet)00:02
PostmanmodsOh hang, I need your opinion on a dev cyclone board (if its worth the $$ or not)00:02
ZipCPUI only have one cyclone board, the DE-10 Nano00:03
tpbTitle: Terasic - All FPGA Main Boards - Cyclone V - DE10-Nano Kit (at
ZipCPUI do have a max-1000 board as well00:03
PostmanmodsTHAT SOLVES THAT LOL00:03
PostmanmodsThe link is to a DE1000:03
ZipCPUI wrote about my experiences with the DE10-nano on the blog00:03
PostmanmodsNo way00:04
PostmanmodsThats a weird coincidence...00:04
ZipCPUNot really ... I've done a *lot* of writing00:04
PostmanmodsI highly appreciate the effort in this00:04
ZipCPUThe blog has lots of good stuff on it00:05
PostmanmodsIt's extremely well put together, I really dig the learning method. Resonates with me, ya now?00:05
ZipCPUThat's my argument00:05
ZipCPUHere's my thesis: Verilog design needs to be taught hand-in-hand with how to work with a good simulator (Verilator) and formal tools.  Without those, you'll end up like so many students at the end of a semester with a design that sort-of works00:06
PostmanmodsHmmm... Haven't gotten that far yet. Verilator simulates the ckt?00:07
ZipCPUTechnically Verilator just converts Verilog to C++00:07
ZipCPUYou can then use that for simulation.  Supposedly (I haven't done the measurements) it's at least as good as if not better (i.e. faster) than the big vendor simulators00:07
Postmanmods*Insert shocked pikachu meme here*00:08
ZipCPUThe other really cool thing about Verilator is that it's easy to integrate into your desktop environment00:08
PostmanmodsGenuine question: do they just not care about the software usability that much or what?00:08
ZipCPUThere's more to the story00:09
PostmanmodsThe design is just... Blech.00:09
ZipCPUFor example, the Verilog spec says designs need to support 0, 1, x, and z.  Verilator only supports 0 and 100:10
ZipCPUBy only supporting 0 and 1, it makes it easier to be faster than the vendor sims00:10
ZipCPUThat's the big thing as I recall00:11
PostmanmodsHow... Did they overlook that?00:11
PostmanmodsJust goes to show that simpler solutions are typically a good route.00:12
PostmanmodsHave learned that the hard way. Many many times.00:12
PostmanmodsSo uh00:27
PostmanmodsI think I just programmed the NVCM with no lattice hardware programmer00:27
ZipCPUIs that a good thing?00:27
PostmanmodsNot sure yet. At least I didnt spend $180 bucks on Lattice's!00:28
PostmanmodsJust thought it was cool that you can use any off the shelf FT2232 with the diamond programmer software without having to buy expensive firmware.00:29
Postmanmodsexpensive hardware*00:30
ZipCPUYeah ... that's how I managed to program my Max-1000.  The expensive software didn't work, the open source software did00:30
PostmanmodsMy story with yosys, it's what brought me here!00:31
ZipCPUYou have a max-1000 board?00:31
PostmanmodsOh no I meant the lattice software wasn't working but yosys did.00:32
ZipCPUOh, yeah00:32
*** emeb_mac has joined #yosys00:41
*** vonnieda has joined #yosys00:53
ZipCPUPostmanmods: Do you do twitter at all?01:07
PostmanmodsDo not, but I do have an instagram!01:08
PostmanmodsI should probably get a twitter...01:08
ZipCPUI would've invited you to join my twitter feed.  There's been a lot of fun information there01:08
Postmanmods@postmanmods on instagram if you are curious.01:08
* ZipCPU doesn't do instragram :/01:08
PostmanmodsAh dang. I should probably just use twitter, seems to be more useful.01:09
ZipCPUI'm trying to keep a formal verification quiz going every Friday for anyone who wants to participate01:09
ZipCPUNot quite sure what this weeks quiz will be (yet) though01:10
PostmanmodsCount me in! Is it at a certain time?01:11
ZipCPUIt's a tweet01:12
PostmanmodsThats does it, I'm making a twitter.01:12
ZipCPUIf you want to see some of the quizes I've done so far, check out the last section of:
ZipCPUBe aware ... you might see questions (and answers) there that I haven't (yet) asked ... ;)01:13
PostmanmodsHa, I have that pdf open in the next tab! I was taking a gander at it.01:13
ZipCPUSo I try to tweet the quiz on a Friday, and the answer to it on a Monday01:13
ZipCPUAnyone who wants to try to answer it in between is welcome to it01:14
ZipCPUI've promised not to be sarcastic on really wild guesses, but sometimes I do need to bite my tongue ;)01:14
ZipCPU"Why is the sky blue"?  "Because ducks have four legs"   just doesn't make sense.01:14
ZipCPUSome of the answers I've gotten have been just that crazy too ... but in general the quizzes are fun01:18
PostmanmodsJust made a twitter and followed ya, I'll keep a lookout for the quiz.01:23
ZipCPULook forward to you seeing you around!01:26
PostmanmodsSame to you! When I actually have money I am definitely subscribing to your patreon. It'll be worth every penny.01:28
ZipCPU"When I actually have money" ... Lol!  I've been saying that to myself for years too01:28
ZipCPUSure, though, enjoy!01:28
*** Cerpin has quit IRC01:29
*** emeb has quit IRC01:45
*** gsi__ has joined #yosys02:13
*** gsi_ has quit IRC02:16
*** thasti has quit IRC02:32
*** PyroPeter has quit IRC02:53
*** jevinskie has joined #yosys02:54
*** PyroPeter has joined #yosys03:06
*** jevinskie has quit IRC03:44
*** Cerpin has joined #yosys03:58
*** jevinskie has joined #yosys04:08
*** rohitksingh has joined #yosys04:34
*** rohitksingh has quit IRC04:39
*** _whitelogger has quit IRC04:50
*** _whitelogger has joined #yosys04:52
*** rohitksingh has joined #yosys05:16
*** rohitksingh has quit IRC05:22
*** rohitksingh_work has joined #yosys05:36
*** futarisIRCcloud has quit IRC06:10
*** rohitksingh has joined #yosys06:13
*** rohitksingh has quit IRC06:30
*** jevinski_ has joined #yosys06:52
*** jevinskie has quit IRC06:53
*** emeb_mac has quit IRC07:06
*** futarisIRCcloud has joined #yosys07:16
*** rohitksingh has joined #yosys07:36
*** rohitksingh has quit IRC07:46
*** attie has joined #yosys08:06
*** mjacob has quit IRC08:10
*** vid has joined #yosys08:29
*** m4ssi has joined #yosys08:45
*** fsasm has joined #yosys09:03
*** vid has quit IRC09:14
*** futarisIRCcloud has quit IRC09:30
*** futarisIRCcloud has joined #yosys09:56
*** rohitksingh has joined #yosys09:57
*** vid has joined #yosys11:04
*** jit10 has joined #yosys11:35
*** futarisIRCcloud has quit IRC12:05
*** rohitksingh has quit IRC12:40
*** rohitksingh_work has quit IRC12:56
*** vid has quit IRC13:23
*** vonnieda has quit IRC13:58
*** rohitksingh has joined #yosys14:07
*** vonnieda has joined #yosys14:15
*** emeb has joined #yosys14:43
*** Ultrasauce has quit IRC15:41
*** vid has joined #yosys15:44
*** rohitksingh has quit IRC15:46
*** vid has quit IRC16:00
*** m4ssi has quit IRC16:12
*** rohitksingh has joined #yosys16:16
*** gnufan_home has joined #yosys16:22
*** MoeIcenowy has quit IRC16:32
*** MoeIcenowy has joined #yosys16:32
*** voxadam has quit IRC16:40
*** voxadam has joined #yosys16:40
*** jevinski_ has quit IRC17:06
*** jevinskie has joined #yosys17:09
ZirconiumXThis is entirely the wrong channel for this, and I apologise, but ZipCPU, I think your ISA blog post is buggy.17:18
ZipCPUISA post?  Which one was that?17:18
tpbTitle: A Quick Introduction to the ZipCPU Instruction Set (at
ZipCPUAhh, okay, what problem have you found?17:19
ZirconiumXYou do comparisons through subtraction and setting flags from the result, right?17:20
ZipCPUThat's one of many ways, yes ... go on17:20
ZipCPUMany 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.17:21
ZirconiumXBut 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.17:23
ZirconiumXWhich doesn't set the negative flag17:24
ZirconiumXSo -128 is greater than +12717:24
ZirconiumXAssuming I've understood this correctly17:24
*** Ultrasauce has joined #yosys17:25
ZirconiumXIf not, maybe it could use clarification anyway17:25
ZipCPUYou 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 point17:25
ZirconiumXYes, I am17:25
ZipCPUI've been through this through several rounds of getting this right, and I think I have it right (now)17:25
ZipCPUIf you do an A-B subtraction, the negation flag is set to more than just the high order bit17:26
ZipCPUIt's the high order bit exclusively or'd to the overflow bit if I recall correctly17:26
* ZipCPU pulls up the code to remind himself17:26
ZirconiumXYeah, that would work17:26
ZirconiumXBecause you want LT/GE to check that N == V/N != V, I think17:27
ZipCPUHere it is:
tpbTitle: zipcpu/cpuops.v at master · ZipCPU/zipcpu · GitHub (at
ZipCPUYou have the problem on ADDs as well as CMPs and SUBs17:29
ZirconiumXI realise it's a "quick introduction", but I found it a little confusing17:29
ZipCPUHere' an addition example: 0x80 + 0x80 (i.e. -128 + -128) = 00 (with overflow).  The sign bit should be negative in this case as well.17:29
ZipCPULet see what I said in the ALU article ...17:30
ZipCPUYeah, it's discussed here:
tpbTitle: A Simple ALU, drawn from the ZipCPU (at
ZipCPUThe penultimate section is devoted to flag calculation17:31
ZirconiumXI will admit to finding your work on formal methods interesting, ZipCPU, but pretty far beyond me17:32
ZipCPUReally?  That's a shame.  Would you like some simple examples to experiment with?17:33
ZirconiumXI 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.17:33
ZipCPUThat one's easy.  Add a bit to the position on the chess board, and then do your comparisons17:34
ZirconiumXBut despite my course in predicate logic, I have no idea how to formalise that one.17:34
ZirconiumXYeah, I've wrote a chess program, so it's something I've had to solve through brute force17:34
ZipCPUif (piece == ROOK) assert((ROOK.x - $past(ROOK.x)==1)||(ROOK.x-$past(ROOK.x)==-1)); assert(ROOK.x[4] == 0);17:35
ZipCPUYou could also do, assert(PIECE.x[4] == 0); assert(PIECE.y[4] == 0);17:36
ZirconiumXBut it gets progressively more difficult, at least in the software world17:38
ZirconiumXI tried to formalise my chess program17:38
ZipCPUWell, yeah, that's sort of the nature of formal.  The more properties you add, the more challenging things get.17:38
ZipCPUFormally verifying software is often harder than formally verifying hardware components17:39
ZipCPUAt least with hardware components, the size of the state space is fairly well bounded17:39
ZirconiumXThe main thing for me is that the solver often goes "I don't know how to solve this" without any more hints17:41
ZipCPUSo, with SymbiYosys, you can often find bugs even if the solver can't fully prove the core17:42
ZipCPUIndeed, formally proving a core for all time takes ... some intrusive work into the internal structure of the core in question17:42
ZipCPUPerhaps a story would help17:42
ZipCPUI've been working on formally verifying an AXI interconnect.  This has been quite the challenge for me, and it's now (mostly) verified17:43
ZipCPUThen, someone handed me their own AXI interconnect to verify.  The code within it was ... computer generated, and not necessarily easy or obvious to understand17:43
ZipCPUInstead of trying to verify that core for all time, I was able to find several bugs that would take place in the first 20 timesteps17:43
ZipCPUIt's not a perfect proof, but it was enough to find some bugs17:44
ZipCPUIf 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.17:46
ZirconiumXThank you, I think I will17:57
ZirconiumXThough writing in Verilog trips me up a little, I think17:57
ZipCPUHave you found verilator -Wall or `default_nettype none yet?17:58
ZipCPUThose two simple things find a *lot* of the Verilog issues for me17:58
ZirconiumXI have, and Yosys catches some things too17:58
ZipCPUIt sure does17:58
tntI actually find yosys pretty tolerant to "invalid" things.17:59
tnt(i.e. things not in the standard that verilator or iverilog choke on)17:59
ZirconiumXWhich 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 garbage18:00
ZirconiumXProbably not the smartest idea, but hey, I'm someone who stares at the output of their compiler18:03
*** rohitksingh has quit IRC18:34
*** rohitksingh has joined #yosys18:40
*** maikmerten has joined #yosys18:57
maikmertenseems 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.19:00
maikmertenerr... the one I received last year has date codes from *2013*19:01
maikmertenthe FPGA device also now has Lattice markings, the jumpers are white - and look hand-soldered :-)19:01
tntAh yeah, I think my first dev board was still marked Silicon Blue :)19:04
*** fsasm has quit IRC19:05
maikmertenyup - the board I received last year (from Mouser) also has those old markings. The FPGA has a date code "1230", so week 30 of 201219:05
maikmertenseems they had nice big batch produced in 2013 which lasted for years on some distribution channels19:06
maikmerten(wow, the LT3030 LDO is a ~7$ part. Seems pretty expensive for two voltages at 750 and 250 mA)19:13
tntit's a fancy ldo :)19:40
tntMmm .... I was giving formal a quick try, I figured I'd test a simple fifo I wrote. But looking athe examples in 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 ...19:43
tpbTitle: wbuart32/ufifo.v at master · ZipCPU/wbuart32 · GitHub (at
ZipCPUtnt: Let me suggest a different example for you19:44
ZipCPU , lesson 1019:44
tpbTitle: Verilog, Formal Verification and Verilator Beginner's Tutorial (at
ZipCPUThe 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 ones19:45
*** jevinskie has quit IRC19:47
*** proteusguy has quit IRC20:04
*** Jybz has joined #yosys20:12
*** rohitksingh has quit IRC20:38
*** maikmerten has quit IRC20:38
tntZipCPU: mm, trying to replicate the same for my code, but so far I get 'PASS' even when trying to assert on obviously false property.20:40
tntbut at least that example match more what I'd expect tx.20:40
ZipCPUAre you working on a FIFO?20:40
ZipCPUAre you assert()ing outputs and local state, while assume()ing any inputs?20:41
tpbTitle: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - (at
tnt"assert((f_used > 0) == rd_empty);"  this should obviously be false.20:42
ZipCPULines 131 and 132 belong in always blocks20:43
* ZipCPU is still looking20:43
tntok, I guess the 'assert' is also in a always.20:45
ZipCPUDid you get the cover traces?20:45
ZipCPUYes, the free version of yosys only supports "immediate" assertions.  "immediate" assertions must be in always blocks20:45
tntNo, it's not generating any vcd20:45
ZipCPUAre you using SymbiYosys?20:45
tntyup, pretty much copied the .sby from your example.20:46
tpbTitle: [tasks] prf cvr [options] prf: mode prove prf: depth 5 cvr: mode cover cvr: dep - (at
ZipCPUAre you sure you want assign f_empty == (f_used != 8'h00)?  Shouldn't it be "f_empty == (f_used == 8'h00)"?20:47
tntDoh ... yeah, obviousy ...20:47
tntdidn't really change anything though20:48
ZipCPUDid it create two directories?20:48
tntHow does it know to generate a clk/rst ?20:48
tntyes fifo_sync_shift_prf / fifo_sync_shift_cvr20:48
ZipCPUThe clock is automatic, you need to generate the reset20:49
tntsame as when I run your example, except with yours I get a vcd .20:49
ZipCPUYou should find traces in the fifo_sync_shift_*/engine_0/ directories20:49
ZipCPUIf they aren't there, then check the fifo_sync_shift_*/logfile.txt files20:49
tntnope, no traces20:49
tnt##   0:00:00  Solver: yices20:49
tnt##   0:00:00  Status: PASSED20:49
ZipCPUWhich file was that one from?20:50
ZipCPUAnd yet no traces in fifo_sync_shift_cvr/engine_0/ ?20:50
tpbTitle: [email protected] /tmp/formal/fifo $ cat fifo_sync_shift_prf/engine_0/logfile_* ## 0:00 - (at
tntnope only the logfile20:51
ZipCPUSo, in the *_prf/ directory, no traces could mean that everything is working20:51
ZipCPUIn the *_cvr/ directory, no traces and PASS means that SymbiYosys didn't find any cover statements in your file20:52
ZipCPUCan you post the logfile from the *_cvr directory?20:52
tntthat's the 2 lines I posted above20:52
ZipCPUOk, time to roll up our sleeves.  There should be a log file in *_*/model/design.log20:53
tntoh, you meant not the engine one.
tpbTitle: SBY 22:44:46 [fifo_sync_shift_prf] Removing direcory 'fifo_sync_shift_prf'. SBY - (at
ZipCPUHmm ... yeah, that means it didn't find any cover statements in your design, so it ended quickly20:54
ZipCPUFound the bug20:54
ZipCPUYou need an ifdef FORMAL not FORMAT20:54
* tnt hides20:54
ZipCPU(We've all done it)20:54
* ZipCPU looks for sweets to coax tnt out of hiding20:55
*** emeb_mac has joined #yosys20:55
tntnow it indeed fails :) (like expected)20:55
ZipCPUMakes more sense, now, huh?  ;)20:56
tntyup. Now I probably need to generate a proper reset20:59
ZipCPUinitial assume(i_reset); often works20:59
tntindeed, thanks.21:00
tntit passes coverage now.21:00
dormandois "logic design adn verification using systemverilog (revised)" as good as it sounds? looks like yosys supports a decent chunk of it21:02
dormandoall my verilog knowledge is based off super old materials21:02
ZipCPUThe free version of Yosys only supports some SV features.  There's a commercial version that supports SV+VHDL+Verilog21:03
dormandopretty sure I don't need the full stack.21:03
dormandotrying to arm myself a bit better for my next project, but reading material is hard to find. half of it are your blog posts :)21:07
ZipCPUThanks for the compliments!21:07
dormandoit's been a big help. wrote a fifo loosely based off your post for my last one21:08
ZipCPUIs there something particular you are looking for that I might help you find?21:08
dormandonot really sure. I come from a background of "new language? read the spec!" but there's a huge variance within the tooling for fpga-land21:08
* ZipCPU sighs heavily21:09
ZipCPUThat's one of the things I like about using Yosys.  You can go from yosys to just about any back end21:09
dormandoand 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 too21:09
dormandoie: 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 on21:10
ZipCPUHave you seen my article about minimizing LUTs?  That accounts for at least some of my coding style21:10
ZipCPUFF's and latches though ... that's easy21:10
dormandoI 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 :)21:11
ZipCPUIf you set anything on the posedge of a clock, always @(posedge i_clk) a <= b; // it'll use a FF21:11
dormandocool. so how do you... find that knowledge in the first place? or the rules around it?21:11
ZipCPUTypically, 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 one21:11
* ZipCPU sits back21:12
dormandoYeah. so I aggressively destroy latches21:12
ZipCPUI got schooled by Clifford when my stuff didn't work21:12
dormandobut I've tried to match some coding style to some of those who don't set much in combinatorial blocks21:12
dormandoand inevitably I stumbled on some combination of things that degraded into a latch (in ISE)21:12
ZipCPUThere's another way to avoid latches: use an always_comb @(*) block21:13
dormandoso I'm not sure how much of that is solved by just using yosys or the newer xilinx tooling21:13
dormandoalways_comb is systemverilog right?21:13
ZipCPUYosys supports it21:13
ZipCPUIt also supports (IIRC) always_latch and always_ff21:13
dormandoit does21:13
dormandothis book I was asking about goes over these extensions. I wasn't finding much online :)21:14
dormandoI'm like dang, I really wish I had these months ago, haha21:14
ZipCPUYou should be able to find an SV spec on line.  It's not much, but it might help21:14
ZipCPUI did write a Verilog tutorial, but I'm not sure I went into that much depth21:14
dormandoYeah I found it. it doesn't do much for style tho.21:14
tpbTitle: Verilog, Formal Verification and Verilator Beginner's Tutorial (at
ZipCPUTry this, it might help (some):
tpbTitle: Minimizing FPGA Resource Utilization (at
dormandolike 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 stuff21:15
dormandothe specs need to be paired with more of those kinds of papers for people to really grok style21:15
ZipCPUOoohh, first rule: avoid cross-domain clocks like the plague21:15
tpbTitle: Rules for new FPGA designers (at
ZipCPUThere's a time for them, but they aren't easy to work with--so I avoid them to the extent that I can21:16
dormandoYeah. I had a blast learning how to use them.21:16
dormandothink your blogs were in that process too21:16
ZipCPUGlad I could help ;)21:16
dormandoI got my raycasting engine up to 20+ FPS at 320x240 on a tinfyga BX by cranking the SPI clock to 150mhz21:16
dormandobut rest of the design is still 16mhz21:16
dormandoit runs faster than an actual 386 would've run wolf3d21:17
dormandoanyway sorry for the spam. appreciate the tips.21:17
tnt:/ "it might start processing from an unreachable state you aren’t expecting." ...21:18
ZipCPUdormando: Let me know if there's something you are looking for, stuck with, or something I might help you find21:18
dormandomy next trick is porting the DOOM rendering engine to arduino + lp8k, so I need to cut LUT's down and improve testing21:18
ZipCPUtnt: Yep!21:18
ZipCPUYou can fix that by adding assertions to prevent it from starting there21:18
dormandobut 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 yet21:18
ZipCPUtnt: Remember: assume inputs, assert local state and outputs21:19
ZipCPUdormando: You must learn the ways of formal :D21:19
dormandoI at very least need automated testing :) I miss "make test" so much21:19
dormandoverilator looks cool21:20
tntZipCPU: I was kind of hoping this would be more "black box" than this.21:20
tpbTitle: Makefiles for formal proofs with SymbiYosys (at
ZipCPUtnt: Only BMC is black box.  Formal in general is *very* white box21:20
tnt(so I could change completely the underlying implementation and just check external properties)21:20
dormandoperfect :)21:20
ZipCPUtnt: There is some ability to do that21:21
*** gnufan_home has quit IRC21:31
tnt\o/ it passed the induction step now.21:39
daveshahIC3 solvers like abc pdr are truly "black box"21:40
daveshahBut they tend to suffer from combinational explosion more21:40
ZipCPUdaveshah: They also seem to be quite limited in their capability21:40
ZipCPUYou said it21:41
daveshahAnd unlike smt they don't support memories21:41
daveshahSo those have to be blasted to logic first, not helping things performance wise either21:41
ZipCPUtnt: o/21:41
tntatm the only property I'm checking is my empty flag, so it's not a super strong proof of validity :p21:43
ZipCPUYes, but consider how much work it takes to get hello world running.  You've finally passed that threshold it seems.21:44
tntSome 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)21:47
ZipCPUNot necessarily21:48
ZipCPUYou might have a FIFO that never fully empties21:48
ZipCPUSo what you want to state is not that empty must fall, but rather that it is able to fall21:48
ZipCPUConsider line 169 here:
tpbTitle: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - (at
ZipCPUThat proves that it is possible to empty the FIFO after it has been full21:49
tntyes, possible.21:51
tntbut I was more thinking of the case where you push 1 single word and empty stays asserted for instance.21:52
ZipCPUYou mean, verify that after pushing a word empty falls?21:52
tntbut not at the next cycle ... pipeline delays could make it happens 1,2,3,... cycles later.21:53
tnt(not in this implementation obviously but in general for a fifo)21:53
*** Jybz has quit IRC21:55
ZipCPUSo ... consider that the crossbar I've been working on is similar21:58
ZipCPURequests can be made by any of the bus masters, and then forwarded to the slaves21:58
ZipCPUIn the middle, there are a couple of stages of pipeline processing ... waiting for an channel grant, and a couple of skid buffers21:59
ZipCPUI can verify that the slave has the right counts (ignoring the interconnect), and I can verify that the master does21:59
ZipCPUTo handle the interconnect, I assume a functioning slave and a functioning master, and then have to prove that they are each driven properly22:00
ZipCPUThat 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 task22:00
tntheh, yeah, that's a couple of difficulty notch above :p22:02
ZipCPUIt's not really all that much more difficult than managing a bunch of counters22:06
tntZipCPU: anyway, time to sleep.  Thanks for your help !22:15
ZipCPU;)  Sleep well22:15
*** vonnieda has quit IRC22:43
*** emeb has quit IRC23:19

Generated by 2.13.1 by Marius Gedminas - find it at!