Correct Hardware Design and Verification Methods Book

	Esterel and Jazz : Two Synchronous Languages for Circuit Design	1
	Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specifications	2
	A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer	8
	Formal Verification of Explicitly Parallel Microprocessors	23
	Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic	37
	Model Checking TLA+ Specifications	54
	Efficient Decompositional Model-Checking for Regular Timing Diagrams	67
	Vacuity Detection in Temporal Model Checking	82
	Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard	97
	Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors	110
	Efficient Verification of Timed Automata using Dense and Discrete Time Semantics	125
	From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking	142
	Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction	157
	Abstract BDDs: A Technique for Using Abstraction in Model Checking	172
	Formal Synthesis at the Algorithmic Level	187
	Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving	202
	Verification of Infinite State Systems by Compositional Model Checking	219
	Formal Verification of Designs with Complex Control by Symbolic Simulation	234
	Hints to Accelerate Symbolic Traversal	250
	Modeling and Checking Networks of Communicating Real-Time Processes	265
	"Have I Written Enough Properties?" A Method of Comparison between Specification and Implementation	280
	Program Slicing of Hardware Description Languages	298
	Results of the Verification of a Complex Pipelined Machine Model	313
	Hazard-Freedom Checking in Speed-Independent Systems	317
	Yet Another Look at LTL Model Checking	321
	Verification of Finite-State-Machine Refinements Using a Symbolic Methodology	326
	Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars	330
	A Systematic Incrementalization Technique and Its Application to Hardware Design	334
	Bisimulation and Model Checking	338
	Circular Compositional Reasoning about Liveness	342
	Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell	346
	Exploiting Retiming in a Guided Simulation Based Validation Methodology	350
	Fault Models for Embedded Systems	354
	Validation of Object-Oriented Concurrent Designs by Model Checking	360
	Author Index	365