<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.
<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: 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>
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 ...
<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.
<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>
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…]