proteus-guy has quit [Remote host closed the connection]
seldridge has quit [Ping timeout: 255 seconds]
X-Scale has quit [Read error: Connection reset by peer]
dxld has quit [Quit: Bye]
dxld has joined #yosys
xerpi has joined #yosys
xerpi has quit [Remote host closed the connection]
xerpi has joined #yosys
leviathan has joined #yosys
leviathan has quit [Remote host closed the connection]
leviathan has joined #yosys
kraiskil has joined #yosys
pointfree1 has quit [Ping timeout: 260 seconds]
maartenBE has quit [Ping timeout: 240 seconds]
MatrixTraveler[m has quit [Ping timeout: 260 seconds]
maartenBE has joined #yosys
pointfree1 has joined #yosys
MatrixTraveler[m has joined #yosys
kraiskil has quit [Read error: Connection reset by peer]
kraiskil has joined #yosys
emeb_mac has quit [Quit: Leaving.]
kraiskil has quit [Read error: Connection reset by peer]
GuzTech has joined #yosys
proteus-guy has joined #yosys
fsasm has joined #yosys
luismarques has joined #yosys
proteus-guy has quit [Remote host closed the connection]
jwhitmore has joined #yosys
proteus-guy has joined #yosys
proteus-guy has quit [Read error: Connection reset by peer]
proteus-guy has joined #yosys
luismarques has quit [Quit: luismarques]
luismarques has joined #yosys
luismarques has quit [Client Quit]
luismarques has joined #yosys
pie__ has joined #yosys
pie_ has quit [Ping timeout: 260 seconds]
luismarques has quit [Quit: luismarques]
X-Scale has joined #yosys
xerpi has quit [Remote host closed the connection]
kraiskil has joined #yosys
nurelin has quit [Ping timeout: 276 seconds]
luismarques has joined #yosys
nurelin has joined #yosys
luismarques has quit [Quit: luismarques]
luismarques has joined #yosys
promach_ has joined #yosys
nurelin has quit [Ping timeout: 276 seconds]
luismarques has quit [Quit: luismarques]
nurelin has joined #yosys
kraiskil has quit [Ping timeout: 240 seconds]
seldridge has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
luismarques has joined #yosys
jwhitmore has quit [Ping timeout: 264 seconds]
jwhitmore has joined #yosys
seldridge has quit [Ping timeout: 248 seconds]
maikmerten has joined #yosys
GuzTech has quit [Quit: Leaving]
jwhitmore has quit [Ping timeout: 240 seconds]
zkrx has quit [Ping timeout: 256 seconds]
<maikmerten>
turns out I don't have a firm grasp of Verilog yet. A seemingly trivial testbench of mine gives very unexpected simulation results (simulation done in iverilog), although the synthesis result works just fine on a FPGA.
<maikmerten>
this is putting some predetermined input into the bus unit of my CPU design, waits until the bus unit finished operation (busy-signal goes low) and checks, if the proper values were read
* ZipCPU|Laptop
is working on formally verifying an FFT right now
<maikmerten>
no, sadly no formal verification :-(
<ZipCPU|Laptop>
Why not?
<ZipCPU|Laptop>
I formally verify all of my bus components.
<ZipCPU|Laptop>
The tools are free, and you find more bugs than with traditional test benches.
<maikmerten>
I guess a misguided lazyness on my part has for now prevented me looking into how to specify the constraints that formal verification check for
<ZipCPU|Laptop>
That part is already done and posted. You are using a wishbone interface, right?
<maikmerten>
yes, I'm using a silly perversion of Wishbone
<maikmerten>
(8 bit data bus, but 32 bit address... c'mon...)
<tpb>
Title: The ZipCPU by Gisselquist Technology (at zipcpu.com)
<maikmerten>
ZipCPU|Laptop, hey, cool, I've seen your site before. It actually triggered my move from Wishbone classic to pipelined operation
<ZipCPU|Laptop>
;)
<maikmerten>
I may be misunderstanding that article, though: It seems you're checking that the bus cycle itself is progressing as specified (e.g., that the bus components behave properly and that the bus, e.g., doesn't get stuck) - which is of course all that the Wishbone specification can specify
<maikmerten>
my testbench basically aims at gaining some confidence that the bus unit actually returns correct data
<ZipCPU|Laptop>
What is the unit under test?
<maikmerten>
of course, formal methods should be helpful here as well
<awygle>
well, it works fine in the fpga because this code isn't synthesizable lol
<maikmerten>
a bus unit, which on the "CPU side" is connected to the testbench (where I apply stimuli) - while on the "bus side" a 1KB RAM simulation with predetermined content is present
<srk>
ZipCPU|Laptop: that's pretty cool!
<awygle>
so whatever issue you have is a simulation issue
<maikmerten>
awygle, indeed
<ZipCPU|Laptop>
I ask because ... 1) I have several examples of formal properties and wishbone slave components, and 2) the value returned may be constrained by properties appropriate to the component
<maikmerten>
awygle, the waveform of the module under test in simulation actually matches what I want - it's just that the testbench checks the module's output at the "wrong time"
<ZipCPU|Laptop>
For example, three specific properties will constrain the proper functioning of any cache.
<awygle>
maikmerten: i think it's because you can't delay like this in initial blocks, you have to do it in an always block. i could be wrong though.
<maikmerten>
and I just can't figure out why the check in the testbench doesn't wait for the busy signal to go low before doing the check
<awygle>
what are you using for simulation?
<maikmerten>
(okay, that last sentence was completely broken)
<maikmerten>
iverilog
<awygle>
yeah, i think you want this to be a continuous check, so it probably wants to be always@(posedge clk)
<awygle>
or similar
<awygle>
but this is a pretty infrequently used corner of the language (at least by people around here). maybe try ##fpga?
<maikmerten>
thanks for your input!
<maikmerten>
I guess that the non-synthesizable part of Verilog indeed is out-of-scope for this particular corner of freenode ;-)
<awygle>
formal is always fun though! and ZipCPU|Laptop swears it's useful :p
<ZipCPU|Laptop>
LP
<ZipCPU|Laptop>
:P
<maikmerten>
oh, I'm pretty sure formal is very useful in a lot of cases!
<maikmerten>
Clifford likes formal verification as well, explaining the SAT-solver in yosys ;-)
<ZipCPU|Laptop>
Especially bus interactions ...
* ZipCPU|Laptop
uses Yosys for all of his formal verification work
<awygle>
yes of course, i'm just giving ZipCPU a hard time
* awygle
hopes to get back to his formal work... someday
<maikmerten>
yeah - bus interactions should be a wonderful target - because there usually are very neat specifications to check against ;-)
* awygle
passes around a hat labeled "pay me to do formal work"
<ZipCPU|Laptop>
Defn: formal shame, verb, to apply formal methods to someone else's design and prove that the design they thought was working still had many bugs within it. ;D
<maikmerten>
don't tell Intel or AMD ;-)
<awygle>
i'm currently looking at C code that locks a mutex, then immediately unlocks it, _then_ modifies a shared resource. lots of horrible things "work" :p
<maikmerten>
yummy.
* ZipCPU|Laptop
will pray for awygle
<awygle>
it's cool, my solution to this is permitted to be "rm -f"
<ZipCPU|Laptop>
Looks like I'll be able to formally verify a second stage of an FFT ... I already managed to prove the penultimate stage, this would be the last stage. (Neither require hardware accelerated multiplies)
<awygle>
nice!
<awygle>
somehow i feel like i could go backwards in the log and find you expressing doubt about the possibility of such a thing somewhere
<ZipCPU|Laptop>
I have doubt about the possibility of proving the general butterfly, and I have doubt about proving the entire thing together, but at this point ... this works so far.
<awygle>
have you done any experimenting with the more "advanced" (for lack of a better term) formal algorithms? beyond k-induction i mean
<ZipCPU|Laptop>
I've done a bunch of stuff with cover, although not with the liveness methods.
<ZipCPU|Laptop>
I've also used the concurrent assertions available in the commercial yosys version.
<awygle>
those are all very cool
<awygle>
but what i meant was things like "abc pdr"
<ZipCPU|Laptop>
I have used abc pdr.
<ZipCPU|Laptop>
The first proof of the entire ZipCPU was using abc pdr.
<awygle>
also the "aiger" solvers (avy and suprove, maybe others?)
<ZipCPU|Laptop>
Yes, I've tried several of those as well.
<awygle>
i find these particularly interesting as they seem to be more powerful, or at least differently powerful, than straightforward k-induction
<ZipCPU|Laptop>
My favorites are yices and boolector still. While I like abc pdr, if my design would fail then it never returns. On the other hand, if the design would succeed ... often abc pdr returns faster than other solvers.
<awygle>
c.f. your induction article
<awygle>
and, being a lazy sort, i am interested in anything that involves less fiddling around :p
<ZipCPU|Laptop>
Well ... you could be like Clifford and avoid induction entirely.
<awygle>
oh? what approach does clifford take?
<ZipCPU|Laptop>
He uses bmc almost exclusively. He and I seem to be quite different from that standpoint.
<ZipCPU|Laptop>
For me, it isn't a proof unless k-induction passes.
<ZipCPU|Laptop>
Although, mathematically, it is possible to prove a design with only BMC
<awygle>
hm. how? wouldn't you have to get into a provably repeating state?
<aiju>
17:25 < maikmerten> I guess that the non-synthesizable part of Verilog indeed is out-of-scope for this particular corner of freenode ;-)
<awygle>
or i guess exhaust the state space
<ZipCPU|Laptop>
Heheh ... Just tried "abc pdr" on the module I'm working on and it instantly passed. I'll still need to do more to get yices or boolector to pass.
<aiju>
i know this!
<maikmerten>
oh :)
<ZipCPU|Laptop>
awygle: All designs get into repeating states. At issue is how many states it takes to get there.
<awygle>
ZipCPU|Laptop: sure, but you have to prove that
<aiju>
maikmerten: it's a race condition
<maikmerten>
ewww
<maikmerten>
I hate those!
<ZipCPU|Laptop>
awygle: Not at all. Someone else did.
<aiju>
maikmerten: '=' in clocked logic is bad news
<awygle>
ZipCPU|Laptop: you don't have to prove that all designs repeat, you have to prove that you've reached a repeating state of your particular design
<awygle>
also isn't this equivalent to solving the halting problem? lol
<aiju>
maikmerten: each initial/always block is a process; @(posedge clk) just means "wait until the clock rises"
<ZipCPU|Laptop>
Ahh, no the paper had a different approach for that. They had a means of determining the maximum depth for any given problem. Apply BMC to that depth, and then you are guaranteed to be done.
<aiju>
maikmerten: '=' is an assgnment that updates the value immediately
<aiju>
so ti depends which two procsses run first :)
<aiju>
*which of the processes runs
<awygle>
ah. interesting.
<aiju>
oversimplifying a bit, <= assignments are delayed until the current timestep is over
<awygle>
i can see how that would be a nice simple brute-force way to do it
<aiju>
17:47 < awygle> also isn't this equivalent to solving the halting problem? lol
<aiju>
only for things that are turing complete :)
<aiju>
verilog designs have a finite state space
<awygle>
i suppose that's true. they're not rewriteable.
<ZipCPU|Laptop>
Especially for riscv-formal, where Clifford has been verifying multiple CPU's. He doesn't have the ability to dive into each individually and create enough properties to ensure they each pass induction.
<awygle>
until/unless we get a self-partially-reconfiguring FPGA :p
<srk>
ZipCPU|Laptop: what's your workflow like?
<ZipCPU|Laptop>
srk: How do you mean?
<srk>
I would like to learn more about formal verif. but the learning curve is steeeep
<ZipCPU|Laptop>
It's not that bad, but go on.
* ZipCPU|Laptop
does teach a course on the topic.
seldridge has joined #yosys
<srk>
ZipCPU|Laptop: well, when you work on a block what tools do you use for verification?
<ZipCPU|Laptop>
Ok, sure ... I'm working on a block of an FFT right now. I'm editing my design in GVIM, saving it, running SymbiYosys, and then examining the trace in gtkwave.
<aiju>
i bought a book on formal verification and it taught you how to use secret intel tools that you will never be able to get your hands on
<ZipCPU|Laptop>
Understand ... I came to formal after doing a lot of test bench work. When I found a bug in my first "working" design, I went around to see if I had bugs in others. Invariably, the answer was always "yes" I had bugs in them that I hadn't found.
<ZipCPU|Laptop>
Designing with formal methods is, IMHO, much easier than the alternative test bench method--you can go faster and be more sure of yourself along the way.
<srk>
I'm half-way thru, using ivory/tower and haskell to generate "better" C code for stm32s
<maikmerten>
aiju, I'm still at a loss of what happens there, though. To me it still appears that the check should take place after a negative edge of busy
<ZipCPU|Laptop>
Ok, the 2-point stage of the FFT now passes formal ... ;)
<ZipCPU|Laptop>
(The 4-point stage and the bit reverse already pass)
<aiju>
maikmerten: are you sure it's not running at time 0?
<aiju>
maikmerten: you could try adding a $display("%T"); to print the current time before the dataout check
<maikmerten>
oooooooooooh
<maikmerten>
that sounds plausible
<aiju>
maikmerten: x->0 is a negedge
<aiju>
maikmerten: @(negedge clk) will trigger on initial clk = 1'b0;
<tpb>
Title: ZipCPU toolchain and initial test (at zipcpu.com)
<ZipCPU|Laptop>
srk: Hopefully I'll have the formally verified build up and ready soon. I'm pretty close, although I just now got distracted by this FFT.
<srk>
are the course materials available possibly? :D
<ZipCPU|Laptop>
Every now and then I'll tweet a slide.
<ZipCPU|Laptop>
You might want to browse through the zipcpu.com/formal/formal.html posts. There's a lot of commonality between those and the courseware.
<srk>
thanks for these
<ZipCPU|Laptop>
My expectation is that the courseware will eventually be released publicly. Feedback from the students said that they wouldn't have understood the course from the slides alone though.
<ZipCPU|Laptop>
(I was hands on, over the shoulders of the students, quite often during the exercises--just to make sure they succeeded.)
<srk>
I'm out of uni for some years now so I'm ok with learning stuff by myself :)
<srk>
doable when you have good foundations and extremely rewarding as you learn stuff which you actually need / want
<ZipCPU|Laptop>
I've been out for ... 15 yrs now? Welcome to where learning is actually fun, and where you can learn what you want to learn.
<srk>
:D
<srk>
this!
promach_ has quit [Ping timeout: 256 seconds]
cr1901_modern has joined #yosys
cr1901_modern1 has joined #yosys
cr1901_modern has quit [Disconnected by services]
cr1901_modern1 has quit [Client Quit]
cr1901_modern has joined #yosys
<shapr>
anyone jumped on board with the NeTV2 for yosys purposes?