danieljabailey has quit [Quit: ZNC 1.6.4+deb1 - http://znc.in]
danieljabailey has joined #yosys
sklv has quit [Quit: quit]
Marex_ is now known as Marex
<promach>
awygle: Sorry to interrupt, I am not sure how you manage with 17 minutes using yices, I am still at could not finish BMC after hours
ekiwi has quit [Quit: ekiwi]
<awygle>
promach: that is interesting. What are the specs for the machine you're using? Processor and RAM specifically
<promach>
intel i7, 8GB RAM
<promach>
awygle
<promach>
i7 6th generation
<promach>
I suppose it is decent enough
<ZipCPU>
Hey, this is cool ... I just learned something new (and very useful) regarding yosys-smtbmc
<cr1901_modern>
That it's the source of all meaning to life?
<ZipCPU>
The problem I've been having is that I might have two different modules calculating the exact same logic.
<ZipCPU>
However, typically, nothing forces the logic state associated with these (identical) flip flops to be the same.
<ZipCPU>
So, for example, you count bus transactions in both your own module as well as a formal checker module.
<ZipCPU>
Both counts are based upon the same logic.
<ZipCPU>
They should be simplified into just that --- the same logic.
<ZipCPU>
"opt -share_all" does that.
<ZipCPU>
I was just using "opt" in my .ys file. I think I'm going to switch everything to "opt -share_all" for any formal logic proofs from here on out.
<cr1901_modern>
Well, I guess that's semi-comparable to finding the meaning of life
<ZipCPU>
Yes, but this was prime. The meaning of life is compound.
<awygle>
promach: i have an i7 4k and 16GB of ram so shouldn't be tooooo different. let me set up and then perform a really stupid experiment...
<cr1901_modern>
ZipCPU: Fair enough :P
stoopkid_ has joined #yosys
<awygle>
promach: so i'm running in a linux vm with nothing else in it but yosys, yices, and your UART module. it has 2 CPUs and 8GB of RAM. it's been running for 10 minutes and it's at step 4133. how does this compare to your experience?
<promach>
awygle: yes, it is quite similar. I remembered BMC i still at timestep #7400 even after 42 minutes
<promach>
is* still
<promach>
awygle: seems like the main difference is that you are running non-linux OS with extra RAM
<awygle>
promach: i suppose so. i don't seem to be maxing RAM on the VM, so i guess it's the OS more than anything
<promach>
strange
<awygle>
indeed
<ZipCPU>
promach: What O/S are you using?
<promach>
currently, it is Arch Linux
<awygle>
removing the --dump-debug and the -g makes it run _much_ faster btw - i would reconsider if you really need those
<promach>
is that is what you are asking
<promach>
if*
<promach>
awygle: -g is necesary
<ZipCPU>
I run -g only after the process completes successfully without it.
<promach>
ZipCPU: after ? I do not get it
<ZipCPU>
I tend to run yosys-smtbmc three times. First for BMC, then for induction, then with -g only after the first two have passed.
<ZipCPU>
The -g isn't necessary for proving that the module works, but it is worth while to see what happened when it does work.
<promach>
ZipCPU: thanks for the tips
<promach>
awygle: removing -g makes BMC finishes in 1 minutes and 40 seconds
<awygle>
promach: i got 2:42 so that seems reasonable
<ZipCPU>
Compared with ... 42 minutes?
<promach>
:)
<awygle>
so help me out here - the BMC needs to run for at least as long as it takes the induction to succeed, right?
<awygle>
i.e. if induction succeeds in 20 steps, you need a BMC run of >= 20 steps?
<ZipCPU>
Sounds good so far.
<awygle>
well in this case the induction is called for 110 steps, and succeeds _immediately_
<awygle>
so either a) there's something wrong with the asserts, or b) we should only need to run BMC for like, two timesteps. right?
<promach>
I am still not quite sure if 20010 timesteps are enough
<promach>
for BMC
<ZipCPU>
For your baud generator, 20010 timesteps should be enough.
<awygle>
i'll just say that when i accidentally ran "prove" with symbiyosys for 20 steps, it returned PASSED. so unless i'm way off, either there's something wrong with the asserts or 20010 steps is many more than necessary.
<ZipCPU>
promach: For your complete Tx ... I'd suggest at least 5x that.
<ZipCPU>
awygle: Yeah but ... if you are testing an operation/interaction that takes N clocks to complete, I'd recommend 2N+6 or so time steps minimum.
<awygle>
ZipCPU: why though?
<awygle>
if the rule is (induction passes) && (bmc passes) && (bmc steps >= induction steps), and that criterion is satisfied, why 2N+6?
<ZipCPU>
Well .... you want the formal prover to at least search the space of your entire operation, don't you? And if that takes N clocks, that'd be 2N time steps, plus one or two clocks to set the operation up.
<ZipCPU>
Why? Because BMC hasn't had enough steps to match your operation (yet).
<awygle>
in that case, there's something wrong with the criterion
<ZipCPU>
Am I misguided here?
<awygle>
one of us is
<ZipCPU>
;D
<ZipCPU>
Wouldn't be the first time ...... for me that is.
<awygle>
there's a logical contradiction here, which can be resolved by either changing our criterion for "proved correct", or by deciding that we don't need to run nearly that many steps
<ZipCPU>
Well ... if you have an N-clock operation, it will take BMC at least 2N time steps to prove that it takes place correctly, right?
<ZipCPU>
That I think we should agree upon, no?
<awygle>
let me review some slides and then come back to this conversation in about 5 minutes
<awygle>
okay. i'm fairly sure that what you're saying is correct, iff we are _only_ using BMC.
<awygle>
BMC proves "within k cycles, i cannot reach a bad state" (presumably by exhaustive search of the state space)
<awygle>
the induction step says "a sequence of k non-bad states will always be followed by another non-bad state"
<awygle>
when you combine that induction step with BMC, you get "the first k reachable states are always non-bad, and any k consecutive non-bad states are always followed by another non-bad state, therefore all reachable states are non-bad"
<awygle>
so the whole point of using the induction step is that we don't need to exhaustively search the state space
<ZipCPU>
Yeah, I get what you are saying there. Makes sense.
<awygle>
now i'll admit the induction step feels... pretty magic to me, so it's hard to trust that if i get PASS in three steps of induction, i'll be good to go with a 3-step BMC. but assuming that the induction is done correctly, it should be so
<ZipCPU>
Ok, with a touch of work, I managed to *prove* that the ZipCPU's basic memory module works (once adjusted)
<ZipCPU>
As before, I found some subtle errors in a module that I thought was working. ;)
<awygle>
hmm, interesting. if i have a clock (assigned by clk = clk === 1'b0) in my testbench, neither z3 nor yices will have anything to do with it
<ZipCPU>
Ahm ... did you use an assert or an assume at all? Do parens help? clk = (clk == 1'b0); ?
<awygle>
i suspect i'm missing an assert or something, yes... currently i have none as every input is valid and outputs are asserted in the module under test
<awygle>
i do have parens, i just didn't want to deal with nested parens in irc :P
<ZipCPU>
always @($global_clock) begin assume(i_clk == !f_last_clk); f_last_clk <= i_clk; end
<awygle>
i'm not sure i understand what the result of that will be
<awygle>
i don't think it will cause i_clk to actually toggle, will it? or if it does, it will do so at the rate of $global_clock?
<ZipCPU>
Sure will.
<ZipCPU>
On each $global_clock step, i_clk will change.
<ZipCPU>
You may need the most recent version of yosys ...
<awygle>
huh, interesting. i had to combine both elements to get the result i wanted (which was something that would run under both "smtbmc z3" and "abc pdr")
<awygle>
always @($global_clock) begin assume(clk ==!f_last_clk); f_last_clk <= clk; clk <= (clk === 1'b0); end
<ZipCPU>
Ahm ... if the clock is coming in from the outside world, then you want to be careful to only make assumptions about it ... not to set it.
<awygle>
this is my testbench, it is the Source Of All Clocks
<awygle>
but duly noted
<ZipCPU>
Yeah, heheh, ahm .... I haven't been successful separating the formal properties from my code (yet).
<awygle>
i decided rather than messing around with `define ASSUME assert i'd just always prove modules from a larger testbench
<awygle>
that way the modules can be integrated without modification into a larger system which is itself formally proven
<ZipCPU>
Hmm, yeah ... but ...
<ZipCPU>
What about this module: module test(i_clk, i_wr, i_val, o_match); always @(posedge i_clk) if (i_wr) r_val <= i_val; assign o_match = (r_val == ); endmodule
<ZipCPU>
You'd never manage to handle that from an external test bench, 'cause you'd have no insight into what the internal r_val variable is.
<ZipCPU>
It can start up, w/in the induction engine, in *any* state.
<ZipCPU>
Create two test modules, just like that, with the same inputs, and try to verify that the o_match outputs of each will be identical.
<ZipCPU>
Tell me how that works out for you.
<awygle>
is that last line supposed to include (r_val == i_val)?
<ZipCPU>
It was supposed to be (r_val == 0), but I think I like your proposed (r_val == i_val) better.
<awygle>
it's a level detector i guess at that point
<awygle>
am i allowed a reset signal?
<ZipCPU>
Sure ... but it will make no difference to the induction engine--only to BMC.
<awygle>
mk, let's give it a try... after i feed the cats. i'll report back
<rqou>
wait wait wait awygle you have cats?
<rqou>
i demand cat pix
<awygle>
2x kittens (well, oldish kittens), as of about two weeks ago
<rqou>
<3 cats
<rqou>
i demand cat pictures
<rqou>
:P
proteus-guy has joined #yosys
<promach>
sorry to interrupt, but temporal induction does not support -g , right ?
<awygle>
read that as "the thing i'm responding to is very true"
<awygle>
ZipCPU: so i'm looking at this again and i'm confused. you want me to instantiate two copies of the module and prove they output the same value? rather than prove some correctness property about the module itself?
<ZipCPU>
awygle: Perhaps some background might help.
<ZipCPU>
I've been working on "proving" some bus translators.
<ZipCPU>
A formal bus description includes within it something like: You can't receive a bus acknowledgement if there isn't an outstanding request.
<ZipCPU>
Hence, the formal bus verification module needs to keep track of the number of outstanding requests.
<ZipCPU>
In a bus translator, you have two of these formal verification modules: one for the master, one for the slave.
<ZipCPU>
Each has a number within it. The two numbers *should* be identical, but the induction step doesn't know that. (BMC does)
<ZipCPU>
So induction may start with these two values being something different ... and all chaos results.
<ZipCPU>
If during your N steps of induction, nothing forces these two values to be equal .... you'll never get there.
<ZipCPU>
The example I gave you above may have been too primitive. But the one I just described should help to make the concept (and difficulty) clear.
<awygle>
I understand your motivation better now, but I feel that should be a solvable problem. It's difficult to say for sure without a fully realized example. Let me finish this trivial example and then we can discuss how/if it applies to that situation
<ZipCPU>
That's actually a very useful example to study as well ...
<ZipCPU>
besides being one of my examples of why placing the formal verification code in an external model has ... some problems associated with it.
aw- has quit [Quit: Leaving.]
proteus-guy has joined #yosys
eduardo__ has joined #yosys
eduardo_ has quit [Ping timeout: 248 seconds]
promach has joined #yosys
<awygle>
ZipCPU: and what properties are you trying to prove in this example?
<awygle>
(also note that pipe[N-1] is never used)
<ZipCPU>
I wish to mrove that sub1 and sub2 are identical, and will produce identical outputs.
<ZipCPU>
*prove
<ZipCPU>
That's a type. 'b' should be equal to pipe[N-1].
<awygle>
Oh I see, I missed top.v
<ZipCPU>
*typo
* ZipCPU
might need another cup of caffeine this morning ....
<awygle>
I haven't actually left bed yet so same :-P
<ZipCPU>
At issue is the fact that there is "hidden" information between sub1 and sub2, and that this hidden information won't be revealed for an as yet unspecified number of clock cycles.
<awygle>
I
<ZipCPU>
The problem with the example I gave last night was that the "hidden information" was revealed immediately--hence it worked quickly for you.
<awygle>
It seems to me that the issue is that the modules are under specified. In this case, and last night's, the reset behavior. In the case of the bus translator, in how the error cases should be handled (what if you _do_ get an ack with nothing outstanding?)
<awygle>
I wouldn't be surprised if this took N induction cycles to prove btw. But I still think I can prove it from the test bench if reset is added to the module.
<ZipCPU>
Sure, N cycles would prove it .... until I placed an external 'ce' line onto each pipe step.
<awygle>
I'll trade you a ce line for a rst line
<ZipCPU>
Sorry, the design already has a reset line--it's just labeled "r" ... but ;) anyway.
<awygle>
So it does ;-) all right well I'll add a ce and then try to prove it. Probably this evening as I have a job which I should do at some point.
<awygle>
Enjoying the discussion!
<ZipCPU>
Check the gist.
<ZipCPU>
I just added the CE.
<awygle>
Copy
<shapr>
Paste
<ZipCPU>
Cut!
* shapr
exits the stage
<ZipCPU>
initial assert(places);
<awygle>
tomorrow && tomorrow && tomorrow
<ZipCPU>
assert((!married)||(!love));
m_t has joined #yosys
pie_ has quit [Ping timeout: 260 seconds]
digshadow has quit [Ping timeout: 258 seconds]
mbuf has quit [Quit: Leaving]
pie_ has joined #yosys
pie_ has quit [Ping timeout: 260 seconds]
digshadow has joined #yosys
fouric has joined #yosys
cr1901_modern has quit [Read error: Connection reset by peer]
cr1901_modern has joined #yosys
digshadow has quit [Ping timeout: 260 seconds]
dys has joined #yosys
juri_ has quit [Ping timeout: 252 seconds]
juri_ has joined #yosys
m_w has quit [Quit: leaving]
m_w has joined #yosys
pie_ has joined #yosys
swick has quit [Ping timeout: 246 seconds]
lok[m] has quit [Ping timeout: 246 seconds]
marbler has quit [Ping timeout: 276 seconds]
pointfree1 has quit [Ping timeout: 264 seconds]
enick_598 has quit [Ping timeout: 246 seconds]
aynah[m] has quit [Ping timeout: 255 seconds]
pie_ has quit [Ping timeout: 248 seconds]
nrossi has quit [Quit: Connection closed for inactivity]
m_t has quit [Quit: Leaving]
_whitelogger has joined #yosys
MatrixTraveler[m has joined #yosys
digshadow has joined #yosys
m_w has quit [Quit: Leaving]
gnufan has quit [Quit: Leaving.]
<awygle>
Can symbiyosys take an .sby file from stdin?
<ZipCPU>
awygle: No.
<ZipCPU>
The source for SymbiYosys is *really* simple, though. If I just new Python I could add it ... ;)
<awygle>
Yeah I was just answering my own question. I wish it used argparse, but I will probably make a PR.
<awygle>
I'd like to add support for Yosys formal in FuseSoC and that seems like the easiest way
<awygle>
The rightest way would be to refactor symbiyosys so it can be used as a proper python module but that sounds like work :-P
MatrixTraveler[m has quit [Write error: Connection reset by peer]
<ZipCPU>
Hey this is cool .... I'm finally writing up a blog post on the results of formally verifying a wishbone bus master!