Why higher-order logic is a good formalism for specifying and verifying hardware. (English) Zbl 0612.94015
Formal aspects of VLSI design, Proc. Workshop, Edinburgh/Scotl. 1985, 153-177 (1986).
[For the entire collection see Zbl 0607.00018.]
Higher-order logic was originally developed as a foundation for mathematics. We show how it can be used both as a hardware description language, and as a deductive system for proving that designs meet their specifications. Examples used to illustrate various specification and verification techniques include a CMOS inverter, a CMOS full adder, an n- bit ripple-carry adder, a sequential multiplier and an edge-triggered Dtype register.
Higher-order logic was originally developed as a foundation for mathematics. We show how it can be used both as a hardware description language, and as a deductive system for proving that designs meet their specifications. Examples used to illustrate various specification and verification techniques include a CMOS inverter, a CMOS full adder, an n- bit ripple-carry adder, a sequential multiplier and an edge-triggered Dtype register.
MSC:
| 94C10 | Switching theory, application of Boolean algebra; Boolean functions (MSC2010) |
| 68Q65 | Abstract data types; algebraic specification |
