A PRESCRIPTIVE FORMAL MODEL FOR DATA-PATH HARDWARE

In this paper we present a formal representation for register-level digital designs. This is a separated representation in that it provides separate but linked representations for behavior, timing, and structure. It has the advantage of being at the same time rich, formal, redundant, and prescriptive. Because it is rich, it covers many aspects of design correctness and completeness. Because it is formal, several well-characterized tests can be applied to a design to determine the extent to which it is well formed. Because it is redundant, internal consistency checks can be used to test a design's internal semantic integrity. And finally, because it is prescriptive, a violated constraint is closely linked to the actions that need to be taken to remove or ameliorate the violation. Specifically, it is possible to represent the structure of a design, the behavior desired of that structure, and the relationship between the two. Hence by testing for adherence to consistency constraints, we can determine whether the structure is capable of expressing the behavior. If the structure is incapable then analysis of the ways in which consistency constraints are violated provides a direct statement of what repairs are required to make the structure capable of expressing the desired behavior.