Formal Methods in Computer-Aided Design: Second International Conference, FMCAD '98, Palo Alto, CA, USA, November 4-6, 1998, Proceedings (Lecture Notes in Computer Science, 1522)

This volumecontains the proceedingsof the Second InternationalConferenceon Formal Methods in Computer-Aided Design (FMCAD'98), organized November 4-6, in Palo Alto, California, USA. The rst event of this series was organized byMandayamSrivasand Albert Camilleriin 1996 inPaloAlto. FMCAD, which evolved from the series Theorem Provers in Circuit Design (TPCD), strives to beapremierforumfordisseminatingresearchinFormalVeri cation(FV) me- ods for digital circuits and systems, including processors, custom VLSI circuits, microcode, andreactivesoftware.Inadditiontosigni cantcase-studiesandve- cationapproaches, FMCADalsoendeavorstorepresentadvancesinthedriving technologies for veri cation, including binary decision diagrams, model che- ing, symbolicreasoning(theorem proving), symbolicsimulation, andabstraction methods. Theconferenceincludedfourinvitedlectures.Theinvitedlecturesweregiven by Kenneth McMillan (Cadence Berkeley Labs) on Minimalist proof assistants: interactions of technology and methodology in formal system level veric ation, by Carl-Johan Seger on Formal methods in CAD from an industrial perspective, by Randal E. Bryant and Bwolen Yang on A performance study of BDD-based model checking, and by Amir Pnueli on Veric ation of data-insensitive circuits: an in-order-retirement case study. Of the 55 regular paper submissionsreceived, 27 were selected by the technical program committee for presentation at the conference. All four tools papers received were also selected. We gratefully acknowledge the services of the technical program comm- tee of FMCAD'98, which consisted of Adnan Aziz (Univ. of Texas at Austin, USA), AlanHu(Univ.ofBritishColumbia, Canada), Albert Camilleri(Hewlett- Packard, USA), CarlPixley(Motorola, USA), CarlosDelgadoKloos (Univ. C- los III de Madrid, Spain), Ching-TsunChou (Intel, USA), EduardCerny (Univ. 3-540-49519-3_BookFrontmatter_OnlinePDF.pdf Formal Methods in Computer-Aided Design Preface Table of Contents 3-540-49519-3_1_OnlinePDF.pdf 3-540-49519-3_2_OnlinePDF.pdf Introduction Related Work Preliminaries The Approach First Step: Abstracting the Scheduling Logic Second Step: Functional Equivalence of SAI and ISA Mechanical Verification Discussion References 3-540-49519-3_3_OnlinePDF.pdf 1 Introduction 2 Abstracting Memories and Functional Units 3 Encoding Uninterpreted Symbols 3.1 Background 3.2 Our Encoding of Uninterpreted Symbols 4 Efficient Modeling of Memory Arrays in Symbolic Simulation 4.1 Symbolic Decisions 4.2 EMM Operation 4.3 Implementation of the Memory Write Operation 4.4 Dynamically Introducing Consistent Initial States 4.5 Comparing Final States 5 Bit-Level Uninterpreted Functions Modeled by the EMM 6 Generating Initial Memory State 6.1 Motivation 6.2 Indexing of Variable Groups 7 Correspondence Checking Methodology 8 Experimental Results 9 Conclusions and Future Work References 3-540-49519-3_4_OnlinePDF.pdf Introduction Preliminaries Solving Fixed Size Bit-Vector Equations Solving Bit-Vector Equations of Non-fixed Size Conclusions References 3-540-49519-3_5_OnlinePDF.pdf 1 Introduction 2 Compositional Model Checking 3 System Overview 4 Design Refinement 4.1 Cache Coherence Protocol Model 4.2 Pipeline Description 4.3 Outline of Refinement Strategy 4.4 Sequencing Protocol Message through the Pipeline 4.5 Details of Protocol Message Delivery 4.6 Details of CAM Index Abstraction 4.7 Details of Address Abstraction 4.8 Details of CAM Abstraction 4.9 Overview of Different Abstraction Layers 5 Size of Models and Run-Time Requirements 6 Conclusions 7 Future Research References 3-540-49519-3_6_OnlinePDF.pdf Introduction Design of Experiments: Treatments for BDDs Class F Mutants: A Basis Class F Mutants: Representative Implementations Comparative Experiments Conclusions References 3-540-49519-3_7_OnlinePDF.pdf Introduction Necessary Background: Proof Systems Gentzen's Sequent Calculus with Cut Removing Cut, and Gaining the Subformula Principle Removing Thinning The Dilemma Proof System The Dilemma Rule Dilemma Derivations Proof Hardness From Proof System to Proof Procedure Triplets Complexity Results Industrial Applications Summary References 3-540-49519-3_8_OnlinePDF.pdf Introduction BDD Size Minimization Heuristic Methods Rewriting Methods The Almana Toolkit Experimental Results Effect of Fan-In Permutation on Size Combining Analysis and Rewriting Towards an Exploratory Tool Conclusion References 3-540-49519-3_9_OnlinePDF.pdf Introduction Experimental Framework Computing Bisimulation Making Bisimulation More Tractable The Lee-Yannakakis Algorithm Minimized Bisimulation on Designs Minimizing Relative to Properties Minimizing with One Atomic Proposition Tuning the Original Algorithm A Comparison to Model Checking Related Work Conclusion and Future Work References 3-540-49519-3_10_OnlinePDF.pdf Introduction Specification of Analog Devices and Circuits Linear and Rectilinear Specifications Derived Specifications Specification of Digital Devices Specification at the Analog Level Verification Decision Procedure Practical Implementation Conclusions References 3-540-49519-3_11_OnlinePDF.pdf Introduction Timed Automata Notation Timed Automata Modeling Circuits and Waveforms Modeling Sets of Waveforms Modeling Combinational Gates Modeling Cross-Talk between Wires Delay Computation with Timed Automata A Region Automaton with Integer Delays The Region Automaton is Acyclic The Algorithm A Conjunctively Decomposed Representation Experimental Results Comparison with Conventional Methods Comparison with Non-specialized Traversal Conclusions and Future Work References 3-540-49519-3_12_OnlinePDF.pdf Introduction Modeling Temporal Behavior Timing Constraint Graphs Well-Formed Specifications Maximum Separation Problem An Algorithm for Acyclic Graphs Restricted Acyclic Graphs Block Partitions The MaxSep Algorithm for Causal Systems Algorithm for Restricted Cyclic Graphs Repetitive Behavior An Algorithm for Cyclic Graphs Sufficient Causal Conditions of Cyclic Systems Conclusion References 3-540-49519-3_13_OnlinePDF.pdf References 3-540-49519-3_14_OnlinePDF.pdf 3-540-49519-3_15_OnlinePDF.pdf Introduction Related Research Motivation Formalization of the Verification Technique Correctness Condition Generator Behavior Axiom Generation Data Path Axiom Generation Controller Axiom Generation Further Enhancements Implementation and Results Discussion and Ongoing Work References 3-540-49519-3_16_OnlinePDF.pdf Introduction High Level Synthesis Formal Capture of the Data Flow Description Formal Capture of the Clustering Result Formal Capture of the Final Result Correctness Correctness of the Clustering Result Correctness of the Final Result Experimental Results Summary and Outlook References 3-540-49519-3_17_OnlinePDF.pdf Introduction The PCI Local Bus Topology The PCI 2.1 Protocol Transaction Ordering Problem and the HP Proposal Formalization of the PCI Protocol in PVS The Model of PCI Network The Properties of PCI Network The PCI Protocol Formalization Formalization of Producer/Consumer Proof of Producer/Consumer Conclusions References 3-540-49519-3_18_OnlinePDF.pdf Introduction Overview BDD Basics Common Implementation Features Model Checking and Relational Product Setup Benchmark BDD Packages Evaluation Process Phase 1 Results: No Variable Reordering Computed Cache Size Garbage Collection Frequency Effects of the Complement Edge Memory Locality for Breadth-First BDD Construction Phase 2 Results: Dynamic Variable Reordering Present and Next State Variable Grouping Reordering the Transition Relations Effects of Initial Variable Orders General Results Issues and Open Questions Related Work Summary and Conclusions References 3-540-49519-3_19_OnlinePDF.pdf 1 Introduction 2 Palette (Profile, AnaLyze, and Track Tool) 3 Palette Features 3.1 Profiling and Analysis of Algorithms 3.2 Tracking the Progress 3.3 Automation of the Expertise 4 Conclusions and Future Work References 3-540-49519-3_20_OnlinePDF.pdf 1 Introduction 2 Preliminaries 2.1 Elimination of Free and Constrained Inputs 3 Netlist Remodeling for Maximizing Quantifiable Inputs 3.1 Remodeling of Latches 3.2 Re-encoding Control Signals 3.3 Re-encoding of Specifications 3.4 Fairness Constraints 4 New Greedy Algorithm for Early Quantification 5 Generating a Counter-Example 6 Data Abstraction 6.1 Definition of the Abstract Model 6.2 Reducing Data-Abstraction Problem to Input Elimination 7 Experimental Results 8 Conclusions References 3-540-49519-3_21_OnlinePDF.pdf Introduction Background JEM1 Microarchitecture Overview The JEM1 Symbolic Simulator PVS Formalization of the JEM1 Supporting Software Simulation Environment Program Results Issues Advances Conclusion References 3-540-49519-3_22_OnlinePDF.pdf Introduction Formalizing Computing Machines ACL2 as an Execution Engine ACL2 as a Theorem-Proving Engine ACL2 as a Symbolic Simulator Extensibility of the Symbolic Simulator Performance Conclusion References 3-540-49519-3_23_OnlinePDF.pdf Introduction Case Study: Out-of-Order Execution Designs Synchronous Transition Systems and their Refinement Refinement between Systems Verifying Refinement The Reference Model: System SEQ The Out-of-Order Algorithm System IOR Refines System SEQ Some Invariants of System IOR Conclusion References 3-540-49519-3_24_OnlinePDF.pdf Introduction Out-of-Order Execution Basic Abstraction Techniques Unabstracted Representation The Brute Force Approach The Reference File Tomasulo's Algorithm with Reference File Overall Verification Approach Other Optimizations Experimental Results Conclusion References 3-540-49519-3_25_OnlinePDF.pdf 1 Introduction A Simple Example 2 The Verification Method Extracting Regular Expressions for Control Paths Guiding Symbolic Simulation 3 Verification Process 4 TORCH 5 Verifying TORCH 6 Discussion References 3-540-49519-3_26_OnlinePDF.pdf Introduction Background Motivating Examples Message-Passing Cache Coherence Protocols Concurrent Programs Generalized Reversible Rules Definition Detection Reduction Algorithms for Invariants and Deadlock Checking Correctness of the Reduction Algorithm Implementing a Progenitor Generator Temporal Property Checking Comparison to Related Work Reversible Rules and Symmetry Practical Results References 3-540-49519-3_27_OnlinePDF.pdf 3-540-49519-3_28_OnlinePDF.pdf Introduction The Fairisle 4 by 4 Switch Fabric The HOL Verification The Specifications Time Taken Errors The MDG Verification The Specifications Time Taken Errors Scalability The VIS Verification The Specifications Time Taken Errors Conclusions References 3-540-49519-3_29_OnlinePDF.pdf Introduction The Mealy Machine Model Behavioral IspCal Syntax Substitution of Process Identifiers Semantics Structural IspCal Syntax Sort Operational Semantics of Structural IspCal Terms Bisimulation Equivalence Microprogrammed Controller User's Model Controller Implementation A Datapath Example A CPU Example Conclusions References 3-540-49519-3_30_OnlinePDF.pdf Introduction Related Work Implicit State Enumeration for EFSMs EFSM Model Implicit State Enumeration Automata-Based Decision Procedures Experimental Results Conclusions and Future Work References 3-540-49519-3_31_OnlinePDF.pdf Introduction Temporal Logics Model Checking on Product Structures CTL* and LTL Model Checking by Extraction of LeftCTL* Experimental Results References 3-540-49519-3_32_OnlinePDF.pdf Introduction Design Principles Workload Distribution Memory Usage Dynamic Variable Reordering Experimental Results Combinational Circuits Big BDDs Future Work References 3-540-49519-3_33_OnlinePDF.pdf Introduction Overview of the System Description of the VHDL Subset Specification Language The Model Checker Conclusion References 3-540-49519-3_34_OnlinePDF.pdf 1 Introduction 2 Overview of Alexandria 3 Using Alexandria to Verify the Birtwistle ALU 3.1 Initial Design and Verification 3.2 Adjustments to the Implementation 4 Conclusions References 3-540-49519-3_35_OnlinePDF.pdf 1 Introduction 2 {{sc Promela}xspace } Description Language 3 Partial Order Reductions in PV 4 On-the-Fly Model-Checking in PV 5 Selective Caching 6 Experimental Results 3-540-49519-3_BookBackmatter_OnlinePDF.pdf Author Index This Volumecontains The Proceedingsof The Second Internationalconferenceon Formal Methods In Computer-aided Design (fmcad’98), Organized November 4-6, In Palo Alto, California, Usa. The Rst Event Of This Series Was Organized Bymandayamsrivasand Albert Camilleriin 1996 Inpaloalto. Fmcad,which Evolved From The Series Theorem Provers In Circuit Design (tpcd), Strives To Beapremierforumfordisseminatingresearchinformalveri Cation(fv) Me- Ods For Digital Circuits And Systems, Including Processors, Custom Vlsi Circuits, Microcode,andreactivesoftware.inadditiontosigni Cantcase-studiesandve- Cationapproaches,fmcadalsoendeavorstorepresentadvancesinthedriving Technologies For Veri Cation, Including Binary Decision Diagrams, Model Che- Ing,symbolicreasoning(theorem Proving),symbolicsimulation,andabstraction Methods. Theconferenceincludedfourinvitedlectures.theinvitedlecturesweregiven By Kenneth Mcmillan (cadence Berkeley Labs) On Minimalist Proof Assistants: Interactions Of Technology And Methodology In Formal System Level Veric Ation , By Carl-johan Seger On Formal Methods In Cad From An Industrial Perspective, By Randal E. Bryant And Bwolen Yang On A Performance Study Of Bdd-based Model Checking, And By Amir Pnueli On Veric Ation Of Data-insensitive Circuits: An In-order-retirement Case Study. Of The 55 Regular Paper Submissionsreceived, 27 Were Selected By The Technical Program Committee For Presentation At The Conference. All Four Tools Papers Received Were Also Selected. We Gratefully Acknowledge The Services Of The Technical Program Comm- Tee Of Fmcad’98, Which Consisted Of Adnan Aziz (univ. Of Texas At Austin, Usa),alanhu(univ.ofbritishcolumbia,canada),albert Camilleri(hewlett- Packard,usa), Carlpixley(motorola,usa), Carlosdelgadokloos (univ. C- Los Iii De Madrid,spain), Ching-tsunchou (intel, Usa), Eduardcerny (univ. Minimalist Proof Assistants: Interactions Of Technology And Methodology In Formal System Level Verification -- Reducing Manual Abstraction In Formal Verification Of Out- Of- Order Execution -- Bit-level Abstraction In The Verification Of Pipelined Microprocessors By Correspondence Checking -- Solving Bit-vector Equations -- The Formal Design Of 1m-gate Asics -- Design Of Experiments For Evaluation Of Bdd Packages Using Controlled Circuit Mutations -- A Tutorial On Stålmarck’s Proof Procedure For Propositional Logic -- Almana: A Bdd Minimization Tool Integrating Heuristic And Rewritingmethods -- Bisimulation Minimization In An Automata-theoretic Verification Framework -- Automatic Verification Of Mixed-level Logic Circuits -- A Timed Automaton-based Method For Accurate Computation Of Circuit Delay In The Presence Of Cross-talk -- Maximum Time Separation Of Events In Cyclic Systems With Linear And Latest Timing Constraints --^ Using Mtbdds For Composition And Model Checking Of Real-time Systems -- Formal Methods In Cad From An Industrial Perspective -- A Methodology For Automated Verification Of Synthesized Rtl Designs And Its Integration With A High-level Synthesis Tool -- Combined Formal Post- And Presynthesis Verification In High Level Synthesis -- Formalization And Proof Of A Solution To The Pci 2.1 Bus Transaction Ordering Problem -- A Performance Study Of Bdd-based Model Checking -- Symbolic Model Checking Visualization -- Input Elimination And Abstraction In Model Checking -- Symbolic Simulation Of The Jem1 Microprocessor -- Symbolic Simulation: An Acl2 Approach -- Verification Of Data-insensitive Circuits: An In-order-retirement Case Study -- Combining Symbolic Model Checking With Uninterpreted Functions For Out-of-order Processor Verification -- Formally Verifying Data And Control With Weak Reachability Invariants -- Generalized Reversible Rules --^ An Assume-guarantee Rule For Checking Simulation -- Three Approaches To Hardware Verification: Hol, Mdg, And Vis Compared -- An Instruction Set Process Calculus -- Techniques For Implicit State Enumeration Of Efsms -- Model Checking On Product Structures -- Bddnow: A Parallel Bdd Package -- Model Checking Vhdl With Cv -- Alexandria: A Tool For Hierarchical Verification -- Pv: An Explicit Enumeration Model-checker. Ganesh Gopalakrishnan, Phillip Windley (eds.). Includes Bibliographical References And Index. This book constitutes the refereed proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, FMCAD '98, held in Palo Alto, California, USA, in November 1998. The 27 revised full papers presented were carefully reviewed and selected from a total of 55 submissions. Also included are four tools papers and four invited contributions. The papers present the state of the art in formal verification methods for digital circuits and systems, including processors, custom VLSI circuits, microcode, and reactive software. From the methodological point of view, binary decision diagrams, model checking, symbolic reasoning, symbolic simulation, and abstraction methods are covered