To: ramu@com.mot.corp.cadsun
Cc: info-hol@edu.ucdavis.cs, Tom.Melham@uk.ac.cam.cl
Subject: Re: Query about testing
In-Reply-To: Your message of Mon, 20 Jan 92 10:06:56 -0600. <9201201606.AA17227@cadsun.corp.mot.com>
Date: Thu, 23 Jan 92 12:10:51 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.413:23.00.92.12.11.28"@cl.cam.ac.uk>


> What is the difference between formal verification and formal testing
> of specifications?  From a mathematical perspective, it looks the
> same.  However, there are probably some differences wrt completeness.

If I had to take a guess as to what "formal testing of specifications"
might mean, I'd say that:

   1) formal verification = proving that a mathematical model of
      the circuit design has some desired property ("satifies
      a specification"):

            |- model  ==>  requirement

   2) formal testing of specifications = deriving consequences from
      the specification of required behaviour for a device, in an
      attempt to convince yourself that the specification really
      expresses what you mean to device to do:

            |- specification  ==>  consequences

Tom