## Mechanized reasoning and hardware designCovers chip designs, mathematical proof versus simulation, automatic verification of sequential circuit designs, and microprocessor specification and verification |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

David May Geoff Barrett and David Shepherd | 3 |

H Pyoott | 21 |

Warren A Hunt Jr and Bishop C Brock | 35 |

Copyright | |

6 other sections not shown

### Common terms and phrases

2OBJ abstract adder algorithm applied Areg arithmetic asynchronous circuits automatic behaviour binary binary decision diagrams Bool boolean Boyer-Moore cache cell clock complex components Computer Science constructed correctness defined dependent types described developed emit encoding equational logic Esterel example execution exits floating point formal methods formal verification formula framework logic function Gonthier groups Halt hardware design hardware verification higher-order IEEE implementation inference rules input instant instruction integers interface loop mathematical mechanism microcode microprocessor model checking module netlist Nuprl OBJ3 object logic Occam operand operations output parallel parametrized pipeline primitive processor programming language proof tree provides proving reasoning represent representation result rewriting semantics sequence sequential signal simulation specification stat statement structure subgoals synchronous syntax synthesis tactics techniques temporal logic term terminates theorem prover transformation transition relation transition systems translation transputer trap type theory variables viper wires