Correct hardware design methodologies : proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies, Turin, Italy, June 12-14, 1991
著者
書誌事項
Correct hardware design methodologies : proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies, Turin, Italy, June 12-14, 1991
North-Holland , Distributors for the U.S. and Canada, Elsevier Science Pub. Co., 1992
大学図書館所蔵 件 / 全4件
-
該当する所蔵館はありません
- すべての絞り込み条件を解除する
注記
"Organized by ESPRIT Basic Research Action 3216 'CHARME' ... in cooperation with EEC CEC, Directorate General XIII [and] IFIP WG 10.2."
"Sponsored by Politecnico di Torino."
Includes bibliographical references and index
内容説明・目次
内容説明
The increasing interest in formal verification of hardware is witnessed by academic and industrial research efforts, multinational research projects and conferences. These proceedings contain the papers presented at the Workshop held in Turin, Italy from 12-14 June, 1991. Papers focus on the practical impact of formal techniques in VLSI design and verification, semantics for hardware description languages, proof environments and methodologies. Preliminary results of the ESPRIT Basic Research Action 3216 CHARME are discussed. Finite State Machines and their verification, semantics for hardware description languages, proof environments and methodologies, as well as examples of verified circuits and Design for Verifiability are also presented.
目次
Opening Session. CHARME: towards formal design and verification for provably correct VLSI hardware (L. Claesen, D. Borrione, H. Eveking, G.J. Milne, J.L. Paillet, P. Prinetto). Proof of FSMS. Formal verification of sequential circuits with VERENA: a case study (M. Mutz). The Product Machine and implicit enumeration to prove FSMs correct (P. Camurati, M. Gilli, P. Prinetto, M. Sonza Reorda). Languages and Semantics I. Semantics and verification for boolean kernel ELLA using IO automata (H. Barringer, G. Gough, T. Longshaw, B. Monahan, M. Peim, A. Williams). Semantics of Statecharts based on graph rewriting (A. Maggiolo-Schettini, A. Peron). FUNNEL: a CHDL with formal semantics (V. Stavridou, J.A. Goguen, S.M. Eker, S. Aloneftis). Specification and Verification. Verification of processor-like circuits (M. Langevin, E. Cerny). PREVAIL: a proof environment for VHDL descriptions (D. Borrione, L. Pierre, A. Salem). SFG-tracing: a methodology of Design for Verifiability (L. Claesen, M. Genoe, E. Verlind, F. Proesmans, H. De Man). Transformational Design. An improved systolic array for string correction (D. Sangiorgi, C. Lengauer). Formal realization of behaviour descriptions in synchronous logic with decentralized control (H. van der Weij). The systematic design of a systolic RSA converter (J.L.W. Kessels). Modelling. The description and automatic verification of digital circuits in Circal (A. Bailey, G.A. McCaskill, J. McIntosh, G.J. Milne). Consistent refinements of specifications for digital systems (N.A. Harman, J.V. Tucker). Design for Verifiability vs. Design for Testability: limiting designers' freedom to achieve what? (P. Camurati, P. Prinetto). Languages and Semantics II. Operational semantics for hardware design languages (H. Barringer, G. Gough, B. Monahan). Hardware specification using the assertion language ASTRAL (G. Buonanno, A. Coen- Porisini, W. Fornaciari). Embedding a CHDDL in a proof system (K.G.W. Goossens). Issues in Theorem-Proving. Improving the performance of a BDD-based tautology checker (S. Horeth). Application of a BDD-package to the verification of HDL descriptions (D. Borrione, D. Deharbe, H. Eveking, S. Horeth). Developing a toolkit for floating-point hardware in the Nuprl proof development system (P.B. Jackson). A synopsis on the comparison of HOL and Boyer-Moore for formal hardware verification (C.M. Angelo, D. Verkest, L. Claesen, H. De Man). Timing Verification. . Timing constraints verification using Temporal Logic (V. Cingel). Timing diagrams for writing and checking logical and behavioural properties of integrated systems (C. Antoine, B. Le Goff). Posters. Circuit layout using Non-Standard Interpretation (S. Singh). TATOO: an industrial timing analyzer (R. Stewart). Using the language LUSTRE for sequential circuit verification (G. Thuau, B. Berkane). From Temporal Logic to Finite Automata (G.G. de Jong). Formal derivation of a computer (L.G. Wang).
「Nielsen BookData」 より
