4 ms·
Why higher-order logic is a good formalisation for hardware
- i_don_t_know 11mo ago(Original title shortened because it's too long.) Why higher-order logic is a good formalisation for specifying and verifying hardware Mike Gordon September 1985, 28 pages DOI https://doi.org/10.48456/tr-77 https://doi.org/10.48456/tr-77 Abstract Higher order logic was originally developed as a foundation for mathematics. In this paper we show how it can be used as: 1. a hardware description language, and 2. a formalism for proving that designs meet their specifications. Examples are given which illustrate various specification and verification techniques. These include a CMOS inverter, a CMOS full adder, an n-bit ripple-carry adder, a sequential multiplier and an edge-triggered D-type register. See also https://lawrencecpaulson.github.io/2023/01/04/Hardware_Verification.html https://lawrencecpaulson.github.io/2023/01/04/Hardware_Verif... and "Interactive Formal Verification, Lecture 11: Hardware Verification" by Lawrence Paulson https://www.youtube.com/watch?v=KVdgoEpo4uI&list=PLVdBoNna-44AN-hq4e3SZP-cbzFNtuV8g&index=13 https://www.youtube.com/watch?v=KVdgoEpo4uI&list=PLVdBoNna-4...