How prevalent are (semi-) formal design methods employed? Which? [I don't have first-hand knowledge of *anyone* using them]
(Semi-) formal methods
Started by ●May 11, 2021
Reply by ●May 13, 20212021-05-13
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
Reply by ●May 13, 20212021-05-13
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?
Reply by ●May 13, 20212021-05-13
On 5/11/2021 9:25 PM, Don Y wrote:> How prevalent are (semi-) formal design methods employed?https://tinyurl.com/thbjw5j4
Reply by ●May 13, 20212021-05-13
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/thbjw5j4Hardly formal -- no cufflinks, watchfob, cumberbund nor tails! :>
Reply by ●May 14, 20212021-05-14
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
Reply by ●May 14, 20212021-05-14
Dave Nadler <drn@nadler.com> writes:>> How prevalent are (semi-) formal design methods employed? > https://tinyurl.com/thbjw5j4Wrong picture, try the one on this page: https://web.stanford.edu/~engler/ Look at the articles linked from there too ;-).
Reply by ●May 14, 20212021-05-14
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*!]
Reply by ●May 15, 20212021-05-15
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.
Reply by ●May 15, 20212021-05-15
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!)
