azonenberg_work has quit [Ping timeout: 272 seconds]
azonenberg_work has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
seldridge has quit [Ping timeout: 272 seconds]
azonenberg_work has quit [Ping timeout: 252 seconds]
rohitksingh has joined #yosys
rohitksingh has quit [Remote host closed the connection]
rohitksingh has joined #yosys
azonenberg_work has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 245 seconds]
rohitksingh has joined #yosys
digshadow has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
<sensille>
ZipCPU: now you finally got me to take a peek into formal verification :)
<sensille>
and it's completely different from what i assumed
emeb_mac has quit [Ping timeout: 272 seconds]
rohitksingh has quit [Quit: Leaving.]
GuzTech has joined #yosys
rohitksingh has joined #yosys
fsasm has joined #yosys
rohitksingh has quit [Quit: Leaving.]
dys has quit [Ping timeout: 252 seconds]
digshadow has quit [Ping timeout: 245 seconds]
X-Scale has quit [Ping timeout: 244 seconds]
[X-Scale] has joined #yosys
[X-Scale] is now known as X-Scale
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
knielsen has joined #yosys
rohitksingh has quit [Quit: Leaving.]
<ZipCPU>
sensille: Really? How's that?
<sensille>
the latter?
<sensille>
the former just happened, i don't know how :)
<sensille>
i imagined formal validation as being something similar as to what i learned at uni
<ZipCPU>
Go on, how do you find it to be different?
<sensille>
building a formal model of what i want to achieve, and prove that the implementation is identical
<ZipCPU>
that was your university experience?
<sensille>
but writing tons of asserts is something i'm very used to and will gladly do while writing verilog :)
<ZipCPU>
So, not necessarily proving the design as a whole works, but creating assertions to prove that assumptions you are making as you write your code are actually valid?
<sensille>
i had a course on "formal verification of programming languages", and even took an exam on it, which i barely passed. it was horrible. i never wanted to look at that ever again
<sensille>
yes
<sensille>
i've read three of your blog posts on 'formal' now, but don't see yet how to prove the whole design with it. you only prove what you _think_ is the whole design, or am i missing something?
<sensille>
but i definitely need to play with it, looks easy enough to integrate and makes simulation a ton easier
<sensille>
not needing to provoke every state by external stimulation
<ZipCPU>
I'm not sure how you would formally verify C/C++, or any other language for that matter. I know some folks have worked on it, but I think I might struggle with that concept.
<ZipCPU>
Formally verifying Verilog code is much easier!
<ZipCPU>
sensille: Start by proving a "module", not the whole design. Then work through your whole design "module" by module.
<ZipCPU>
Start at the leaves.
<ZipCPU>
Only later aggregate items together.
<ZipCPU>
Be aware, there are problems with aggregation. The first of these you will encounter are the assumptions made in the leaf modules.
<ZipCPU>
If S is a Submodule of P the parent, then when formally verifying P any assumptions within S may limit the formal verification of P.
<sensille>
i've seen your ASSUME-macro
<ZipCPU>
Does this mean you understand why I use it then?
<sensille>
yes
<ZipCPU>
Ok, then you should understand most of the difficulties there.
<ZipCPU>
If you are just learning, then I'd suggest you start with your leaf modules, and only after verifying those would I recommend moving on to aggregated proofs.
<sensille>
yes. i have a fifo, too, could start with that :)
<ZipCPU>
It's certainly where I started.
<sensille>
but even only asserting wher i'm most unsure can already help a ton
<ZipCPU>
A new believer is born!! :D
<sensille>
as i've learned: "if it's not asserted, it's not true"
<sensille>
i'm a big fan of assert in C-code
<ZipCPU>
You will enjoy working with the tools then.
<ZipCPU>
Assert's in formal work much nicer than those in C
<sensille>
but you can never sure your formal verification is complete, or can you?
<sensille>
+be
<ZipCPU>
I think you can be.
<ZipCPU>
I've shown several examples on the blog of things I think are complete.
<sensille>
you have to formally prove it :)
<ZipCPU>
Well, yeah
<sensille>
the proof is a lie ;)
<ZipCPU>
? How so?
<ZipCPU>
I must be missing something ... what is a lie?
<ZipCPU>
In formal verification, you create a series of assertions and (possibly) assumptions. The formal tools will prove that given your code and the assumptions, the assertions then hold.
<sensille>
sorry, nothing specific. it's just that in all my time in university i never really learned to believe in proofs
<ZipCPU>
Ahh ... you need to try this.
<ZipCPU>
You'll learn that the tools do a better job than you do ... or at least that's what I've learned.
<sensille>
yeah, i see the value immediately
<ZipCPU>
I've never had a time where an assertion proved via formal was rendered invalid in practice unless the assumptions were somehow not met.
<sensille>
i had several cases where the assert (in C) i wrote was just plain wrong
<ZipCPU>
Of course, when using yosys you also get a trace (VCD file) showing "how" the assert is wrong ...
<sensille>
so i'm in no way doubting the value of that method, it's just that i don't think you can ever be 100% sure
<ZipCPU>
My problem has never been that the proof was invalid. More often, I just haven't asserted enough behavioral properties
<ZipCPU>
For example, I formally verified a data cache. Upon request for an item not in the cache, it would go fetch a cache line and return the item. Upon a write, it would write through the cache to the memory. All was good, and looked good.
<ZipCPU>
I was so pleased I ran the design using Verilator.
<ZipCPU>
Then I found the one thing I missed ... I missed proving that the design would come back to its reset/idle state following a read. It's not that the designs formal properties weren't valid, they were.
<ZipCPU>
The problem was ... I missed asserting something that needed to be said.
<ZipCPU>
In another problem, I created an avalon -> WB bridge. I verified this bridge, but somehow made an assumption about the input.
<sensille>
that's my point exactly
<ZipCPU>
In practice, whenever I tried writing a value to the bridge, the bridge locked up the whole board hard.
<ZipCPU>
A cover statement later pointed out my bug
<ZipCPU>
Hence, I now like to cover all interesting cases through the code.
maikmerten has joined #yosys
fsasm has quit [Ping timeout: 246 seconds]
seldridge has joined #yosys
<awygle>
Yeah this is something I had to make peace with too. What you really want to do is prove correctness under some specification and asserts feel like an indirection on the specification rather than the spec itself
seldridge has quit [Ping timeout: 244 seconds]
<ZipCPU>
awygle: 75 hrs and still going
<ZipCPU>
I simplified the problem. In the simplified problem, it's been going for 36 hrs, 33 since reaching induction step 2
<sensille>
awygle: i'm totally fine with that approach, but i have some trouble with the term 'formal verification'
<ZipCPU>
This butterfly is proving itself to be a challenge to prove.
<shapr>
ZipCPU: what's the bottleneck? CPU? IO?
<shapr>
ram?
<ZipCPU>
One machine has 32GB of RAM. The algorithm is using about 2.1GB, so RAM isn't the bottleneck.
<ZipCPU>
I don't think IO is the bottleneck either.
<shapr>
oh
<shapr>
is the prover single threaded?
<ZipCPU>
I think the problem is that there's a multiply within the butterfly, and that's what's hard to prove.
<shapr>
are you using all the cores?
<ZipCPU>
I tried using a multithreaded solver (suprove). That one ran out of memory and failed.
<ZipCPU>
The proof is only using two cores: one for induction, one for BMC
<ZipCPU>
So ... I tried to simplify the multiply to a simple 3-bit multiply. It's still struggling. :|
<ZipCPU>
Formal methods have particular problems with multiplies. Multiplies and encryption.
<shapr>
ran out of memory?!
<shapr>
hrm
<ZipCPU>
The multicore proof? Yes.
<shapr>
are you using symbiosys?
<ZipCPU>
Yes.
<shapr>
I'm tempted to fire it up on my laptop
<shapr>
symbiosys is C++, yeah?
<ZipCPU>
No
<ZipCPU>
SymbiYosys is Python.
<ZipCPU>
It's a fairly basic script that calls a "solver"
GuzTech has quit [Quit: Leaving]
<ZipCPU>
Several solvers are available: abc pdr, smtbmc yices, smtbmc boolector, smtbmc z3, aiger avy, aiger suprove, etc.
<ZipCPU>
The solvers tend to be written in C or other higher level language.
<sorear>
what properties are you trying to prove about multiplies and encryption?
emeb has joined #yosys
<ZipCPU>
sorear: I'm not trying to prove anything about encryption. I'm trying to formally verify a decimation in frequency FFT butterfly. Just one single butterfly.
<ZipCPU>
Since there's a logic multiply within it, of my own construction, the butterfly has become difficult to verify.
<sorear>
I’m still curious what properties you’re verifying of the butterfly
<ZipCPU>
Here it is in sum: This butterfly is supposed to calculate y0 = x0 + x1, and y1 = x0 - coef * x1. I'm trying to prove a series of properties based upon coef
<ZipCPU>
For example, if coef = 0, then y1 should be x0. If coef = 1, then y1 should be x0-x1. If coef = -1, then y1 should be x0+x1
<ZipCPU>
I'm sticking with +/- 1 or zero multiplication properties, since the multiplication is already "known" to work.
<awygle>
I wonder if you can cap suprove at 16gb
<ZipCPU>
The computer where suprove failed has 32GB on it.
<awygle>
Sure but, margin
<awygle>
Gotta let other stuff run
<awygle>
(also I gotta get me one of these 32gb workstations)
<awygle>
ZipCPU: so are you going to add UL support to icestorm? ;)
<ZipCPU>
Me??
<awygle>
well clearly somebody has to
<awygle>
The People Have Spoken. or a Person anyway
<ZipCPU>
No. No one has spoken. No one has spoken until there are dollars applied to the problem. :D
<ZipCPU>
Even if there were dollars applied, I wouldn't be the most likely person to work on it.
<awygle>
something something money is speech something something 'merica
<awygle>
something something campaign finance reform something something get mad quit the internet for the day
<ZipCPU>
?? I didn't get that.
<awygle>
it's not important lol
<sensille>
money?
<ZipCPU>
The SymbiYosys has taken and is taking a lot of money to get it going and to fuel its support.
<ZipCPU>
NextPNR is no different.
seldridge has joined #yosys
seldridge has quit [Ping timeout: 252 seconds]
<awygle>
money! it's a gas
<qu1j0t3>
share it fairly but don't take a slice of my pie
<qu1j0t3>
don't give me that do-goody-good bull-shit
<awygle>
where were you when we had our Rush confusion the other week? :p
<qu1j0t3>
i know zero Rush :)
rohitksingh has joined #yosys
<awygle>
you're missing out
rohitksingh has quit [Ping timeout: 252 seconds]
GuzTech has joined #yosys
seldridge has joined #yosys
dys has joined #yosys
xdeller has quit [Remote host closed the connection]
xdeller has joined #yosys
emeb has quit [Quit: Leaving.]
emeb_mac has joined #yosys
dxld has quit [Quit: Bye]
dxld has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
dxld has quit [Quit: Bye]
dxld has joined #yosys
maikmerten has quit [Remote host closed the connection]