<cr1901_modern>
Tfw I want to read ZipCPU's blog post but I also _don't_ want to do it b/c I want to discover how to write a spec myself
<cr1901_modern>
but I also don't want to write a wb core
<cr1901_modern>
Ehhh, screw it, I skimmed it... looks like I had the right idea at least (bring out a bunch of helper signals that aid in formal verification)
<cr1901_modern>
I think the next design I'll do is a pipelined 16x16 unsigned multiplier
<cr1901_modern>
I can use it to test miform out
<awygle>
ZipCPU: where you were making your choices in areas where the spec was unclear, did you try to determine what common practice was?
<promach>
ZipCPU: For UART Rx, how much time you took for formal verification ?
<ZipCPU|Laptop>
awygle: Not really. Common practice is not to use WB/B4 pipeline. ;D
<ZipCPU|Laptop>
promach: Not a fair question. The post took weeks to put together. Formally verifying the cores didn't take nearly that long.
<ZipCPU|Laptop>
Of course ... everytime I found a bug in the formal_master.v file I had to re-verify everything again.
<awygle>
ZipCPU|Laptop: fair enough ;-)
<fouric>
ZipCPU|Laptop: holy cow
<fouric>
i don't recall there being quite so much stuff on your blog last time i checked
<ZipCPU|Laptop>
Heheh!
digshadow has quit [Quit: Leaving.]
<promach>
ZipCPU|Laptop: I mean computation time, not post preparation time
digshadow has joined #yosys
<promach>
by the way, I also wish to do wishbone coding after this
<ZipCPU|Laptop>
Ten minutes max.
<awygle>
ZipCPU is aggressively prolific :-P
<promach>
10 minutes max ? what ?
<promach>
huh /
<promach>
?
<ZipCPU|Laptop>
Yeah .... the proofs each took about 10mins max.
<promach>
strange, why mine is taking hours ?
<ZipCPU|Laptop>
All the code, and yosys configs, are all posted.
<promach>
no, I mean UART Rx
<ZipCPU|Laptop>
Well, for one, I didn't need more than about 80 steps or so.
<promach>
oh, you changed the baud rate to lower ones ?
<ZipCPU|Laptop>
No, I didn't post formal code for a UART.
<ZipCPU|Laptop>
Ahh ... my bad. I answered the wrong question.
<ZipCPU|Laptop>
Sorry.
<promach>
so, it is 10 minutes for UART Rx formal verification ?
jpo has quit [Ping timeout: 240 seconds]
<ZipCPU|Laptop>
promach: I thought you were talking about the WB post from today. My WB components only take about 10 mins each.
<promach>
I will get to WB after UART though
<ZipCPU|Laptop>
I have yet to do a formal proof of a UART--for precisely the reason you are puzzling through.
proteusguy has quit [Ping timeout: 240 seconds]
jpo has joined #yosys
<awygle>
Somebody go prove an I2C core :p
<ZipCPU|Laptop>
Shouldn't be all that hard.
<ZipCPU|Laptop>
I've got one that might be fun to prove ....
<awygle>
A fully blinged out multi master one
<awygle>
Supporting both standard and extended addresses etc
proteusguy has joined #yosys
<awygle>
(I do not like I2C)
<rqou>
not possible :P
<rqou>
i've yet to use an i2c core that had zero errata
<awygle>
It would be interesting if an attempt to prove an I2C core instead proved the protocol fundamentally unsound
<qu1j0t3>
> prover becomes depressed
<rqou>
i don't believe i2c is unsound
<rqou>
it doesn't have any fairness or liveness guarantees though
<rqou>
i really love (/s) this because shorted wires -> everything silently stops working
<awygle>
I don't either. At least not simple master-slaves. Jury is out on multi master
<awygle>
Thankfully barely used in practice
<rqou>
i've done it
<cr1901_modern>
awygle: While nobody likes I2C, it's becoming clear to me that all implementations of standards tend to obey de-facto, unsaid rules, instead of a real spec
<rqou>
it "worked" in the sense that it successfully exchanged data
<rqou>
this was before i understood ideas like fairness or liveness
<awygle>
I have too sadly
<awygle>
I worked on a project with MM I2C as the primary system bus.
oldtopman has quit [Ping timeout: 246 seconds]
<cr1901_modern>
what is fairness and liveness?
<rqou>
awygle: are you me? :P
<awygle>
cr1901_modern: any standard that doesn't have _both_ a formal spec _and_ a reference implementation is doomed to that fate
<awygle>
rqou: did yours go to space?
<rqou>
lol no
<ZipCPU|Laptop>
"barely used in practice" ... never used an HDMI monitor?
<rqou>
i believe that's not truly multi-master
<ZipCPU|Laptop>
well ... okay ... I can believe that.
<cr1901_modern>
What is fairness and liveness in the context of a bus like I2C?
<cr1901_modern>
*
<rqou>
can every master get a turn to send data?
<rqou>
will data manage to get through eventually?
proteusguy has quit [Ping timeout: 240 seconds]
oldtopman has joined #yosys
<cr1901_modern>
I don't see how one's different than the other, aside from "hardware failure so data never arrives at destination, but is actually sent"
<cr1901_modern>
but does a spec model that?
<ZipCPU|Laptop>
Preliminary versions of my I2C controller even managed to hang the bus ....
<rqou>
well, you can for example have a bus that says "transactions will be aborted after xxx duration, but the first to initiate a transaction gets the bus"
<rqou>
so it tries to guarantee liveness because stuck transactions will be aborted
proteusguy has joined #yosys
<rqou>
but one master can keep monopolizing the bus
<awygle>
Well, the second one went to space. The first one tried but caught Extremely Fire along the way.
<ZipCPU|Laptop>
Exactly ... I broke protocol with a broken controller and ... the monitor never reset. I had to reset the bus manually with hand-controlled GPIO.
<cr1901_modern>
"transactions will be aborted after xxx duration" So, start a new transaction with the same payload?
<cr1901_modern>
can every master get a turn to send data? <-- this is fairness?
<rqou>
well, you can have different fairness guarantees
<rqou>
e.g. "every master gets to send an equal amount of data (up to the limit of the bus)"
<cr1901_modern>
Doesn't that need a time frame to be a useful metric?
<rqou>
probably
<cr1901_modern>
Where can I learn more about liveness and fairness, b/c the wiki article doesn't seem to apply in this context
<awygle>
You don't even need a bad actor to break I2C. A fully conforming master can open a transaction and just never close it without ever breaking spec.
<rqou>
^ that too
<cr1901_modern>
rqou: Where did you learn about liveness/fairness?
<rqou>
mostly in the context of operating systems actually
<awygle>
And SMBus despite being better actually made everything worse because it looks similar enough that people get lazy/greedy and try to use the same core for both.
<cr1901_modern>
Thankfully digital hardware in practice is (mostly) just huge FSMs, so I could learn about liveness and _attempt_ to write my own yosys-smtbmc proofs. Badly.
<rqou>
yeah, FSMs are much more amenable to verification than giant software tangles :P
<rqou>
something something halting problem :P
<rqou>
cr1901_modern, awygle: troll suggestion: prove that FooBarEnterpriseApp and its giant mess of spring+hibernate+whatever-java-framework correctly records intern working hours :P :P
<cr1901_modern>
No.
<rqou>
where's the grumpy cat to go with the no?
<awygle>
Well they were grumpy but I just fed them so now they're just a little sullen.
<rqou>
lol
<cr1901_modern>
Probably too busy trying to eke more money out of ppl who like memes too much
<awygle>
/r/memeeconomy
<awygle>
Wait, wrong shitposting service
<pointfree>
What are the size limits of inputs to yosys?
<pointfree>
All switches on the same row of a PSoC5LP Horizontal Channel routing block form a product.
<pointfree>
All rows form a sum.
<pointfree>
This gives you a jumbo-sized logic expression describing the Horizontal Channel block.
<pointfree>
I'd like to compress this routing block by generating a blif or something and running yosys logic minimization on it.
<thoughtpolice>
cr1901_modern: There's really 3 things, safety, liveness, and fairness. Safety says "bad things don't happen" (ever). Liveness says "something good will happen" (eventually). Fairness is sort of like liveness in a sense, but it's easier to think of as it saying "Good things will keep happening" (forever, like "a scheduler will give every process a piece of time to run, and never has a 'stuck' case").
<pointfree>
synthesizing/mapping logic to the HC routing block would amount to taking parts of the HC routing block expression and minimizing that.
<thoughtpolice>
You'll probably find most of the literature on them regarding concurrent process theory/specification, e.g. "Proving Liveness of Concurrent Programs" by Lamport, for example https://lamport.azurewebsites.net/pubs/liveness.pdf
<pointfree>
(this is also how envision yosys logic synthesis to PSoC 5LP routing blocks would work)
<awygle>
pointfree: wow that is jumbo pretty sure abc could handle it tho. Give it a try I say
<cr1901_modern>
thoughtpolice: Ty... I was gonna look at that paper, but closed the search results before I clicked it :P
<awygle>
pointfree: would that basically describe the cell that Yosys would tech map onto for the psoc?
<thoughtpolice>
But most of the ideas are still applicable to hardware designs or whatnot if you just squint a bit. Safety and liveness in particular have a particularly neat relation in that "all properties are the intersection of a liveness property and a safety property".
<cr1901_modern>
I don't understand that last point
<cr1901_modern>
safety seems kinda impractical in practice? I mean, bad things _never_ happen? Of course they do! If I sneeze wrong for instance, a wire could come loose on my I2C bus. That's a "bad thing"
<thoughtpolice>
This is actually also closely related to the notion of topological spaces, where any topological space is in fact, an intersection of a 'dense set' and a 'closed set', but that's more of just a cool thing. The details on that are here: https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf
<awygle>
And now you have a basis for the space of properties and suddenly its linear algebra!
<awygle>
Lol thoughtpolice beat me to it
<cr1901_modern>
Saw the prefix "topolo-", and redirected to /dev/null, sorry :)
<cr1901_modern>
I can't bend my brain far enough to be able to grok it
<thoughtpolice>
cr1901_modern: Sure, but you don't prove "nobody will sneeze on the I2C" wire. That's not really it's job. It's not like when Intel says "Our chips do not catch fire", and you take a bunch of newspapers and shove them under your heatsink and it all catch fire, you say "I've proven you wrong!" I mean, I guess in the most technical sense you have, but it's not really a meaningful one.
<cr1901_modern>
thoughtpolice: What I meant in that context is that asserts are likely to fail if a wire is assumed to be bad
<cr1901_modern>
Maybe some redundant protocols can protect against that?
<cr1901_modern>
where if a wire goes down, the hardware can adjust
<rqou>
it's basically impossible on a shared medium like i2c
<rqou>
one node can always go "trolololol" and short out the bus
<thoughtpolice>
Sure, I could also operate every board 100C above its operating temperature. It's not about whether or not a meteorite can hit you or not, it's about the assumptions you have for the model you're working with. When you work with properties like this, you aren't working in a physical realm... you're working in an abstract one where a model tries to encapsulate precisely what you want.
<cr1901_modern>
Fair enough
<thoughtpolice>
And you try to say "Under every invariant of the model, this statement I'm going to make is true". That's really it.
<puddingpimp>
cr1901_modern: POWER8 and POWER9 do that on the Centaur interconnect between the CPU and memory controller IC
<cr1901_modern>
puddingpimp: Cool, I'll have to check that out when I have a chance
<puddingpimp>
the talk is on Hotchips, I can't remember what year
<rqou>
and of course, you never _have to_ verify all of these properties
<rqou>
you can decide what your design requires
<rqou>
you can e.g. say "i don't care if reading an unmapped address on the bus hangs the cpu forever"
<cr1901_modern>
I know, I was just thinking out loud
<thoughtpolice>
cr1901_modern: Also that paper is mostly not about topology, I think you can skip the last section. :) It actually formulates things like safety and liveness in terms of automaton and sets. It would probably go well after reading Lamport's paper, I think.
<puddingpimp>
also majority carry logic for radhard, I don't know if they try and prove the whole chip against SEU, or prove the building blocks and use correct by construction translation from a non-MCL design
<cr1901_modern>
Lots of implicit assumptions go out the window if you can't assume the hardware works
<cr1901_modern>
erm, the physics of the hardware works*
ekiwi has quit [Quit: ekiwi]
<cr1901_modern>
thoughtpolice: Cool. Now what do you mean by "all properties are the intersection of a liveness property and a safety property"?
<cr1901_modern>
all systemverilog properties* are the...?
<pointfree>
awygle: a small part. There's one of those big HC blocks between each pair of UDB's. The HV blocks combine all those HC blocks into one massive expression for the entire PSoC routing fabric.
<pointfree>
This means a graph of quantifiers (for-all/there-exists, aka AND/OR) over the variables in the UDB's PLD's. I don't think Cypress tools make use of the routing fabric for logic/quantifiers. Doing so can make expressions/logic configuration with exponential sizes very concise.
<pointfree>
The DSI (connecting to) the peripherals/gpios has the same structure so the quantifiers are also over the peripherals/gpios
<thoughtpolice>
cr1901_modern: You can sort of think of it as an SV property but that's not really the right level of thinking... It's more abstract. I strongly suggest at least skimming the first bit of the paper, sections 1 and 2 are enough, but IIRC it's something like this:
<cr1901_modern>
thoughtpolice: I plan to, just need to finish things tonight
<thoughtpolice>
You have a program X, which you think of as a sequence of states over time: state 1 -> state 2 -> state 3 .... Now, normally, you view some property about the program as logical property or predicate, like P(X), means "For all states, the internal counter does not go beyond 10", e.g. it's some kind of logical predicate or whatever. That paper gives you a way, instead, of viewing a property, a statement about a program, as a
<thoughtpolice>
"Buchi automaton", which is just another kind of finite state automata.
<thoughtpolice>
This automata can be decomposed into two different disjoint sets: one set specifies that certain program states "won't ever happen" (safety), and another set specifies that "certain states will eventually occur" (liveness)
<cr1901_modern>
Where does fairness come in?
<cr1901_modern>
certain states will eventually occur and keep occuring?
<thoughtpolice>
The notion of 'safety' and 'liveness' is also closely related to the notion of 'invariant' and 'well founded-ness', especially when you view programs as sequences of 'ascending' states. Invariants of a system are things that are always true -- and well-founded sets classify that "certain states will eventually be reached"
<rqou>
you probably don't need fairness unless you're doing some fancy space or whatever thing
<rqou>
a lot of real systems don't have fairness guarantees
<thoughtpolice>
Like before, a few weeks ago, when I mentioned "well founded" things being related to induction, that was the same idea, in a sense.
<cr1901_modern>
Yea, I still haven't gotten around to actually following up on that ._.
<cr1901_modern>
Saying "you don't need it" doesn't help me if I'm curious
<thoughtpolice>
But yes, if you're a supernerd, you can then go even further and take the topological view. (Which, again, which is really more of just a cool thing to noodle about)
<thoughtpolice>
(Now recently I read a paper connecting programming languages to Noether's theorem, which is all about system invariants. I wonder what the "concurrent process view" of Noether's theorem is :)
<thoughtpolice>
cr1901_modern: Also I don't actually know how fairness fits into this automaton story! Lamport's paper actually has the skivvy on fairness, but basically yes, "Certain states occur and will always keep occurring" is a good way of thinking of it
<thoughtpolice>
Like an OS scheduler, which is the classic example: every process that exists will always be 'scheduled', i.e. get some time slice, forever, as long as it exists. So nothing else can starve something out
<thoughtpolice>
(This statement of course sense nothing about relative sizes of the timeslices/quantums or whatever, but you could create a better model that did, I guess)
<thoughtpolice>
Lamport in particular has done of very good research about these kinds of problems, just in the domain of concurrent/distributed systems, and I find much of his work to be very approachable.
<cr1901_modern>
Fair... I just don't want to go down a rabbit hole when getting answers to my q's
<thoughtpolice>
At the very least, you could waste your time on far worse papers than the ones written by him, I suppose :)
ZipCPU|Laptop has quit [Ping timeout: 248 seconds]
<cr1901_modern>
lol nice
<qu1j0t3>
holy shit this changes everything
pie_ has joined #yosys
<awygle>
puddingpimp: the latter, usually
<awygle>
pointfree: I was assuming it wasn't the only such block :-)
<ZipCPU>
One thought to add regarding formal proofs and I2C. On each formal proof I've done, I've *assumed* the inputs, and *asserted* the outputs of the module I've worked with.
<ZipCPU>
Should any of the I2C input wires fail to act like one expects .... then all bets are off and who knows what might happen. The formal proof doesn't apply in those cases.
<awygle>
Right. Any proof is only under certain conditions.
<awygle>
That being said, it's often good to specify as many of the failure states as you can
<awygle>
As I think you've found in all of your published proofs to date
ZipCPU|Laptop has joined #yosys
digshadow has quit [Ping timeout: 240 seconds]
digshadow has joined #yosys
digshadow has quit [Ping timeout: 248 seconds]
proteus-guy has quit [Read error: Connection reset by peer]
digshadow has joined #yosys
mbuf has joined #yosys
proteus-guy has joined #yosys
aw- has joined #yosys
mbuf has quit [Remote host closed the connection]
mbuf has joined #yosys
nrossi has joined #yosys
leviathanch has joined #yosys
proteusguy has quit [Ping timeout: 240 seconds]
proteusguy has joined #yosys
AlexDaniel has quit [Ping timeout: 258 seconds]
aynah[m] has quit [*.net *.split]
indy has quit [*.net *.split]
FabM has quit [*.net *.split]
jhol has quit [*.net *.split]
LongHairedHacker has quit [*.net *.split]
brandonz has quit [*.net *.split]
kmehall has quit [*.net *.split]
marbler has quit [Ping timeout: 240 seconds]
swick has quit [Ping timeout: 255 seconds]
enick_803 has quit [Ping timeout: 250 seconds]
pointfree1 has quit [Ping timeout: 248 seconds]
MatrixTraveler[m has quit [Ping timeout: 255 seconds]
lok[m] has quit [Ping timeout: 255 seconds]
brandonz has joined #yosys
jhol has joined #yosys
indy has joined #yosys
FabM has joined #yosys
LongHairedHacker has joined #yosys
kmehall has joined #yosys
dys has quit [Ping timeout: 260 seconds]
dys has joined #yosys
aynah[m] has joined #yosys
leviathanch has quit [Remote host closed the connection]
FabM has quit [Ping timeout: 252 seconds]
pointfree1 has joined #yosys
marbler has joined #yosys
Guest89866 has joined #yosys
lok[m] has joined #yosys
swick has joined #yosys
AlexDaniel has joined #yosys
FabM has joined #yosys
AlexDaniel has quit [Read error: Connection reset by peer]
AlexDaniel has joined #yosys
AlexDaniel has quit [Ping timeout: 240 seconds]
sunxi_fan has quit [Read error: No route to host]
aw- has quit [Quit: Leaving.]
proteus-guy has quit [Ping timeout: 246 seconds]
sklv has quit [Ping timeout: 248 seconds]
pie_ has quit [Ping timeout: 248 seconds]
sklv has joined #yosys
proteus-guy has joined #yosys
leviathanch has joined #yosys
AlexDaniel has joined #yosys
Guest73474 has joined #yosys
_whitelogger has quit [Ping timeout: 250 seconds]
juri_ has quit [Ping timeout: 250 seconds]
_whitelogger has joined #yosys
Guest73474 has quit [Remote host closed the connection]
sklv has quit [*.net *.split]
gnufan has joined #yosys
sklv has joined #yosys
AlexDaniel has quit [Ping timeout: 240 seconds]
mbuf has quit [Quit: Leaving]
m_t has joined #yosys
FabM has quit [Quit: ChatZilla 0.9.93 [Firefox 52.3.0/20170811091919]]
digshadow has quit [Ping timeout: 250 seconds]
pie_ has joined #yosys
digshadow has joined #yosys
AlexDaniel has joined #yosys
AlexDani` has joined #yosys
AlexDaniel has quit [Ping timeout: 240 seconds]
AlexDani` is now known as AlexDaniel
leviathanch has quit [Remote host closed the connection]
nrossi has quit [Quit: Connection closed for inactivity]