Hardware Specification, Verification and Synthesis: Mathematical Aspects

Chapter 20 Design for verifiability

Chapter 21 Verification of synchronous circuits by symbolic logic simulation

Chapter 22 Constraints, abstraction, and verification

Chapter 23 Formalising the design of an SECD chip

Chapter 24 Reasoning about state machines in higher-order logic

Chapter 25 A mechanically derived systolic implementation of pyramid initialization

Chapter 26 Behavior-preserving transformations for high-level synthesis

Chapter 27 From programs to transistors: Verifying hardware synthesis tools

Chapter 28 Combining engineering vigor with mathematical rigor

Chapter 29 Totally verified systems: Linking verified software to verified hardware

Chapter 30 What's in a timing discipline? Considerations in the specification and synthesis of systems with interacting asynchronous and synchronous components

Chapter 31 Complete trace structures

Chapter 32 The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation

Chapter 33 Manipulating logical organization with system factorizations

Chapter 34 The verification of a bit-slice ALU

Chapter 35 Verification of a pipelined microprocessor using clio

Chapter 36 Verification of combinational logic in Nuprl

Chapter 37 Veritas+: A specification language based on type theory

Chapter 38 Categories for the working hardware designer