Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.arch.embedded > #30632

Re: (Semi-) formal methods

Show all headers | View raw

On 5/15/2021 12:44 AM, HT-Lab wrote:
> On 14/05/2021 20:37, Don Y wrote:
>> 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.
>>
> 
> It became a must have tool about 2-3 decades ago for the safety critical/ 
> avionics/medical industries.

But these are industries with inherently high levels of overhead -- possibly
suggesting (market) "efficiency" (in other industries) as a reason that
discourages adoption.

So, if it/they have value *there*, why aren't it/they embraced EVERYWHERE?
Obviously, other product offerings in other industries face similar design
problems...

> Design where becoming so complex that simulation 
> could no longer answers questions like, is dead-lock or life-lock possible on 
> our statemachine, can you buffers overflow, do you have arithmetic overflow, 
> deadcode, race condition etc. The tools are now well established and most of 
> the above questions can be answered (with some user constraints) by a simple 
> push button tool. They are still expensive (you won't get much change from 20K 
> UK pounds) but most high-end FPGA/ASIC companies use them. They are not a 
> replacement for simulation but one of the tools you need to complete your 
> verification.
> 
> Regards,
> Hans
> www.ht-lab.com
> 
> 
>> [Just because a tool "makes sense" -- logically or economically -- doesn't
>> mean it will be adopted, much less *embraced*!]
> 

Back to comp.arch.embedded | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

(Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-11 18:25 -0700
  Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-13 15:25 +0100
    Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-13 11:57 -0700
      Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-14 10:43 +0100
        Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 12:37 -0700
          Re: (Semi-) formal methods HT-Lab <hans64@htminuslab.com> - 2021-05-15 08:44 +0100
            Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 02:48 -0700
          Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-15 12:02 +0100
            Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 15:07 -0700
  Re: (Semi-) formal methods Dave Nadler <drn@nadler.com> - 2021-05-13 19:32 -0400
    Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-13 16:57 -0700
    Re: (Semi-) formal methods Paul Rubin <no.email@nospam.invalid> - 2021-05-14 12:22 -0700
  Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 21:55 -0700
  Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 21:52 -0700
    Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 18:14 +1000
      Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 02:10 -0700
        Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 20:54 +1000
          Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 12:26 -0700
            Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-16 11:41 +1000
              Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-16 00:35 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-02 12:03 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-01 22:23 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-02 22:39 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-02 09:01 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-03 11:54 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-03 01:56 -0700
  Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 14:15 +1000

csiph-web