pie__ has quit [Remote host closed the connection]
pie__ has joined #yosys
m_t has quit [Quit: Leaving]
dys has quit [Ping timeout: 252 seconds]
<awygle>
an open question to the channel - is there any way in which it makes sense to "prove" a synchronizer circuit?
<awygle>
a 2ff or 3ff synchronizer?
Exaeta-mobile has joined #yosys
Exaeta-mobile2 has quit [Ping timeout: 245 seconds]
<ZipCPU>
sorear: Regarding a CPU where it isn't clear whether or not a compiler might be built for it ... consider the Hive CPU on OpenCores.
<ZipCPU>
I remember asking the author of it whether or not it would even be possible to build a compiler for it.
<ZipCPU>
As I recall, its a barrell processor containing a bunch of stack register sets. My question: how do you make certain you never overflow any of the register sets, and what do you do when that happens.
<ZipCPU>
awygle: Good question. I can't think of any.
<ZipCPU>
Clifford and I have discussed adding metastability detection /processing to yosys-smtbmc, but as I recall it hasn't moved forward for a lack of a clear way of doing it.
<awygle>
ZipCPU: me either. i thought i'd come up with something but then i realized that the best i could hope for would be to prove it _didn't_ work
<awygle>
a 2ff synchronizer is fundamentally an abdication of formal correctness in favor of a more achievable probabilistic correctness
<ZipCPU>
You might be more successful proving that a word synchronizer, using 2ff or 3ff flag synchronization, worked.
<awygle>
right, we assume a 2ff or 3ff works as expected, and from that we can prove additional primitives
<ZipCPU>
Yeah, pretty much.
<ZipCPU>
You could do neat things with gray codes, though ... such as proving that no more than one bit ever changed at a time when crossing clock domains.
<awygle>
right, or that a signal was valid for ... what is it, 1.5 clocks? 3 clocks? and therefore isn't missed
<ZipCPU>
Yes.
<ZipCPU>
I've thought about proving that an async FIFO works via formal. Perhaps taking Cliff Cumming's async FIFO and proving many of the properties he declares are true using formal methods.
<awygle>
i would love to do that. perhaps i will someday.
<awygle>
i'd like to do a full library of synchronization primitives, ideally
<ZipCPU>
So far, I have all the synchronization primitives I've needed--save for that asynchronous FIFO.
<ZipCPU>
They're all posted on line, although most are buried within the projects that use them.
<awygle>
sure. but i'd like to prove them correct (under their operating conditions). also, re-impementing something is sometimes the best way to be sure you understand it :)
<awygle>
always a tension between that and wanting to make forward progress, of course
<ZipCPU>
So ... I've got three fun proofs within the formal course to be done as exercises: one is a proof of a clock gate, another is a proof of a clock switch, and the third is the proof of an input SERDES modules.
<ZipCPU>
Each submits nicely to yosys-smtbmc.
jophish_ has joined #yosys
jophish_ has quit [Client Quit]
<awygle>
that does sound interesting
<ZipCPU>
Would you believe I found all of the basic designs online via Google? I just didn't find any of the proofs on line.
<ZipCPU>
They only take about 20-50 lines or so.
<ZipCPU>
They make for really nice student exercises even.
jophish_ has joined #yosys
jophish_ has quit [Client Quit]
jophish_ has joined #yosys
cemerick has joined #yosys
jophish_ has quit [Client Quit]
jophish_ has joined #yosys
digshadow has quit [Ping timeout: 240 seconds]
AlexDaniel has joined #yosys
jophish_ has quit [Remote host closed the connection]
cemerick_ has joined #yosys
digshadow has joined #yosys
cemerick has quit [Ping timeout: 240 seconds]
<esden>
but I need to spend more time with your code first :D
<esden>
ups sorry wrong channel
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 252 seconds]
promach has joined #yosys
<awygle>
argh. my proof is failing (which i expect) but afaict the assert is not actually false.
<awygle>
in the alleged "counterexample" trace
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 240 seconds]
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 240 seconds]
<awygle>
bleh. brain fried. fix crazy problem tomorrow.
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 252 seconds]
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 245 seconds]
indy has quit [Read error: Connection reset by peer]
indy has joined #yosys
cemerick has quit [Ping timeout: 248 seconds]
davos has joined #yosys
leviathan has joined #yosys
GuzTech has joined #yosys
davos has quit [Remote host closed the connection]
sklv has quit [Ping timeout: 255 seconds]
ar3itrary has quit [*.net *.split]
sorear has quit [*.net *.split]
cfelton has quit [*.net *.split]
proteus-guy has quit [*.net *.split]
kristianpaul has quit [*.net *.split]
tmiw has quit [*.net *.split]
forrestv has quit [*.net *.split]
cfelton has joined #yosys
ar3itrary has joined #yosys
proteus-guy has joined #yosys
sorear has joined #yosys
kristianpaul has joined #yosys
tmiw has joined #yosys
forrestv has joined #yosys
leviathan has quit [Remote host closed the connection]
leviathan has joined #yosys
sklv has joined #yosys
forrestv has quit [Max SendQ exceeded]
forrestv has joined #yosys
leviathan has quit [Read error: Connection reset by peer]
leviathan has joined #yosys
m_t has joined #yosys
srk has quit [Ping timeout: 276 seconds]
srk has joined #yosys
srk has quit [Changing host]
srk has joined #yosys
<ZipCPU>
awygle: Had that problem. Check that you are processing the file you think you are. Also, I've been known to replace the contents of complex asserts with simple wires, just to make it easier to see if one has been violated.
m_t has quit [Quit: Leaving]
flagellum_ has joined #yosys
flagellum_ has quit [Quit: Page closed]
dys has joined #yosys
<awygle>
ZipCPU: thank you. Actually what is happening is that the assert is false, but it is inside an if statement which is also false.... I'll refactor to remove the if temporarily and see what that gets me
AlexDaniel has quit [Remote host closed the connection]
m_t has joined #yosys
<ZipCPU>
awygle: You know you can replace an "if (A) assert(B)" with assert((!A)||(B)); right? You might find that helps.
<ZipCPU>
Then make sure you have wires containing A and B that you can examine with a trace.
<ZipCPU>
Don't forget to make certain that the wires end up being *in* the trace. The Lord knows how many times I've ended up scratching my head wondering why a design was failing when I'd never rebuilt the SMT2 file.
clifford_ has quit [Read error: Connection reset by peer]
clifford_ has joined #yosys
TFKyle_ is now known as TFKyle
<awygle>
whaaaaaaat is happeninig. my whole assert statement is one line, _which is high_, and it's _still_ reporting failure in BMC
<awygle>
ohhhhhh okay i figured it out. i've had this problem before actually. when it displays the counterexample trace, the assertion failure is in the *previous* timestep.
<GuzTech>
awygle: Yes, apparently you have to check the previous time step when you get a counter example.
<GuzTech>
That's the least of the oddities (to me at least).
<awygle>
this is what i get for not doing any formal work since november
<awygle>
GuzTech: i'd be interested in reading an enumeration of the oddities as you perceive them
<awygle>
in the interests of "how can we make this better for all of us"
<GuzTech>
Well, for example, I've formally verified a stack I implemented. During that process I got counter examples where my input clock (i_clk) remains low even though my assertions are in clocked always blocks using i_clk.
<GuzTech>
Now, as I understand it, it uses $global_clock for the smt time steps.
<GuzTech>
But I was under the impression that an assert statement inside an always clocked block uses that clock when checking the assertion.
<ZipCPU>
Ok, so ... in the trace output ... always @(*) assert(A); will fail in the last clock cycle.
<ZipCPU>
always @(posedge i_clk) assert(A); will fail one cycle before the last cycle.
<ZipCPU>
GuzTech: Unless you place clk2fflogic in your yosys script file, the actual clock trace will be ignored.
<ZipCPU>
The current version of yosys on github does one better though ... it will create a "clock" signal the "looks" like the global clock signal. This works nicely for one clock designs.
<ZipCPU>
For 2+ clock designs, you *really* need to use clk2fflogic.
<GuzTech>
Oh so that's the reason? That probably explains why it *does* work in another design.
<ZipCPU>
Well ... perhaps not the reason but a better description of the symptoms ...
<awygle>
so always @(posedge clk) doesn't matter unless i have clk2fflogic? all properties are checked during $global_clock ticks?
<awygle>
that.. seems like some kind of spec violation
dmin7 has joined #yosys
<awygle>
on the plus side i just came up with a way to eliminate f_past_valid which always bothered me pedagogically
<ZipCPU>
If you only have one clock, and no clk2fflogic, then the always @(posedge clk) becomes an always at the next simulation step. It doesn't get evaluated until the next cycle--i.e. it waits for the positive edge of the clock for evaluation. This leads to the problem where the trace looks like its good at the last cycle, but failed on the cycle prior.
<ZipCPU>
awygle: Sure! How are you doing it?
* ZipCPU
is bothered by it too, but hasn't found a way around it .... (yet)
<GuzTech>
Well, I just added clk2fflogic, and now my assertions fail -_-
<GuzTech>
I take the part about the verified stack implementation back.
<ZipCPU>
If you add clk2fflogic, you then have to assume that the clock changes.
<ZipCPU>
always @($global_clock) assume(i_clk != $past(i_clk)); .... or some such.
<awygle>
ZipCPU: it occurred to me that it represented a failure of specification. the key insight was "none of these properties are guaranteed to hold until the core has been reset".
<awygle>
so i replaced f_past_valid with f_reset_in_past, a signal which asserts that, at some point in the past, the core has been reset
<GuzTech>
ZipCPU: is that why you have a f_last_clock that you force to toggle each clock cycle?
<ZipCPU>
awygle: Heheh! Yeah, I can see that one.
<ZipCPU>
GuzTech: Exactly!
<ZipCPU>
However, by removing clk2fflogic, I don't need that code anymore (usually)
<awygle>
next step - eliminate f_last_clk! which i think i might know how to do...
<ZipCPU>
GuzTech: I'm not reserving clk2fflogic for only those designs I have which use more than one clock.
<awygle>
or i can just delete it, that works too
<GuzTech>
Ok, from the manual: clk2fflogic - This command replaces clocked flip-flops with generic $ff cells that use the implicit global clock.
<GuzTech>
Well there you go.
<ZipCPU>
awygle: You only need f_last_clk if you aren't using clk2fflogic. Even then, you might be able to use $past(i_clk). Just be careful--the clock may start high or low depending on how you constrain it.
<ZipCPU>
;)
<awygle>
ZipCPU: so if i understand correctly, "always @(posedge clk)" desugars into "always @(*) begin; if ($rose(clk) begin;"?
* ZipCPU
isn't willing to go that far, not being that certain of the answer
Exaeta-mobile has quit [Read error: Connection reset by peer]
Exaeta-mobile has joined #yosys
<awygle>
okay, i understand :) am i _directionally_ correct?
<ZipCPU>
Ok, now that I'm thinking more about it, awygle: No. It's not equivalent to that.
<awygle>
(all models being wrong but some models being useful)
<ZipCPU>
If for no other reason then @(*) doesn't have a clock to reference in order to answer the $rose(clk) question.
<awygle>
mmm fair
<ZipCPU>
Further, always @(*) doesn't have the delayed by one assertion issue.
Exaeta-mobile2 has joined #yosys
Exaeta-mobile has quit [Ping timeout: 245 seconds]
<ZipCPU>
If you have multiple cover statements, you'll want to add a % to your VCD filename, as in: --dump-vcd file%.vcd
<awygle>
ah, i wasn't using -c
* awygle
runs off to find the symbiyosys equivalent
<ZipCPU>
You can also do always @(posedge i_clk) if (condition) cover(event); This is equivalent to a statement of cover((condition)&&(even));
<ZipCPU>
Symbiyosys is actually easier to use when it comes to cover. Just set the mode to "cover" and go.
<awygle>
very nice
<ZipCPU>
Another yosys command that is really useful is the chparam command. You may find that you want to formally prove things for simpler parameter values then you would actually use. Placing chparam in your yosys script will make that modification for you, keeping you from needing to adjust the default parameter values in your code.
<awygle>
hmm, that would be a good improvement for things like CI
<ZipCPU>
That will run BMC, induction, and then -g but soon to be replaced with cover ... all three in order.
<awygle>
and sby's code is super simple. maybe i'll see if i can add that.
<awygle>
but first, cats
<ZipCPU>
Actually, that makefile uses a lot of yosys-smtbmc -g commands. In practice, these seem to be fairly worthless. They need to be replaced with cover statements.
gnufan1 has joined #yosys
gnufan has quit [Read error: Connection reset by peer]
<awygle>
hm, the easy change _almost_ works but doesn't quite because we run into directory structure problems. maybe i'll get my proof to 100% and _then_ start hacking on sby
<awygle>
fun fact - if you specify two "mode" lines under [options] the last one wins
<awygle>
ZipCPU: have you used "live" mode in sby?
cemerick has joined #yosys
cemerick_ has joined #yosys
cemerick has quit [Ping timeout: 245 seconds]
leviathan has quit [Remote host closed the connection]
Exaeta-mobile has joined #yosys
sklv has quit [Ping timeout: 255 seconds]
Exaeta-mobile3 has joined #yosys
Exaeta-mobile2 has quit [Ping timeout: 245 seconds]
Exaeta-mobile2 has joined #yosys
Exaeta-mobile has quit [Read error: Connection reset by peer]
Exaeta-mobile3 has quit [Ping timeout: 245 seconds]
sklv has joined #yosys
Exaeta-mobile has joined #yosys
Exaeta-mobile3 has joined #yosys
Exaeta-mobile2 has quit [Read error: Connection reset by peer]
Exaeta-mobile has quit [Ping timeout: 245 seconds]
Exaeta-mobile has joined #yosys
Exaeta-mobile3 has quit [Ping timeout: 245 seconds]
cemerick_ has quit [Ping timeout: 240 seconds]
<sorear>
ZipCPU: I don't see anything particularly novel to compile for in Hive. within each function you can treat it as an 8-register RISC with all registers call-saved; use the free pushes and pops in the first and last basic block to combine save/restore with use; use an interprocedural register allocation pass to load-balance the register stacks and switch to memory stacks when they are exhausted/for recursive functions
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 252 seconds]
GuzTech has quit [Ping timeout: 252 seconds]
xrexeon has joined #yosys
Exaeta-mobile has quit [Ping timeout: 245 seconds]
Exaeta-mobile has joined #yosys
Exaeta-mobile2 has joined #yosys
Exaeta-mobile has quit [Ping timeout: 245 seconds]