Formal Methods in Computer-Aided Design Book

	Challenges in system-level design	1
	Generating fast multipliers using clever circuits	6
	Verification of analog and mixed-signal circuits using hybrid system techniques	21
	A methodology for the formal verification of FFT algorithms in HOL	37
	A functional approach to the formal specification of networks on chip	52
	Proof styles in operational semantics	67
	Integrating reasoning about ordinal arithmetic into ACL2	82
	Combining equivalence verification and completion functions	98
	Synchronization-at-retirement for pipeline verification	113
	Late design changes (ECOs) for sequentially optimized esterel designs	128
	Non-miter-based combinational equivalence checking by comparing BDDs with different variable orders	144
	Scalable automated verification via expert-system guided transformations	159
	Simple yet efficient improvements of SAT based bounded model checking	174
	Simple bounded LTL model checking	186
	QuBE++ : an efficient QBF solver	201
	Bounded probabilistic model checking with the Mur[phi] verifier	214
	Increasing the robustness of bounded model checking by computing lower bounds on the reachable states	230
	Bounded verification of past LTL	245
	A hybrid of counterexample-based and proof-based abstraction	260
	Memory efficient all-solutions SAT solver and its application for reachability analysis	275
	Approximate symbolic model checking for incomplete designs	290
	Extending extended vacuity	306
	Parameterized vacuity	322
	An operational semantics for weak PSL	337
	Accepting predecessors are better than back edges in distributed LTL model-checking	352
	Bloom filters in probabilistic verification	367
	A simple method for parameterized verification of cache coherence protocols	382
	A partitioning methodology for BDD-based verification	399
	Invariant checking combining forward and backward traversal	414
	Variable reuse for efficient image computation	430