edited by Magdy A. Bayoumi, Greham Jullien ; organized by the Center for Advanced computer Studies, University of Southwestern Louisiana ; co-sponsored by IEEE Circuits and Systems Society, IEEE Computer Society
出版情報:
Los Alamitos, Calif. ; Tokyo : IEEE Computer Society Press, c1998 xvi, 460 p.
IEEE/ACM International Conference on Computer-Aided Design ; IEEE Circuits and Systems Society ; IEEE Computer Society ; Institute of Electrical and Electronics Engineers ; IEEE Electron Devices Society
出版情報:
New York : Association for Computing Machinery, c1998 xxii, 704 p. ; 28 cm
Esterel and Jazz Two Synchronous Languages for Circuit Design / Gérard Berry
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specifications / Peter Jansen
Proof of Microprocessors
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer / Ravi Hosabettu ; Ganesh Gopalakrishnan ; Mandayam Srivas
Formal Verification of Explicitly Parallel Microprocessors / Byron Cook ; John Launchbury ; John Matthews ; Dick Kieburtz
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic / Miroslav Velev ; Randal Bryant
Efficient Decompositional Model-Checking for Regular Timing Diagrams / Nina Amla ; E. Allen Emerson ; Kedar S. Namjoshi
Vacuity Detection in Temporal Model Checking / Orna Kupferman ; Moshe Vardi
Formal Methods and Industrial Applications
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard / Cindy Eisner
Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors / Y.Xu ; E.Cerny ; A.Silburt ; A.Coady ; Y.Liu ; P.Pownall
Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics / Marius Bozga ; Oded Maler ; Stavros Tripakis
Abstraction and Compositional Techniques From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking / E.Allen Emerson ; Richard J. Trefler
Automatic Error Correction of Large Circuits Using Boolean Decomposi- tion and Abstraction / Dirk W. Hoffmann ; Thomas Kropf
Abstract BDDs: A Technique for Using Abstraction in Model Checking / Edmund Clarke ; Somesh Jha ; Yuan Lu ; Dong Wang
Theorem Proving Related Approaches
Formal Synthesis at the Algorithmic Level / Christian Blumenröhr ; Viktor Sabelfeld
Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving / Mark Aagaard ; Thomas Melham ; John O'Leary
Verification of Infinite State Systems by Compositional Model Checking / K.L.McMillan
Symbolic Simulation/Symbolic Traversal
Formal Verification of Designs with Complex Control by Symbolic Simulation / Gerd Ritter ; Hans Eveking ; Holger Hinrichsen
Hints to Accelerate Symbolic Traversal / Kavita Ravi ; Fabio Somenzi
Specification Languages and Methodologies
Modeling and Checking Networks of Communicating Real-Time Processes / Jürgen Ruf
"Have I Written Enough Properties?" A Method of Comparison between Specification and Implementation / Sagi Katz ; Orna Grumberg ; Danny Geist
Program Slicing of Hardware Description Languages / E.Clarke ; M.Fujita ; S.P.Rajan ; T.Reps ; S.Shankar ; T.Teitelbaum
Posters
Results of the Verification of a Complex Pipelined Machine Model / Jun Sawada ; Warren A. Hunt, Jr
Hazard-Freedom Checking in Speed-Independent Systems / Husnu Yenigun ; Vladimir Levin ; Doron Peled ; Peter Beerel
Yet Another Look at LTL Model Checking / Klaus Schneider
Verification of Finite-State-Machine Refinements Using a Symbolic Methodology / Stefan Hendricx ; Luc Claesen
Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars / George Economakos ; George Papakonstantinou
A Systematic Incrementalization Technique and Its Application to Hardware Design / Steven Johnson ; Yanhong Liu ; Yuchen Zhang
Bisimulation and Model Checking / Kathi Fisler ; Moshe Y. Vardi
Circular Compositional Reasoning about Liveness
Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell / Nancy A. Day ; Jeffrey R. Lewis
Exploiting Retiming in a Guided Simulation Based Validation Methodology / Aarti Gupta ; Pranav Ashar ; Sharad Malik
Fault Models for Embedded Systems / Jens Chr. Godskesen
Validation of Object-Oriented Concurrent Designs by Model Checking / Michaela Huhn ; George Logothetis
Author Index
Invited Talks
Esterel and Jazz Two Synchronous Languages for Circuit Design / Gérard Berry
Design Process of Embedded Automotive Systems - Using Model Checking for Correct Specifications / Peter Jansen
The 50 revised full papers presented were carefully selected for inclusion in the volume
The book is divided into sections on design environments and tools, theory and methods, engineering systems, intelligent systems, signal processing, and specific methods and applications
The 50 revised full papers presented were carefully selected for inclusion in the volume
The book is divided into sections on design environments and tools, theory and methods, engineering systems, intelligent systems, signal processing, and specific methods and applications
Minimalist Proof Assistants: Interactions of Technology an Methodology in Formal System Level Verification / Kenneth L. McMillan
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution / Robert B. Jones ; Jens U. Skakkebaek ; David L. Dill
Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking / Miroslav N. Velev ; Randal E. Bryant
Solving Bit-Vector Equations / M.Oliver Moller ; Harald Rueß
The Formal Design of 1M-Gate ASICs / Asgeir Por Eiriksson
Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations / Justin E. Harlow III ; Franc Brglez
A Tutorial on Stalmarck's Proof Procedure for Propositional Logic Mary Sheeran and Gunnar Stalmarck
Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods / Macha Nikolskaia ; Antoine Rauzy ; David James Sherman
Bisimulation Minimization in an Automata-Theoretic Verification Framework / Kathi Fisler ; Moshe Y. Vardi
Automatic Verification of Mixed-Level Logic Circuits / Keith Hanna
A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk / S. Tasiran ; S.P. Khatri ; S. Yovine ; R.K. Brayton ; A. Sangiovanni-Vincentelli
Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints / Fen Jin ; Henrik Hulgaard ; Eduard Cerny
Using MTBDDs for Composition and Model Checking of Real-Time Systems / Jurgen Ruf ; Thomas Kropf
Formal Methods in CAD from an Industrial Perspective / Carl-Johan H. Seger
A Methodology for Automatic Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool / Nazanin Mansouri ; Ranga Vemuri
Combined Formal Post- and Presynthesis Verification in High Level Synthesis / Thomas Lock ; Michael Mendler ; Matthias Mutz
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem / Abdel Mokkedem ; Ravi Hosabettu ; Ganesh Gopalakrishnan
A Performance Study of BDD-Based Model Checking / Bwolen Yang ; David R. O'Hallaron ; Armin Biere ; Olivier Coudert ; Geert Janssen ; Rajeev K. Ranjan ; Fabio Somenzi
sponsored by the Japan Society of Applied Physics, IEEE Electron Devices Society, in cooperation with IEEE Asian Steering Committee for Trans. on CAD/ICAS, Institute of Electronics, Information and Communication Engineers
出版情報:
Tokyo, Japan : Business Center for Academic Societies Japan , Piscataway, NJ : Copies can be purchased from IEEE Service Center Single Publication Sales Unit, c1993 xi, 179 p. ; 30 cm
sponsored by VLSI Society of India(VSI), Dept. of Electronics-Government of India in cooperation with the IEEE Cmputer Society's Technical Committees on Design Automation and VLSI, IEEE Circuits and Systems Society, ACM SIGDA
出版情報:
Los Alamitos, Calif. : IEEE Computer Society Press, c1995 xxvii, 425 p. ; 28 cm
sponsored by Iowa State University, IEEE Computer Society Technical Committee on VLSI, IEEE Circuits and Systems Society ; in cooperation with IEEE Signal Processing Society, ACM SIGDA
出版情報:
Los Alamitos, Calif. : IEEE Computer Society Press, c1996 xiii, 300 p. ; 28 cm
Amsterdam ; New York : North-Holland , New York, N.Y., U.S.A. : Distributors for the U.S. and Canada, Elsevier Science Pub. Co., 1991 xii, 350 p. ; 23 cm
Amsterdam ; New York : North-Holland , New York, N.Y., U.S.A. : Distributors for the U.S. and Canada, Elsevier Science Pub. Co., 1990 xiv, 380 p. ; 23 cm
sponsored by VLSI Society of India (VSI) , DOE, Government of India ; in cooperation with ACM SIGDA IEEE, IEEE Circuits and Systems Society, IEEE Computer Society DATC, VLSI-TC
出版情報:
Los Alamitos, Calif. : IEEE Computer Society Press, c1994 xx, 423 p. ; 28 cm
sponsored by the IEEE Computer Society Technical Committee on Design Automation, the Association for Computing Machinery Special Interest Group on Design Automation (SIGDA) ; in cooperation with IFIP Workgroups 10.2 and 10.5
出版情報:
Los Alamitos, Calif. : IEEE Computer Society Press, c1994 ix, 171 p. ; 28 cm
Amsterdam ; New York : North-Holland , New York, N.Y., U.S.A. : Distributors, for the U.S. and Canada, Elsevier Science Pub. Co., 1990 x, 457 p. ; 23 cm
Shuzi Yang, Ji Zhou, Cheng-Gang Li, chairs/editors ; sponsored by Chinese Computer Federation ... [et al.] ; cosponsored by Association for Computing Machinery, SIGGRAPH, USA ... [et al.] ; organized by Huazhong University of Science and Technology, China ; published by SPIE--the International Society for Optical Engineering
出版情報:
Bellingham, Wash., USA : SPIE, c1996 xiii, 826 p. ; 28 cm