In my previus post on abstraction, we were left with the question of what makes a valid abstraction. For example, suppose we have a gate-level design of an adder. If we write:

a = b * c;

we can see that this is a higher level of abstraction, but we would not generally consider it a valid abstraction of an adder. A valid abstraction would be:

a = b + c;

In general, functions are not as simple as adders and multipliers. We need to define some way of determining whether a design is a valid abstraction of another design.

A valid abstraction is one that preserves some property of the original design.

In RTL, the property of interest is that the abstract function should produce the same output for all inputs, i.e. functionality is preserved. What abstractions are being used in RTL? Let’s look at our adder example. There is structural abstraction because we have eliminated all gates. There is data abstraction from bits to bit vectors. There is temporal abstraction if you consider that the gates have non-zero delays. There is no behavioral abstraction because values are specified for all possible input values. This is a valid abstraction if all output values of the abstraction are the same as the non-abstracted version.

Abstraction works like a less-than-or-equal (<=) operator. Suppose you have designs A and B. If A is an abstraction of B, we can write A <= B. Suppose also that B is an abstraction of C, B <= C. We know that if A <= B and B <= C, then A <= C. This also holds for abstractions. Since abstraction is the hiding of irrelevant detail, you can think of the less than relation as meaning “less detailed than”.

Suppose you have designs D, E, and F, with D<=E and D<=F. We know D is an abstraction of E and F, but what do we know about the relative abstraction levels between E and F? We cannot consider one as being an abstraction of the other even though they are equivalent in some sense. This type of relationship is important in design where D is a specification and E and F are different implementations of the same specification.

The flip side of this is: suppose we have designs P, Q, and R, with P<=R and Q<=R. In other words, P and Q are different abstractions of R. Again there is nothing we can say about the relative abstraction levels between P and Q. This relationship is important in verification where P and Q are different abstract models of the design R.

One last note: it is generally an intractable problem to prove that an abstraction is valid. If you are familiar with equivalence checking, this is basically a method to prove that an abstraction is valid.