Symbolic model checking
Formal verification means having a mathematical model of asystem, a language for specifying desired properties of the system ina concise, comprehensible and unambiguous way, and a method of proofto verify that the specified properties are satisfied. When the methodof proof is carried out substantially by machine, we speak ofautomatic verification. "Symbolic Model Checking" deals withmethods of automatic verification as applied to computerhardware.The practical motivation for study in this area is the high andincreasing cost of correcting design errors in VLSI technologies.There is a growing demand for design methodologies that can yieldcorrect designs on the first fabrication run. Moreover, design errorsthat are discovered before fabrication can also be quite costly, interms of engineering effort required to correct the error, and theresulting impact on development schedules. Aside from pure costconsiderations, there is also a need on the theoretical side toprovide a sound mathematical basis for the design of computer systems, especially in areas that have received little theoreticalattention.
What people are saying - Write a review
We haven't found any reviews in the usual places.
SYMBOLIC MODEL CHECKING
8 other sections not shown
Other editions - View all
abstract ASSIGN asynchronous asynchronous circuit atomic propositions automatic Binary Decision Diagrams bisimulation Boolean formula bounded bus snooping characterized checker components computing configuration CTL formula cutoff point deadlock defined DME circuit equivalence relation esac example explosion problem exponential expression fairness constraints false Figure finite state machines firing sequence formal verification function gate Gigamax global bus UIC greatest fixed point implementation induction infinitely input interleaving model iteration language least fixed point lemma linear Mealy machines method model checking algorithm model checking technique module Mu-Calculus non-deterministic number of cells OBDD nodes occurs operators output Petri polynomial priority queue properties protocol read command read-owned read-shared command reduced reply-owned representation representing result semantics simulation snoop specification subset substitution symbolic constant symbolic model checking temporal logic terminal marking theorem token transition relation tree ordered true UIC for cluster unfolding variable vector waiting flag width write-resp-shared