A Framework for the High-Level Specification and Verification of Synchronous Digital Logic Systems
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.
Cite
@article{arxiv.2201.10632,
title = {A Framework for the High-Level Specification and Verification of Synchronous Digital Logic Systems},
author = {Nick Mertin and K. Ritsuka and Karen Rudie},
journal= {arXiv preprint arXiv:2201.10632},
year = {2023}
}