Hardware Specification, Verification and Synthesis 1989: Ithaca, NY, USA

Session 1

• George J. Milne:
  Design for Verifiability. 1-13
  
• Randal E. Bryant:
  Verification of Synchronous Circuits by Symbolic Logic Simulation. 14-24
  
• Daniel Weise:
  Constraints, Abstraction and Verification. 25-39
  

Session 2

• Brian T. Graham, Graham M. Birtwistle:
  Formalising the Design of an SECD chip. 40-66
  
• Paul Loewenstein:
  Reasoning about State Machines in Higher-Order Logic. 67-89
  
• Christian Lengauer, Bikash Sabata, Farshid Arman:
  A Mechanically Derived Systolic Implementation of Pyramid Initialization. 90-105
  

Session 3

• Raul Camposano:
  Behavior-Preserving Transformations for High-Level Synthesis. 106-128
  
• Geoffrey M. Brown, Miriam Leeser:
  From Programs to Transistors: Verifying Hardware Synthesis Tools. 129-151
  
• Shiu-Kai Chin:
  Combining Engineering Vigor with Mathematical Rigor. 152-176
  

Session 4

• Jeffrey J. Joyce:
  Totally Verified Systems: Linking Verified Software to Verified Hardware. 177-201
  
• P. A. Subrahmanyam:
  What's in a Timing Discipline? Considerations in the Specification and Synthesis of Systems with Interacting Asynchronous and Synchronous Components. 202-223
  
• David L. Dill:
  Complete Trace Structures. 224-243
  
• Alain J. Martin:
  The Design of a Delay-Insensitive Microprocessor: An Example of Circuit Synthesis by Program Transformation. 244-259
  

Session 5

• Steven D. Johnson:
  Manipulating Logical Organization with System Factorizations. 260-281
  
• Warren A. Hunt Jr., Bishop Brock:
  The Verification of a Bit-slice ALU. 282-306
  
• Mark Bickford, Mandayam K. Srivas:
  Verification of a Pipelined Microprocessor Using Clio. 307-332
  

Session 6

• David A. Basin, Peter Del Vecchio:
  Verification Of Combinational Logic in Nuprl. 333-357
  
• F. Keith Hanna, Neil Daeche, Mark Longley:
  Veritas⁺: A Specification Language Based on Type Theory. 358-379
  
• Mary Sheeran:
  Categories for the Working Hardware Designer. 380-402