## Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference, CHARME '95, Frankfurt, Germany, October 1995. ProceedingsThis book constitutes the refereed proceedings of the IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design Methodologies, CHARME '95, held in Frankfurt, Germany, in October 1995. The 20 revised full papers presented were carefully selected by the program committee and address all current aspects of research and advanced applications in the field of formal verification of hardware. Among the topics covered are model checking, theorem proving, formally verified synthesis, process algebras, finite state systems, verification environments, language containment, and VHDL. |

### What people are saying - Write a review

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

### Contents

Theorem proving | 35 |

Formally verified synthesis | 71 |

Process algebras | 103 |

Copyright | |

1 other sections not shown

### Other editions - View all

### Common terms and phrases

abstract machine actions algorithm applied approach assignment automata automated automaton behaviour bisimulation Boolean c-step cache coherence circuit components compressed values condition construction correct corresponding defined definition delta cycle denote deterministic elements encoding equation equivalence error event example execution expression finite first-order formal verification formula function gate given graph hardware description language hardware design hash table IEEE implementation initial input interface process labeled language logic loop memory model checking node non-deterministic Nqthm omission probability operator output partial order path port process algebra process statement proof properties protocol reachable recursive registers relation represent representation resp reuse semantics seqi sequence sequential sequential circuits signal simulation specification step structure subset Symbolic Model Checking symbolic simulation synchronous synthesis tableau temporal logic theorem tion transformation transition relation transition system tuple variables verification methods VHDL wait statement