Formal Methods for Hardware Verification 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures / [electronic resource] :
edited by Marco Bernardo, Alessandro Cimatti.
- VII, 243 p. Also available online. online resource.
- Lecture Notes in Computer Science, 3965 0302-9743 ; .
- Lecture Notes in Computer Science, 3965 .
Hardware Design and Simulation for Verification -- Automatic Test Pattern Generation -- An Introduction to Symbolic Trajectory Evaluation -- BDD-Based Hardware Verification -- SAT-Based Verification Methods and Applications in Hardware Verification -- Building Efficient Decision Procedures on Top of SAT Solvers -- Refinement and Theorem Proving -- Floating-Point Verification Using Theorem Proving.
This volume presents a set of papers accompanying the lectures of the sixth e- tion of the InternationalSchool on Formal Methods for the Design of Computer, Communication and Software Systems (SFM). Thisseriesofschoolsaddressestheuseofformalmethodsincomputerscience asaprominentapproachto therigorousdesignofcomputer,communicationand software systems. The main aim of the SFM series is to o?er a good spectrum of current research in foundations as well as applications of formal methods, which can be of help for graduate students and young researchers who intend to approach the ?eld. SFM 2006 was devoted to formal techniques for hardware veri?cation and covered several aspects of the hardware design process, including hardware - signlanguagesand simulation, propertyspeci?cationformalisms,automatic test pattern generation, symbolic trajectory evaluation, BDD-based and SAT-based model checking, decision procedures, re?nement, theorem proving, and the v- i?cation of ?oating point units. The opening paper by Bombieri, Fummi, and Pravadelli provides a general viewonsimulation-basedmodeling andveri?cationstrategiesfor developing- bedded systems. In particular, the paper is focussed on describing state-of-the artco-simulationapproachesandveri?cationstrategiesbasedonfaultsimulation and assertion checking. The paper by Drechsler and Fey reviews the basic concepts and algorithms for the postproduction test of integrated circuits. The then authors present an advanced SAT-based tool for automatic test pattern generation. The paper by Claessen and Roorda concentrates on simulation-based mod- checking techniques, which do not need to represent the states of the design, but only the values that ?ow through each signal. In particular, the authors introduce a high-performance simulation-based model-checking technique called symbolic trajectory evaluation.
9783540343059
10.1007/11757283 doi
Computer science. Computer Communication Networks. Software engineering. Logic design. Computer Science. Software Engineering. Programming Languages, Compilers, Interpreters. Logics and Meanings of Programs. Special Purpose and Application-Based Systems. Computer Communication Networks.