A Formal Method for the Specification, Analysis, and Design of Register-Transfer Level Digital Logic

This paper describes a method for formally modeling digital logic using algebraic relations. The relations model digital logic at the register-transfer (RT) level. An RT-level behaviorial specification is used to develop the relations, which express timing relationships that must be satisfied by any correct implementation. An extension of the model is shown which can be used for synthesis at the RT level. The growth rate and computational properties of the model are discussed, and an example of synthesis is shown.