Hardware Specification, Verification and Synthesis: Mathematical Aspects

1. Front Matter

   PDF

2. Design for verifiability

   • George J. Milne

   Pages 1-13

3. Verification of synchronous circuits by symbolic logic simulation

   • Randal E. Bryant

   Pages 14-24

4. Constraints, abstraction, and verification

   • Daniel Weise

   Pages 25-39

5. Formalising the design of an SECD chip

   • Brian Graham, Graham Birtwistle

   Pages 40-66

6. Reasoning about state machines in higher-order logic

   • Paul Loewenstein

   Pages 67-89

7. A mechanically derived systolic implementation of pyramid initialization

   • Christian Lengauer, Bikash Sabata, Farshid Arman

   Pages 90-105

8. Behavior-preserving transformations for high-level synthesis

   • R. Camposano

   Pages 106-128

9. From programs to transistors: Verifying hardware synthesis tools

   • Geoffrey M. Brown, Miriam E. Leeser

   Pages 129-151

10. Combining engineering vigor with mathematical rigor

    • Shiu-Kai Chin

    Pages 152-176

11. Totally verified systems: Linking verified software to verified hardware

    • Jeffrey J. Joyce

    Pages 177-201

12. What's in a timing discipline? Considerations in the specification and synthesis of systems with interacting asynchronous and synchronous components

    • P. A. Subrahmanyam

    Pages 202-223

13. Complete trace structures

    • David L. Dill

    Pages 224-243

14. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation

    • Alain J. Martin

    Pages 244-259

15. Manipulating logical organization with system factorizations

    • Steven D. Johnson

    Pages 260-281

16. The verification of a bit-slice ALU

    • Warren A. Hunt Jr., Bishop C. Brock

    Pages 282-306

17. Verification of a pipelined microprocessor using clio

    • Mark Bickford, Mandayam Srivas

    Pages 307-332

18. Verification of combinational logic in Nuprl

    • David A. Basin, Peter Del Vecchio

    Pages 333-357

19. Veritas+: A specification language based on type theory

    • F K Hanna, N Daeche, M Longley

    Pages 358-379

20. Categories for the working hardware designer

    • Mary Sheeran

    Pages 380-402

Current research into formal methods for hardware design is presented in the papers in this volume. Because of the complexity of VLSI circuits, assuring design validity before circuits are manufactured is imperative. The goal of research in this area is to develop methods of improving the design process and the quality of the resulting designs. The major trend apparent at the workshop is that researchers are rapidly moving away from post hoc proof techniques with their great expense. A number of papers were presented that dealt with problems of synthesizing correct circuits and of designing with the goal of verification. Researchers are also beginning to deal with the theoretical issues of reasoning about concurrent systems and asynchronous systems, and to introduce new logical tools such as constructive type theory and category theory. Most of the research reported was performed in the United States.

• Hardware
• Mikroelektronik
• Mikroprozessor
• Schaltkreis
• Synchronisation
• VLSI
• Verifikation
• complexity
• formal method
• logic
• microprocessor
• processor
• verification

Policies and ethics