Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

Consistency of Incomplete Designs

IP.com Disclosure Number: IPCOM000083810D
Original Publication Date: 1975-Jul-01
Included in the Prior Art Database: 2005-Mar-01
Document File: 2 page(s) / 14K

Publishing Venue

IBM

Related People

Roth, JP: AUTHOR

Abstract

A computer hardware design is complete when inputs determine corresponding outputs. Designs specified at higher levels (e.g., architectural) are commonly incomplete, some outputs may not be determined for a particular input and state combination. There are effective methods for verification of complete designs. To understand the difficulty of extending this technique to incomplete designs, it is necessary to look first at the method of construction of these designs -- the form is called Regular -- and second to discuss the algorithm for constructing "counter-examples".

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 52% of the total text.

Page 1 of 2

Consistency of Incomplete Designs

A computer hardware design is complete when inputs determine corresponding outputs. Designs specified at higher levels (e.g., architectural) are commonly incomplete, some outputs may not be determined for a particular input and state combination. There are effective methods for verification of complete designs. To understand the difficulty of extending this technique to incomplete designs, it is necessary to look first at the method of construction of these designs -- the form is called Regular -- and second to discuss the algorithm for constructing "counter-examples".

A large-scale design is constructed by suitable interconnection of "macros" which, in turn, are composed from smaller macros and finally, the smallest element, the "incomplete circuit". This description holds true whether the design is defined at a high, say architectural, level or at a low, detailed logic design. Thus to define this construction precisely start with, not the incomplete circuit, but rather the cells which are used to define their functioning, their "behavior".

Cells are correspondences between certain assemblages of values of input variables (whether these variables represent an aspect of the behavior of just one physical object or macro or "spread", as they may, over several) and corresponding values of some output variables. Cells are consistent whenever "interfacing" of input parts implies interfacing of output parts. An assemblage of pairwise-consistent cells is an incomplete cover: it defines the functioning of some piece and level of the design.

If the cover contains all elements of the Cartesian product of its input variables then it is complete; otherwise, incomplete. An incomplete circuit has an incomplete defining cover.

Now construction begins by suitably interconnecting incomplete circuits, by identification of output variables of one with input variables of another. This step thus defines a new macro; its primary inputs are those of the original incomplete circuits which have not been identified with others; its primary outputs may be any variables input or output of the joined circuits. This proceeds inductively, step-by-step, using the macros in precisely the same way as for complete circuits. The construction is a regular incomplete design if; 1) no feedback is introduced;, and 2) if feedback is introduced then a special construction is used to ensure t...