<chatter>
to accept Islam say that i bear witness that there is no deity worthy of worship except Allah and Muhammad peace be upon him is his slave and messenger
chatter has quit [Client Quit]
scrts has joined ##openfpga
cr1901_modern has joined ##openfpga
Neuron1k has quit [Ping timeout: 245 seconds]
Neuron1k has joined ##openfpga
pie__ has joined ##openfpga
pie_ has quit [Ping timeout: 258 seconds]
<Lord_Nightmare>
does that guy keep switching IPs? bleh, he's been trolling channels all over
<cr1901_modern>
I like pie as well. Especially pumpkin or sweet potato pie.
Ardeshir has joined ##openfpga
Ardeshir has quit [Remote host closed the connection]
Ardeshir has joined ##openfpga
Ardeshir has quit [Remote host closed the connection]
Ardeshir has joined ##openfpga
Ardeshir has quit [Read error: Connection reset by peer]
Ardeshir has joined ##openfpga
digshadow has quit [Quit: Leaving.]
digshadow has joined ##openfpga
DocScrutinizer05 has quit [Disconnected by services]
DocScrutinizer05 has joined ##openfpga
<pie__>
cr1901_modern, :3
<pie__>
now i want some pastries :(
<jn__>
pie__: are you in $hometown again?
<pie__>
not yet
<pie__>
i leave tomorrow morning
<cr1901_modern>
Bit too late for me to have pastries tonight...
<jn__>
pie__: still in hamburg?
<pie__>
yea
<pie__>
you_
<jn__>
i'm going to leave hamburg today
<pie__>
i see
<azonenberg>
clifford: ping
<azonenberg>
Trying to figure out how to implement initialization values / ROMs in a yosys SMT problem
<azonenberg>
as a simple example, I have two memories that should never be written ("assume property !we")
<azonenberg>
the trace does not show any writes to them
<azonenberg>
they are initialized in the HDL to the same value
<azonenberg>
But they are reading different values in the counterexample
<azonenberg>
Which implies, to me, the solver isn't respecting INIT properties
<azonenberg>
I even tried a smtc file that said "initial assume (= [mem_lat0] [mem_lat1] )"
<azonenberg>
and i'm getting different read values
kuldeep__ has joined ##openfpga
kuldeep_ has quit [Ping timeout: 248 seconds]
Ardeshir has quit [Quit: Leaving]
<azonenberg>
clifford: Found a workaround where i added a combinatorial read port to the memory `ifdef FORMAL'd
<azonenberg>
and assumed the read output was the same
Tanfrieze has quit [Ping timeout: 264 seconds]
cr1901_modern has quit [Ping timeout: 252 seconds]
cr1901_modern has joined ##openfpga
<cr1901_modern>
Yay, crashed my system again, 'cept this time Windoze didn't even generate a dump file :/
<cr1901_modern>
So I have NO idea what the hell went wrong
pie__ has quit [Ping timeout: 248 seconds]
<azonenberg>
Welp
<azonenberg>
Proof is coming along and i definitely like the new verification tools in yosys
<azonenberg>
But there's a few things i'm making it assume
<azonenberg>
that i think should not be assumed
_whitelogger has joined ##openfpga
<cr1901_modern>
I've been trying to build LLVM for Windows. Want to take a guess how that's been going?
<azonenberg>
Super fun? :p
<cr1901_modern>
Well, I'm not nearly as angry as normal b/c it's going JUST as I expected it to go, so there's that :)
<cr1901_modern>
Let's see:
<cr1901_modern>
1. Clang can't be built on Windows without a Microsoft-internal switch now (big-obj)
<cr1901_modern>
2. This also means only 64-bit builds are supported now
<azonenberg>
Do people still use 32-bit OSes
<azonenberg>
for x86?
<azonenberg>
i'm legitimately curious
<cr1901_modern>
azonenberg: I default to 32-bit builds even on 64-bit
<cr1901_modern>
it's a preference
<cr1901_modern>
and it actually makes a difference in the case of LLVM
<cr1901_modern>
3. Some libraries take 30 MINUTES to link b/c binutils doesn't have facilities to speed up 64-bit Debug-enabled, Big-obj COFF builds like it does with ELF (gold)
<cr1901_modern>
4. I just found out that my binutils is too old (Before Jan 2016), b/c COFF big-obj support in binutils was broken until then
<cr1901_modern>
So yea, having a great fucking time :D
clifford has quit [Ping timeout: 260 seconds]
<cr1901_modern>
(On a 32-bit build, library links do not take extreme amounts of time. But of course they don't work, so no point in trying anymore)
<azonenberg>
how the heck do you spend 30 minutes linking a binary?
<azonenberg>
meanwhile i'm fighting yosys trying to get it to initialize some stuff in a SMT problem
<cr1901_modern>
Debug symbols
<azonenberg>
it's skipping all of my reset logic
<cr1901_modern>
Idk *why* it takes that long, I just know it has to do with debugging information
<cr1901_modern>
5 (BONUS!). I become very worried if your object file has more than 30,000 sections in it.
<cr1901_modern>
6. If I upgrade gcc now, will all my custom-compiled stuff not in repos, break due to the new libstdc++?
<cr1901_modern>
azonenberg: My sympathies :(
Tanfrieze has joined ##openfpga
_whitelogger has joined ##openfpga
<cr1901_modern>
Perhaps it's actually testing all states without regard to whether they are in fact reachable?
<azonenberg>
That makes it useless for verification
* cr1901_modern
shrugs and apologizes for that useless info
<azonenberg>
the whole point of the solver is to prove a given state can/can't occur given certain initial state
<azonenberg>
And it keeps putting me into states that are impossible
massi has joined ##openfpga
eduardo has joined ##openfpga
m_t has joined ##openfpga
<lain>
azonenberg: watch clifford's 33c3 talk
<lain>
it mentions this sort of thing
<azonenberg>
i went through his slides
* azonenberg
watches vid
<lain>
but yeah I dunno, I haven't quite wrapped my head around the concept
<azonenberg>
its just confusing because the solver isn't respecting my constraints as far as i ca ntell
<azonenberg>
like, i am trying to prove two versions of a module are identical
<azonenberg>
i.e. given the same inputs they produce the same outputs
<azonenberg>
but it's failing
<azonenberg>
because the memories inside the modules are initialized to different values by the solver
<azonenberg>
Do you think this is sufficient coverage for what's basically just a block ram? :p
<azonenberg>
Once i get this figured out, next step will be a fifo
<azonenberg>
(as well as Splash support since right now i'm running all these tests by hand)
<azonenberg>
I want to try and get full formal coverage of all of my core IP i rely on everywhere
pie_ has joined ##openfpga
cr1901_modern has quit [Ping timeout: 256 seconds]
<lain>
:)
<azonenberg>
Aaand it's coming up on 4 in the morning
* azonenberg
wonders if he should sleep
eduardo20 has joined ##openfpga
<pie_>
<azonenberg> Aaand it's coming up on 4 in the morning
<pie_>
>4in the morning
<pie_>
i know that feelingway too well
<pie_>
theres something very specific about 4 in the morning
<pie_>
not 2, not 5, but 4
<azonenberg>
lol
<pie_>
*not 3, not 5
<lain>
haha
<pie_>
and so lob the holy handgrenade at thine foe, etc
<qu1j0t3>
hahaha
<qu1j0t3>
that's what i was thinking of
clifford has joined ##openfpga
<clifford>
azonenberg, memory init values are supported. Can you send code?
pie_ has quit [Ping timeout: 265 seconds]
eduardo_ has joined ##openfpga
eduardo has quit [Ping timeout: 260 seconds]
eduardo20 is now known as eduardo
_whitelogger has joined ##openfpga
<pointfree>
Use the Net (from the .route file) as the signal name and ForceSignal to U(x,y,1)i
<pointfree>
e.g: ATTRIBUTE placement_force of Net_3:SIGNAL IS "U(0,0,A)0";
<pointfree>
After constraining your Nets to a different PLD, UDB your .route file will be larger but it will be constrained to your PLD, UDB of choice.
<clifford>
azonenberg, by its very nature, induction mode does not use initial constraints. it gives you a trace that starts with a seqence of N valid states (not forbidden by assertions) followed by a transition into an invalid state. If the N valid states are reachable, then you have a bug. If there are not reachable then you have to add an assertion to tell Yosys that they are not reachable.
<azonenberg>
clifford: So how can I tell the solver that the memories should all be the same at the start of the inductive step?
<clifford>
You cannot restrict the start of the induction step. That does not make any sense, since the first step of the induction step is a placehjolder for any reachable state.
<clifford>
If your memories should be the same in all reachable states, add an assertion.
<azonenberg>
How do i assert that memory in a child module should be the same as memory in another child module?
<azonenberg>
unclear on the syntax :)
Ardeshir has joined ##openfpga
<clifford>
See slide 31 (and memcmp.* in the example download).
<clifford>
You do it in an smtc file
<azonenberg>
huh i thought i tried that, maybe i did it wrong
<azonenberg>
Does this look like a correct use of constraints/assertions now?
Ardeshir has quit [Remote host closed the connection]
<azonenberg>
i'm basically trying to prove that OUT_REG is producing the desired number of cycles of latency and that the memory is indeed a dual port ram behaving as implied by the behavioral model at 219-230
<azonenberg>
The solver passes, just want to make sure i'm not doing something stupid
<clifford>
you will need the initial block otherwise the BMC will trivially fail because it decided to start with different memory contents
<azonenberg>
So a full proof will require both the induction and BMC?
<azonenberg>
the solver does not check the initial conditions?
<clifford>
yosys-smtbmc without -i proves the base case and with -i proves the induction step. induction without base case technically does not prove anything..
<azonenberg>
ah ok
<azonenberg>
so with -i does not prove the base case
<clifford>
yes
<azonenberg>
Why is that, out of curiosity?
<clifford>
it would take more time to also prove the base case
<azonenberg>
What i mean is
<azonenberg>
why would you ever want to run the inductive step
<azonenberg>
without proving the base first
<azonenberg>
since as you said it proves nothing
<azonenberg>
And any change to the RTL or constraints invalidates both
<clifford>
you wouldn't, but you might want to run BMC (base case) without proving induction
Ardeshir has joined ##openfpga
<clifford>
(e.g. if the base case already fails)
<azonenberg>
Yeah
<azonenberg>
So it seems to me the sane option would be to have either base only, or base+inductive
<azonenberg>
seems like allowing just the inductive step is a bit of a footgun?
<azonenberg>
I generally am a fan of interfaces that are hard to misuse
<clifford>
I usually run very deep BMCs (as deep as I can first), then I try induction. Simply because a deep base case couter example is worth much more than a counter example produced by induction, and running a deep BMC might give you confidence that the induction counter example is actually unreachable and thus help setting a direction for dealing with a failing induction step.
<azonenberg>
Interesting
<azonenberg>
Also, it looks like the -1 is not strictly necessary
<azonenberg>
but it massively speeds up the BMC
<azonenberg>
presumably by giving it some guidance as to what's impossible
<clifford>
The -1 just skips the assertion for the first time step.
<clifford>
Are you using z3 as solver?
<azonenberg>
Yes
<azonenberg>
It took 11 seconds with that block to do a 20-cycle BMC
<azonenberg>
Without, i got 13 steps in in 2 minutes before giving up and killin it
<clifford>
Try yices if you can. It's free for "non-commercial" use.
<clifford>
(I'm just using the pre-compiled binaries. I assume they know how to build their software.)
<azonenberg>
welp now that i have this figured out i have more code to write
<azonenberg>
and i have to work out build automation for some of this
<azonenberg>
so i dont have to manually run yosys and the solver separately each time i change a source file
<clifford>
Makefile? :)
<clifford>
btw: next project is "SymbiYosys" -- a single front-end for all yosys based formal verification flows. Will also support running many solvers in parallel and just use whatever result comes back first. Will hide base-case vs induction step complexity as well.
<cr1901_modern>
I'm still amazed that yosys' Makefile works as well as it does
<azonenberg>
Well i also want to do parallel runs of everything so i'll be integrating them in my existing parallel build system
<azonenberg>
since as far as i'm concerned formal verification is just one part of an overall build/test flow
<azonenberg>
i need to do synthesis and runs in actual hardware
<azonenberg>
simulation
<azonenberg>
and formal
<azonenberg>
any one module may be covered by one or all
<clifford>
interesting: for your code yices actually seems to be slower than z3. boolector however is about twice as fast as z3.
<clifford>
(this is the base case with "always -1")
Ardeshir has quit [Quit: Leaving]
<azonenberg>
clifford: interesting
<azonenberg>
I just pushed a constraint update
<azonenberg>
check out performance with just the initial vs the initial+always
<azonenberg>
how does yices act vs z3?
<azonenberg>
Also are you aware of any solvers (does yices do this?) that can run a single smt problem on multiple cores?
<clifford>
but whatever I do, I cannot reproduce the 2 minutes case.