Designing correct circuits : proceedings of the Second IFIP WG10.2/WG10.5 Workshop on Designing Correct Circuits, Lyngby, Denmark, 6-8 January 1992
著者
書誌事項
Designing correct circuits : proceedings of the Second IFIP WG10.2/WG10.5 Workshop on Designing Correct Circuits, Lyngby, Denmark, 6-8 January 1992
（IFIP transactions, A . Computer science and technology ; 5）
North-Holland , Elsevier Science [distributor], 1992
大学図書館所蔵 全9件
内容説明・目次
内容説明
The papers compiled in this volume cover a wide range of topics within the general area of provably correct design, including proofs of fundamental results, post hoc formal verification of designs and design techniques where correctness is ensured by construction. The papers are unique in that they demonstrate the use of design techniques for designing real chips. The book should, thus, not be missed by students and researchers interested in the deployment of formally-based techniques on real problems within a great diversity of application areas. Application areas treated within the volume range from packet-routers, arbiters, multiprocessors, serial-parallel converters and CPUs - to arithmetic units and counters. A significant group of the papers is concerned with the special requirements of asynchronous and delay-insensitive design.
目次
Using Transformations and Verification in Circuit Design (J.B. Saxe, S.J. Garland, J.V. Guttag, J.J. Horning). Modulo-N Counters: Design and Analysis of Delay-Insensitive Circuits (J.C. Ebergen, A.M.G. Peeters). Newtonian Arbiters Cannot be Proven Correct (M. Mendler, T. Stroup). Incomplete TRS-Specifications of Boolean Functions and their Verification (S. Krischer). Using the Language Lustre for Sequential Circuit Verification (G. Thuau, B. Berkane). Invited Talk: Three Notions of Proof (P. Naur). Transe: An Experimental Transformation Assistant for Digital Circuit Design (G. Durrieu, K. Kessaci, M. Lemaitre). Circuit Analysis by Non-Standard Interpretation (S. Singh). Reasoning about Permutations in Regular Arrays (B. Lisper, S. Rajopadhye). Sequence Semantics of Ruby (L. Rossen, R. Sharp). A Proof of the Non-Restoring Division Algorithm and its Implementation on the Cathedral-II ALU (D. Verkest, L. Claesen, H. De Man). Invited Talk: Formal Design in an Industrial Research Laboratory: Lessons and Perspectives (J. Bormann, H. Nusser-Wehlan, G. Venzl). Using Synchronized Transitions for Simulation and Timing Verification (M.R. Greenstreet). Provably Correct Synthesis of Asynchronous Circuits (S.F. Smith, A.E. Zwarico). High-level Design of an Asynchronous Packet-routing Chip (M.B. Josephs, R.H. Mak, J.T. Udding, T. Verhoeff, J.T. Yantchev). Analysis and Identification of Self-timed Circuits (M. Kishinevsky, A. Kondratyev, A. Taubin, V. Varshavsky).
「Nielsen BookData」 より