Subject: RE: Accellera: Branching vs. Linear Time
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Sat Jul 14 2001 - 00:54:52 PDT
>
> so much for "formal verification".
>
> Moshe
>
In my experience, in an industrial setting a fully formal (and fully
automated) verification is not possible. At certain points, one has to
interject
manual/ meta level
reasoning. One might then create a axiomatic framework for the meta level
and reason in there, but probably that will be too hard (complexity wise, as
well as implementation wise), and secondly, industries can not afford to
have formal proof theorists as well as model checking experts, logicians
etc in their verification teams.
Besides all that, abstraction mechanism is usually manual, and certain
abstractions can be automated as is done in cadence SMV, when you tell
the system that certain variables are of certain types (symmetric, ordset
(for induction), scalarset (for symmetry)), and so on.
As a result, even the mechanical abstraction is manually hinted, and
if the user makes a mistake, some times SMV can catch that, for example
if a variable is declared for induction reasoning (ordset) and then one adds
an integer(not equal to 1)
to that variable, SMV does not allow it, and so on.
So, even though every thing is not automated/formal, at least the tool
and the language allows user to hint certain abstraction and proof
possibilities which I think should be a part of every tool!
Sandeep
This archive was generated by hypermail 2b28 : Tue Jul 10 2001 - 00:58:40 PDT