Advances in Hardware Design and Verification: IFIP TC10 WG10.5 International Conference on Correct Hardware and Verification Methods, 16–18 October 1997, Montreal, Canada

Front Matter....Pages i-ix
ASIC/System Hardware Verification at Nortel: A View from the Trenches....Pages 1-1
Front Matter....Pages 3-3
Proving the Correctness of the Interlock Mechanism in Processor Design....Pages 5-22
Verifying Out-of-Order Executions....Pages 23-47
Formal Modeling and Validation Applied to a Commercial Coherent Bus: A Case Study....Pages 48-62
Front Matter....Pages 63-63
An approach to Verilog-VHDL interoperability for synchronous designs....Pages 65-87
A Polymodal Semantics for VHDL....Pages 88-105
A semantic model for VHDL-AMS....Pages 106-123
Front Matter....Pages 125-125
Model Checking without Hardware Drivers....Pages 127-127
Efficient CTL* Model Checking for Analysis of Rainbow Designs....Pages 128-145
Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals....Pages 146-163
Front Matter....Pages 165-165
A Parallel Approach to Symbolic Traversal based on Set Partitioning....Pages 167-184
Implementation of a Multiple-Domain Decision Diagram Package....Pages 185-202
Using induction and BDDs to model check invariants....Pages 203-213
Front Matter....Pages 215-215
CheckOff-M: Model Checking and Its Role in IP....Pages 217-217
On the Non-Termination of MDG-Based Abstract State Enumeration....Pages 218-235
Simulation-Based Verification of Network Protocols Performance....Pages 236-251
Front Matter....Pages 253-253
Integrated Reasoning Support in System Design: Design Derivation and Theorem Proving....Pages 255-272
Hardware Compilation Using Attribute Grammars....Pages 273-290
Automatic Post-Synthesis Verification Support for a High Level Synthesis Step by using the HOL Theorem Proving System....Pages 291-308
Panel Discussion: Is There a Crisis in Hardware Verification?....Pages 309-310
Back Matter....Pages 311-313