clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
dxld has joined #yosys
digshadow has quit [Quit: Leaving.]
<promach> ZipCPU: do you place your assertion within the design source code itself ?
<ZipCPU> Yes. It seems to work best there.
<ZipCPU> That allows you to assert not only the outputs, but also information regarding the internal state.
<promach> I am starting to formally verify my UART receiver, do you have comments before I start designing the assert() and assume() and cover() ?
<ZipCPU> Formally prove your transmitter first ... its easier, and you'll learn a lot.
* ZipCPU hasn't formally proven his UART receiver yet
<promach> ok
<ZipCPU> See ... the receiver has some difficult parts to it when "proving" it.
<ZipCPU> For example, just what "speed" do you pick for the simulated transmitter that you'll be proving your receiver against?
<ZipCPU> Is the speed absolute, or is there any fuzziness about where the incoming bit changes?
<promach> cover() should help, at least from what I read
<cr1901_modern> I have no idea what cover does, tbh
<cr1901_modern> Mainly b/c I didn't bother to read up on it ;P
<ZipCPU> cr1901_modern: I haven't needed it (yet).
<ZipCPU> Today's success: Formally proving not only my WB -> AXI bridge, but also an Avalon -> WB bridge.
<cr1901_modern> I've been in a rut most of the week, tbh
<cr1901_modern> (surprise surprise)
<ZipCPU> In hind sight, I'm glad I proved my ZipCPU prefetches first. They created a nice build-up to proving a full-blow bus bridge.
<ZipCPU> I mean, part of the difficulty in a bridge is ... just how long do you anticipate giving the downstream bus to respond?
<ZipCPU> cr1901_modern: I'm not allowed to be in a rut. Someone wants to sponsor some of this work ... so, I'll have to provide *some* kind of result. ;)
<cr1901_modern> Lucky you... While I have a few clients, I can't seem to find more
<ZipCPU> In this case, being active on-line was the key to finding this particular client.
<cr1901_modern> Well yes. That's how I've found my clients too. It hasn't helped lately to find _new_ ones. Only keep current ones
<cr1901_modern> Which I mean, is fine. Until it isn't.
<ZipCPU> cr1901_modern: I should mention ... I haven't made the changes you recommended to how I describe formal induction.
<ZipCPU> I'm just still ... struggling to understand exactly how it works, and the description I gave is how I understand it -- misguided though it may be.
<ZipCPU> All that's to say ... I'm still thinking over your description.
<cr1901_modern> ZipCPU: Asking about this topic on MathOverflow is on my todo list
<cr1901_modern> I.e. "reconciling temporal induction w/ the definition of mathematical induction"
<ZipCPU> Let me know when you get an answer. I'd love to read it myself.
* kuldeep fpga dev board is on they way!
<kuldeep> *the
<ZipCPU> o/
<cr1901_modern> ZipCPU: Will do
<thoughtpolice> Well, I think it depends on what you define "mathematical induction" as. Do you think of it as "Induction on the natural numbers"? That's a kind of induction, but it isn't really what induction *is*. I'm sure this seems like nitpicking (i.e. "wikipedia says it's over the natural numbers!") but it's rather important. Temporal induction and "natural induction" are both more specific cases of a more general technique, concerning
<thoughtpolice> relations between sets.
<thoughtpolice> "Mathematical induction" is typically just a case where the "sets" are naturals and the "relation" is something like "less than". Temporal induction is where the sets are "states" and the "relation" is "transitions to" (much in the way states in any automaton are 'related' by if they transition to one another)
<cr1901_modern> thoughtpolice: This is why I like logs: https://irclog.whitequark.org/yosys/2017-10-19#1508451688-1508451688;
<cr1901_modern> thoughtpolice: And your explanation is fine, I would still like a formal definition to sink my teeth into
<cr1901_modern> not the wordy version I attempt to explain in the linked logs
<thoughtpolice> "Well founded relations" are essentially the formal version of what I said. https://en.wikipedia.org/wiki/Well-founded_relation -- so if you're looking for sort of the "common ancestor" between them, that's a good place to start.
<thoughtpolice> Another example is theorem provers or whatever, where you also tend to do 'structural induction' -- it's like the generalization of induction to lists, or trees or other recursive data types, where your 'base case' is the 'empty list' and the inductive case is "if P(L), and M is a prefix list of L, then P(M)", i.e. you recurse down the list, eventually hitting a base case, and proving it for all cases. (That's a way you prove
<thoughtpolice> a program always terminates, for example.)
* cr1901_modern doesn't know how to use a theorem prover, just an SMT solver
<thoughtpolice> Most of them aren't very easy to use anyway. :)
<cr1901_modern> I've noticed...
m_w has quit [Quit: leaving]
m_w has joined #yosys
<sorear> i'm the other way around
<sorear> take: what induction is is transfinite induction
<thoughtpolice> My functional programming experience is leaking, clearly. (I think in general we sit closer to abstractions such as well-founded-ness)
<thoughtpolice> Or at least pedagogically, we do.
<awygle> sorear: i don't think you get to define induction using the word induction...
<ravenexp> you just need to prove the base case
<awygle> so i'm playing with yosys a bit, i wrote myself a boring gray code counter with an asynchronous reset. when i try to synthesize with yosys -S gray.v, i get "ERROR: Async reset \rst_i yields non-constant value 8'mmmmmmmm for signal \count."
<awygle> within my reset clause i have "count <= {SIZE{1'b0}};", so it really should just be 0. am i missing something? does yosys have issues with async resets?
* cr1901_modern has no idea :(
<awygle> i've heard of x, and z, but never m
digshadow has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
mbuf has joined #yosys
<cr1901_modern> clifford: Is "if $condition begin assert($assertion) end" equivalent to "assert property ($condition |-> $assertion)" in the general case?
<cr1901_modern> nevermind, forget that q. It's opening a can of worms I'm not prepared to yet
dys has quit [Ping timeout: 240 seconds]
nrossi has joined #yosys
<cr1901_modern> Does anyone know the simulation/synthesis semantics for an empty begin/end block in Verilog? At the very least, is it legal?
dys has joined #yosys
leviathanch has joined #yosys
mbock has joined #yosys
leviathanch has quit [Read error: Connection reset by peer]
proteusguy has joined #yosys
kerel has quit [Quit: http://quassel-irc.org - Chat comfortably. Anywhere.]
kerel has joined #yosys
kerel has quit [Quit: http://quassel-irc.org - Chat comfortably. Anywhere.]
kerel has joined #yosys
befedo has joined #yosys
pie_ has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
pie_ has joined #yosys
m_t has joined #yosys
mbuf has quit [Quit: Leaving]
pie_ has quit [Ping timeout: 264 seconds]
<promach> is it true that yosys-smtbmc does not support non-overlapping operator |=> yet ?
kristianpaul has quit [Quit: Lost terminal]
kristianpaul has joined #yosys
<ZipCPU> promach: Doesn't (A |=> B) mean the same as if ($past(A)) assert(B); ?
pie_ has joined #yosys
<promach> For a simple PISO shift register, what have I done wrong with https://gist.github.com/anonymous/1f9aa44394238150c40c874feb60af1f#file-shift_register-v-L26-L28 ?
pie_ has quit [Ping timeout: 240 seconds]
leviathanch has joined #yosys
<ZipCPU> promach: Try always @(*) assert (valid & !data_out);
<ZipCPU> Although ... your code will still break.
<ZipCPU> Look at the VCD file.
<ZipCPU> promach: Are you struggling to learn how to work with the yosys-smtbmc flow? The error you are getting *should* lead you directly to the problem you are having.
<promach> ## 0 0:00:00 Solver: z3
<promach> ## 0 0:00:00 Checking asserts in step 0..
<promach> ## 0 0:00:00 Assert failed in Tx_top.PISO: ../rtl/shift_register.v:28
<promach> ## 0 0:00:00 BMC failed!
<promach> ## 0 0:00:00 Writing trace to VCD file: Tx.vcd
<promach> ## 0 0:00:00 Status: FAILED (!)
<promach> ZipCPU
<ZipCPU> Ok, so ... look at shift_register.v line 28, and look at the VCD file.
<ZipCPU> What does it tell you?
<promach> I have already done assume on lines 26 and 27
<promach> so it should not fail
<ZipCPU> No?
<ZipCPU> What about the example given in your VCD file showing you inputs that would cause your design to fail.
<ZipCPU> Further, you are "assume"ing an ouput on line 27. That's wrong. Assume inputs, assert outputs.
<promach> hmm... line 27 is now removed, yet same error
<ZipCPU> Of course! Have you looked at the VCD file?
<promach> yeah
<ZipCPU> What's it tell you? You should see a trace that violates line 28.
<promach> data_out equals 1 in the vcd waveform
<ZipCPU> And ... ? Is valid true?
<promach> valid equals 0
<ZipCPU> So ... remember, the checker is going to try *ALL* input combinations that it can in order to see if it can cause one of your assumptions to be violated.
<ZipCPU> If valid equals 0, the assertion in line 28 will then fail.
<ZipCPU> So ... anytime the checker can make vaild = 0, it can cause your design to fail.
<ZipCPU> All you've said about valid is that it will start at zero. Wait, oops, that means that even in the initial conditions the assertion on line 28 will fail.
<promach> what about line 26 ?
<ZipCPU> All line 26 states is that valid will be initially equal to zero.
<ZipCPU> Line 26, though, contradicts your property in line 28, which asserts that both valid and !data_out will be true on the same clock.
<ZipCPU> Even this isn't what you want, since data_out will only ever be zero (as a result of valid) on the next clock based upon lines 21-23.
dys has quit [Ping timeout: 255 seconds]
jophish has quit [Ping timeout: 240 seconds]
jophish has joined #yosys
<shapr> jophish: hi!
<shapr> jophish: how's the log treating you?
pie_ has joined #yosys
SMDhome has quit [Ping timeout: 255 seconds]
m_w has quit [Ping timeout: 255 seconds]
m_w has joined #yosys
mbock has quit [Quit: Leaving.]
SMDhome has joined #yosys
proteusguy has quit [Ping timeout: 240 seconds]
proteusguy has joined #yosys
<promach> ZipcPU: but I have line 27
digshadow has quit [Ping timeout: 252 seconds]
<ZipCPU> The initial assume(data_out == 1) line?
<ZipCPU> Thought you had commented that out.
<ZipCPU> So ... if valid = 0, then (valid & !data_out) = 0 regardless of what data_out equals.
dys has joined #yosys
adityaP has joined #yosys
befedo has quit [Quit: befedo]
digshadow has joined #yosys
befedo has joined #yosys
ZipCPU|Laptop has quit [Ping timeout: 252 seconds]
ZipCPU|Laptop has joined #yosys
clifford has quit [Remote host closed the connection]
dys has quit [Ping timeout: 248 seconds]
leviathanch has quit [Remote host closed the connection]
m_t has quit [Quit: Leaving]
adityaP has quit [Quit: Connection closed for inactivity]
dys has joined #yosys
nrossi has quit [Quit: Connection closed for inactivity]
digshadow has quit [Ping timeout: 240 seconds]
uelenbot has quit [Quit: No Ping reply in 180 seconds.]
waylon531 has joined #yosys
digshadow has joined #yosys
befedo has quit [Quit: befedo]
ZipCPU|Laptop has quit [Ping timeout: 248 seconds]