Forums

(Semi-) formal methods

Started by Don Y May 11, 2021
How prevalent are (semi-) formal design methods employed?
Which?

[I don't have first-hand knowledge of *anyone* using them]
Don Y <blockedofcourse@foo.invalid> wrote:
> How prevalent are (semi-) formal design methods employed? > Which?
We use theorem provers to find bugs in ISA specification: https://www.cl.cam.ac.uk/~pes20/sail/ They're quite handy for finding bugs before they hit silicon... Theo
On 5/13/2021 7:25 AM, Theo wrote:
> Don Y <blockedofcourse@foo.invalid> wrote: >> How prevalent are (semi-) formal design methods employed? >> Which? > > We use theorem provers to find bugs in ISA specification: > https://www.cl.cam.ac.uk/~pes20/sail/ > > They're quite handy for finding bugs before they hit silicon...
But, presumably, only of value if you're a SoC integrator? I.e., given COTS devices, what might they reveal to users of said devices?
On 5/11/2021 9:25 PM, Don Y wrote:
> How prevalent are (semi-) formal design methods employed?
https://tinyurl.com/thbjw5j4
On 5/13/2021 4:32 PM, Dave Nadler wrote:
> On 5/11/2021 9:25 PM, Don Y wrote: >> How prevalent are (semi-) formal design methods employed? > > https://tinyurl.com/thbjw5j4
Hardly formal -- no cufflinks, watchfob, cumberbund nor tails! :>
Don Y <blockedofcourse@foo.invalid> wrote:
> On 5/13/2021 7:25 AM, Theo wrote: > > Don Y <blockedofcourse@foo.invalid> wrote: > >> How prevalent are (semi-) formal design methods employed? > >> Which? > > > > We use theorem provers to find bugs in ISA specification: > > https://www.cl.cam.ac.uk/~pes20/sail/ > > > > They're quite handy for finding bugs before they hit silicon... > > But, presumably, only of value if you're a SoC integrator? > > I.e., given COTS devices, what might they reveal to users of > said devices?
They can reveal bugs in existing implementations - where they don't meet the spec and bad behaviour can result. However CPU and FPGA design is what we do so that's where we focus our efforts. Depends whether FPGA counts as COTS or not... Theo
Dave Nadler <drn@nadler.com> writes:
>> How prevalent are (semi-) formal design methods employed? > https://tinyurl.com/thbjw5j4
Wrong picture, try the one on this page: https://web.stanford.edu/~engler/ Look at the articles linked from there too ;-).
On 5/14/2021 2:43 AM, Theo wrote:
> Don Y <blockedofcourse@foo.invalid> wrote: >> On 5/13/2021 7:25 AM, Theo wrote: >>> Don Y <blockedofcourse@foo.invalid> wrote: >>>> How prevalent are (semi-) formal design methods employed? >>>> Which? >>> >>> We use theorem provers to find bugs in ISA specification: >>> https://www.cl.cam.ac.uk/~pes20/sail/ >>> >>> They're quite handy for finding bugs before they hit silicon... >> >> But, presumably, only of value if you're a SoC integrator? >> >> I.e., given COTS devices, what might they reveal to users of >> said devices? > > They can reveal bugs in existing implementations - where they don't meet the > spec and bad behaviour can result. > > However CPU and FPGA design is what we do so that's where we focus our > efforts. Depends whether FPGA counts as COTS or not...
Understood. Tools fit the application domains for which they were designed. How did *adoption* of the tool come to pass? Was it "mandated" by corporate policy? Something <someone> stumbled on, played with and then "pitched" to management/peers? Mandated by your industry? etc. [Just because a tool "makes sense" -- logically or economically -- doesn't mean it will be adopted, much less *embraced*!]
On 12/5/21 11:25 am, Don Y wrote:
> How prevalent are (semi-) formal design methods employed? > Which? > > [I don't have first-hand knowledge of *anyone* using them]
Don, IDK if you know about TLA+, but there is a growing community using it. It is specifically good at finding errors in protocol (== API) designs (because "TL" means "Temporal Logic"). I haven't used it so can't really answer many questions, but I have been following the mailing list for some time and greatly admire some of the excellent folk are are using it. <https://learntla.com/introduction/> Clifford Heath.
On 5/14/2021 9:15 PM, Clifford Heath wrote:
> On 12/5/21 11:25 am, Don Y wrote: >> How prevalent are (semi-) formal design methods employed? >> Which? >> >> [I don't have first-hand knowledge of *anyone* using them] > > Don, IDK if you know about TLA+, but there is a growing community using it. It > is specifically good at finding errors in protocol (== API) designs (because > "TL" means "Temporal Logic"). I haven't used it so can't really answer many > questions, but I have been following the mailing list for some time and greatly > admire some of the excellent folk are are using it.
My query was more intended to see how *commonplace* such approaches are. There are (and have been) many "great ideas" but, from my vantage point, I don't see much by way of *adoption*. (Note your own experience with TLA!) [The "(Semi-)" was an accommodation for *individuals* who may be using such things even though their work environment doesn't] So, you either conclude that the methods are all "hype" (not likely), *or*, there is some inherent resistance to their adoption. Price? (Process) overhead? NIH? Scale? Education? <shrug> [Note my followup question to Theo as to how *he/they* ended up with their tool/process] There seem to be many "lost opportunities" (?) for tools, techniques, processes, etc. I'm just curious as to *why* (or, why *not*). Or, said another way, what does a tool/process have to *do* in order to overcome this "resistance"? It's as if a (professional) writer wouldn't avail himself of a spell-checker... Or, a layout guy not running DRCs... (yes, I realize this to be an oversimplification; the examples I've given are just mouse clicks!)