FMCAD '98
(Formal Methods in Computer Aided Design)
Hyatt Rickey's
, Palo Alto, CA, Nov 3-6, 1998
Registration and Hotel/Transportation information
FMCAD'98 UPDATE
PROGRAM INFORMATION
TUESDAY, Nov.3
, 19:30-21:30: Registration and Reception, Hyatt Rickey's
WEDNESDAY, Nov.4
7:00-8:45:
Registration and Continental Breakfast
8:45-9.00:
Welcome
9:00-10.00:
Session 1: Invited talk, Dr. Kenneth McMillan. Title:
Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification.
Chair:
Edmund Clarke
10:00-10:15:
Coffee Break
10:15-11:15:
Session 2: Processor Verification I.
Chair: Mandayam Srivas.
10:15-10:45:
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution
, Robert B. Jones, Jens U. Skakkebaek, and David Dill
10:45-11:15:
Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking
, Miroslav N. Velev and Randal E. Bryant
11:15-12:15:
Session 3: Tools & Studies I.
Chair: Albert Camilleri.
11:15-11:45:
Solving Bit-Vector Equations
, M.O. Moller and H. RueB
11:45-12:15:
The formal design of 1M-gate ASICs
, Asgeir Thor Eiriksson
12:15-1:30:
Lunch served
1:30-2:30:
Session 4: Boolean Methods I.
Chair: Randal E. Bryant.
1:30-2:00:
Design of Experiments for evaluation of BDD packages using controlled circuit mutations
, Justin E. Harlow III and Franc Brglez
2:00-2:30:
A tutorial on stalmarck's proof procedure for propositional logic
, Mary Sheeran and Gunnar Stalmarck
2:30-3:30:
Session 5: Tools & Studies II.
Chair: Alan Hu.
2:30-3:00:
Almana: A BDD Minimization Tool Integrating Heuristic and Rewriting Methods
, Macha Nikolskaia, Antoine Rauzy, and David James Sherman
3:00-3:30:
Bisimulation Minimization in an Automata-Theoretic Verification Framework
, Kathi Fisler and Moshe Y. Vardi
3:30-3:45:
Coffee Break
3:45-4:45:
Session 6: Verification of Digital Abstraction.
Chair: Ranga Vemuri.
3:45-4:15:
Automatic verification of mixed-level logic circuits
, Keith Hanna.
4:15-4:45:
A timed automaton-based method for accurate circuit delay computation in the presence of cross-talk
, S. Tasiran, S.P. Khatri, S. Yovine, R.K. Brayton, and A. Sangiovanni-Vincentelli
4:45-5:45:
Session 7: Timing Issues and Verification.
Chair: Tom Henzinger.
4:45-5:15:
Maximum time separation of events in cyclic systems with linear and latest timing constraints
, Fen Jin, Eduard Cerny, and Henrik Hulgaard
5:15-5:45:
Using MTBDDs for composition and model checking of real-time systems
Juergen Ruf and Thomas Kropf
THURSDAY, Nov.5
7:00-9:00:
Registration and Continental Breakfast
9:00-10.00:
Session 8: Invited talk, Dr. Carl-Johan Seger. Title:
Formal Methods in CAD from an Industrial Perspective.
Chair:
John Brzozowski.
10:00-10:15:
Coffee Break
10:15-11:45:
Session 9: Tools & Studies III.
Chair: Steven Johnson.
10:15-10:45:
A methodology for completely automatic verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool
, Nazanin Manzouri and Ranga Vemuri
10:45-11:15:
Combined Formal Post- and Presynthesis Verification in High Level Synthesis
, Thomas Lock, Michael Mendler, and Matthias Mutz
11:15-11:45:
Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem
, Abdel Mokkedem, Ravi Hosabettu, and Ganesh Gopalakrishnan
11:45-1:00:
Lunch served
1:00-2:00:
Session 10: Special Talk: Prof. Randal E. Bryant and Bwolen Yang.
Title: A Performance Study of BDD-based Model Checking.
Chair:
Jerry Burch.
Co-authors: David R. O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev Ranjan, and Fabio Somenzi
2:00-2:15:
Break.
2:15-3:15:
Session 11: Model Checking I.
Chair: Eduard Cerny.
2:15-2:45:
Symbolic Model Checking Visualization
, Gila Kamhi, Limor Fix, Ziv Binyamini
2:45-3:15:
Input elimination and abstraction in model-checking
, Sela Mador-Haim and Limor Fix
3:15-3:30:
Coffee Break
3:30-4:30:
Session 12: Symbolic Simulation Methods.
Chair: Paul Loewenstein.
3:30-4:00:
Symbolic Simulation of the JEM1 Microprocessor
, David A. Greve
4:00-4:30:
Symbolic Simulation: an ACL2 Approach
, J. Strother Moore
4:30-5:15:
Business Meeting
7:30-9:30:
Session 13: Banquet. Speaker: Prof. Michael Flynn, Department of Electrical Engineering, Stanford. Title:
Computer Arithmetic: Past, Present, and Future.
Chair:
David Dill
FRIDAY, Nov.6
7:00-9:00:
Registration and Continental Breakfast
9:00-10.00:
Session 14: Invited talk, Prof. Amir Pnueli. Title:
Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study
Chair:
J.Strother Moore
Co-author: T. Arons.
10:00-10:15:
Coffee Break
10:15-11:15:
Session 15: Processor Verification II.
Chair: Steven German.
10:15-10:45:
Combining symbolic model checking with uninterpreted functions for out of order processor verification
, Sergey Berezin, Armin Biere, Edmund Clarke, and Yunshan Zhu
10:45-11:15:
Formally Verifying Data and Control with Weak Reachability Invariants
, Jeffrey Su, David Dill, and Jens U. Skakkebaek
11:15-12:15:
Session 16: Modeling and Verification Methods I.
Chair: Tom Shiple.
11:15-11:45:
Generalized reversible Rules
, Norris Ip
11:45-12:15:
An Assume-Guarantee rule for checking simulation
, T. A. Henzinger, S. Qadeer, S.K. Rajamani, and S. Tasiran
12:15-1:30:
Lunch served
1:30-2:30:
Session 17: Modeling and Verification Methods II.
Chair: Thomas Kropf.
1:30-2:00:
Three approaches to hardware verification: HOL, MDG, and VIS Compared
, Sofiene Tahar, Paul Curzon, and Jianping Lu
2:00-2:30:
An instruction set process calculus
, Shiu-Kai Chin and Jang Dae Kim
2:30-3:30:
Session 18: Model Checking II.
Chair: Limor Fix.
2:30-3:00:
Techniques for implicit state enumeration of EFSMs
, James Kukula, Tom Shiple, and Adnan Aziz
3:00-3:30:
Model checking on product structures
, Klaus Schneider
3:30-3:45:
Coffee Break
3:45-4:25:
Session 19: An Overview of some FM tools.
Chair: Michael J.C. Gordon.
3:45-3:55:
BDDNOW : A Parallel BDD Package
, Kim Milvang-Jensen and Alan J. Hu
3:55-4:05:
Model-checking VHDL with CV
, David Deharbe, Subash Shankar, and Edmund Clarke
4:05-4:15:
Alexandria: A tool for hierarchical verification
, Annette Bunker, Trent Larson, Michael Jones, Phillip Windley
4:15-4:25:
PV: An Explicit Enumeration Model-checker
, Ratan Nalumasu and Ganesh Gopalakrishnan
4:25-4:30:
Closing Remarks & Best Paper Award
4:30-5:45:
Tool Demos