9. CHARME 1997: Montréal, Québec, Canada

@proceedings{DBLP:conf/charme/1997,
  editor    = {Hon F. Li and
               David K. Probst},
  title     = {Advances in Hardware Design and Verification, IFIP WG 10.5 International
               Conference on Correct Hardware Design and Verification Methods,
               16-18 October 1997, Montr{\'e}al, Qu{\'e}bec, Canada},
  booktitle = {CHARME},
  publisher = {Chapman {\&} Hall},
  series    = {IFIP Conference Proceedings},
  volume    = {105},
  year      = {1997},
  isbn      = {0-412-81330-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Preface

• Allan Silburt: ASIC/system hardware verification at Nortel: a view from the trenches. 1 BibTeX

Part One - Advanced Processor Verification

• Xiaoshan Li, Antonio Cau, Ben C. Moszkowski, Nick Coleman, Hussein Zedan: Proving the correctness of the interlock mechanism in processor design. 5-22 BibTeX
• Werner Damm, Amir Pnueli: Verifying out-of-order executions. 23-47 BibTeX
• Ganesh Gopalakrishnan, Rajnish Ghughal, Ravi Hosabettu, Abdelillah Mokkedem, Ratan Nalumasu: Formal modeling and validation applied to a commercial coherent bus: a case study. 48-62 BibTeX

Part Two - Semantics of Hardware-Description Languages

• Dominique Borrione, F. Vestman, H. Bouamama: An approach to Verilog-VHDL interoperability for synchronous designs. 65-87 BibTeX
• Subash Shankar, James R. Slagle: A polymodal semantics for VHDL. 88-105 BibTeX
• Natividad Martínez Madrid, Peter T. Breuer, Carlos Delgado Kloos: A semantic model for VHDL-AMS. 106-123 BibTeX

Part Three - Model Checking

• Carlos M. Roman, Gary De Palma, Robert P. Kurshan: Model checking without hardware drivers. 127 BibTeX
• Willem Visser, Howard Barringer, Donal Fellows, Graham Gough, Alan Williams: Efficient CTL* model checking for analysis of rainbow designs. 128-145 BibTeX
• Jürgen Ruf, Thomas Kropf: Symbolic model checking for a discrete clocked temporal logic with intervals. 146-163 BibTeX

Part Four - Decision Graphs

• Gianpiero Cabodi, Paolo Camurati, Antonio Lioy, Massimo Poncino, Stefano Quer: A parallel approach to symbolic traversal based on set partitioning. 167-184 BibTeX
• Stefan Höreth: Implementation of a multiple-domain decision diagram package. 185-202 BibTeX
• David Déharbe, Anamaria Martins Moreira: Using induction and BDDs to model check invariants. 203-213 BibTeX

Part Five - New Verification Techniques

• Roger B. Hughes: CheckOff-M: model checking and its role in IP. 217 BibTeX
• Otmane Aït Mohamed, Xiaoyu Song, Eduard Cerny: On the non-termination of MDGs-based abstract state enumeration. 218-235 BibTeX
• Mario Baldi, Fulvio Corno, Maurizio Rebaudengo, Paolo Prinetto, Matteo Sonza Reorda, Giovanni Squillero: Simulation-based verification of network protocols performance. 236-251 BibTeX

Part Six - Issues in Formal Synthesis

• Steven D. Johnson, Paul S. Miner: Integrated reasoning support in system design: design derivation and theorem proving. 255-272 BibTeX
• George Economakos, George K. Papakonstantinou, Kiamal Z. Pekmestzi, Panayotis Tsanakas: Hardware compilation using attribute grammars. 273-290 BibTeX
• Matthias Mutz: Automatic post-synthesis verification support for a high level synthesis step by using the HOL theorem proving system. 291-308 BibTeX

Panel

• Carlos M. Roman: Is there a crisis in hardware verification? 309-310 BibTeX