A Framework for the High-Level Specification and Verification of Synchronous Digital Logic Systems

TL;DR

This paper introduces a formal framework for specifying and verifying synchronous digital logic systems, enabling automated verification of system behavior against specifications with a focus on complex interfaces and closed-loop configurations.

Contribution

It presents a novel uniform and symmetric approach to specifying input/output ports and an automaton-based method for verifying system behavior, advancing formal methods in digital logic design.

Findings

Automaton model encodes arbitrary computational processes.

Verification of closed-loop systems is decidable.

Framework supports complex input/output interfaces.

Abstract

A syntactic model is presented for the specification of finite-state synchronous digital logic systems with complex input/output interfaces, which control the flow of data between opaque computational elements, and for the composition of compatible systems to form closed-loop systems with no inputs or outputs. This model improves upon similar existing models with a novel approach to specifying input and output ports in a way which is uniform and symmetric. An automaton model is also presented for encoding arbitrary computational processes, and an algorithm is presented to generate an automaton representation of a closed-loop system. Using the automaton model, the problem of timing-agnostic verification of closed-loop systems against a desired behavioural specification, encoded as the similarity of closed-loop systems in terms of the set of computations performed, is shown to be decidable. The relationship between the models and real-world implementations of systems is discussed.