Formal verification of basic memory devices

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

Abstract

Formal methods have been used recently to verify high-level functional specifications of digital systems. Such formal proofs have used simple models of circuit components. In this article we describe complementary work which uses a more detailed model of components and demonstrates how hardware can be specified and verified at this level. In this model all circuits can be described as structures of gates, each gate having an independent propagation delay. The behaviour of digital signals in real time is captured closely. The function and timing of asynchronous and synchronous memory elements implemented using gates is derived. Formal proofs of correctness show that, subject to certain constraints on gate delays and signal timing parameters, these devices act as memory elements and exhibit certain timing properties. All the proofs have been mechanically generated using Gordon’s HOL system.