Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <2017.9411211041@frogland.inmos.co.uk>
Subject: Re: FWD: The Pentium chip wasn't verified
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Mon, 21 Nov 1994 10:41:50 +0000 (GMT)
In-Reply-To: <199411210920.AA23298@borneo.gmd.de> from "Matthew Morley" at Nov 21, 94 10:20:20 am
Content-Type: text
Content-Length: 3337

Matthew Morley has said:
> -By the way, I heard that BDD's breaks down when verifying multipliers.
> 
> Yes, they break down and cry when they can't find a good variable
> ordering. There is a proof that no good variable ordering exists for
> such circuits. 
> 
> Conjecture #1. No good BDD variable ordering exists for circuits
> having multiplier sub-circuits.
> 
> Conjecture #2. BDDs break down almost always!
> 
> -Does this mean that theorem proving has a good chance of beating
> -model checking in the area of verifying multiplication and division
> -circuits?
> 
> It's interesting to here on the one hand the theorem provers opine
> that model checking's no good in general as "it only handles diddy
> circuits", and model checkers, on the other, opine that theorem
> proving's no good as "it's just too inefficient".

Yes, as someone who's used both theorem proving and currently model
checking they both have advantages and disadvantages.

Model checking can handle things a lot bigger than "diddy circuits" -
for example, we're currently using model checking on models translated
directly from the VHDL source of parts of a current design ... however,
as Matthew says, all this is crucially dependent on finding good
variable orderings and while there are reordering algorithms to improve
variable orderings it still requires  someone with an understanding of
both the model and the model checker to get at good "first
approximation".

Theorems proving may seem inefficient, but used in the correct places
(and probably with a preparedness to use mk_thm to avoid major delays
in "proving to obvious") can be more efficient due to the ability to
abstract and generalise. At the workshop day after the CAV meeting at
Stanford this year Paul Lowenstein gave an interesting talk of some of
his experiences with formal methods at Sun ... two examples used model
checking but the third used HOL because "it was quicker"!

> Reality is likely to be somewhere in between, when the clouds of hype
> disperse.

Theorem proving and model checking have problems but their strengths and
weaknesses may be complimentary:

HOL-like theorem provers are good at abstraction but are inefficient at
knocking out "simple" proofs, BDD based model checkers are good at
proving simple properties but need abstraction to handle large designs.

I think "reality" is "likely to be somewhere in between" with systems
which can use the abstractive power of theorem proving to be able
construct "correct abstarction" of problems into simpler ones which can
be handed on to a BDD based model checker to prove. Interestingly at
the CAV meeting I noticed that some of the model checking people seem
to be coming to this opinion ... or, they were realising that there
might not be another BDD-liek quantum jump in representable model size
to come and they need other techniques to handle big designs.


--------------------------------------------------------------------------
david shepherd:                           sgs-thomson microelectronics ltd 
email:des@inmos.co.uk                                      1000 aztec west
tel: 01454-616616 x 638                                        almondsbury
                                                                   bristol
"whatever you don't want, you don't want negative advertising"    bs12 4sq