Designing Correct Circuits: Workshop jointly organised by the Universities of Oxford and Glasgow, 26-28 September 1990, Oxford - Couverture souple
Synopsis
Contents: Constrained proofs.- Hardware synthesis in constructive type theory.- An algebraic framework for data abstraction in hardware description.- Generic specification of digital hardware.- Sampling and Proof: A Half-case Study.- High level test generation via process composition.- Towards truly delay-insensitive circuit realizations of process algebras.- The design of a delay-insensitive stack.- Specifying the micro-program parallelism for microprocessors of the von Neumann style.- The implementation and proof of a Boolean simplification system.- A model for synchronous switching circuits.- Efficient circuits as implementations of non-strict functions.- Verification of synchronous concurrent algorithms.- Use of the OTTER Theorem Prover for the Formal Verification of Hardware.- Proof-based transformation of formal hardware models.- Ruby algebra.- Using the declarative language LUSTRE for circuit verification.- Optimising designs by transposition.- Author Index.
Les informations fournies dans la section « Synopsis » peuvent faire référence à une autre édition de ce titre.
