A prescriptive formal model for data-path hardware

The authors present a formal representation for register-level digital designs. The formalism is expressed in term of three models of a design, the data-flow structure, and timing models, and by bindings that express the interrelationships of the three models. The authors describe the desiderata that led to the particular choice of representation: a uniform representation for specification and implementation, the ability to express detailed implementation constraints, formality, descriptiveness, ease of testing, ease of encoding, executability, and prescriptiveness. They then describe related work and describe the representation and correctness constraints. Formal semantics for the representation are given, and a brief overview of a system that implements them is presented