Theorem provers in circuit design : proceedings of the IFIP TC10/WG10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience, Nijmegen, the Netherlands, 22-24 June 1992

Ifip Tc, Experience, V. Stavridou, Tom Melham, Raymond T. Boute · North-Holland eBooks · 1992

Research Papers. Invited paper: Introduction to a Formally Defined Hardware Description Language (B.C. Brock, W.A. Hunt, Jr. and W.D. Young). A Description Methodology for Parameterized Modules in the Boyer-Moore Logic (D. Verkest et al.) Hierarchical Mixed-mode Verification of Complex FSMs Described at the RT Level (T. Margaria). Implementation of the Veritas Design Logic (K. Hanna, N. Daeche and G. Howells). Synchronous Realization of Asynchronous Computations (H.H. Lovengreen and J. Staunstrup). Modelling and Verification of Timing Conditions with the Boyer Moore Prover (D.J. Kinniment and A.M. Koelmans). Invited paper: Experience with Embedding Hardware Description Languages in HOL (R. Boulton et al.). Incremental Design and Formal Verification of Microcoded Microprocessors (J.M.J. Herbert). Transformational Design in a Theorem Prover (H. Busch). FUNNEL and 2OBJ: Towards an Integrated Hardware Design Environment (V. Stavridou et al.). Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification (M. Bickford and M. Srivas). Theorem Proving as an Industrial Tool for System Level Design (S. Bainbridge, A. Camilleri and R. Fleming). Tutorial Papers. Mechanized Verification of Circuit Descriptions Using the Larch Prover (J. Staunstrup, S.J. Garland and J.V. Guttag). The Veritas Design Logic: A User's View (K. Hanna and N. Daeche). Nuprl and its Use in Circuit Design (P.B. Jackson). Using the State Delta Verification System (SDVS) for Hardware Verification (B. Levy et al.).

Read the paper · More papers on PaperTik