		Search-engine friendly clone of the ACL2 documentation.

Expressions

Why-infinite-width

Notes about our use of infinite-width vectors as the basis for our expression language.

It probably seems very odd to base the core of a hardware description language on infinite width vectors. After all, in real hardware every wire and register will, of course, be of some particular, finite size.

In HDLs like Verilog, every variable is always declared to have some particular width, and every operator like a + b ultimately ends up being interpreted as having some fixed size—well, at least after ``elaboration'' is over. As a concrete example to discuss, consider a Verilog fragment like the following:

wire signed [3:0] a = ...;
wire [15:8] b = ...;
wire c = ...;
wire [7:0] ans = {8{c}} & (a % b);

We can imagine developing vector-level expression languages that include size information. This might be done, for instance, by having a kind of context that records the sizes and ranges of the various expressions, and then interpreting vector-level expressions in some way that is relative to this context. For instance, our context might be some kind of structure that binds names to ranges/types, say:

((a   (signed 3 0))
 (b   (unsigned 15 8))
 (c   (unsigned nil nil))
 (ans (unsigned 7 0)))

And given such a context, we could write functions to infer the widths of operators. We might, for instance, represent the expression for ans as something like this:

(bitand (replicate 8 c) (mod (cast-to-unsigned a) b))

And then, using the context, we would be able to see that this occurrence of mod is an 8-bit operation, and its first argument a needs to be zero-extended from 4 bits to 8 bits, and so on. We might be able to use the context to type-check expressions and determine that certain expressions, like (bitsel 5 a), are invalid since 5 is not a valid index into a wire from 3 to 0.

All of this might be a fine approach, but we have not pursued it.

Instead, in our expression language, we adopt the convention that every variable represents an infinitely long, signed value. The main consequence of this is that we do not need a context. Instead, all size/signedness coercions become explicit in the expressions themselves.

This seems like a strong advantage. It means, for instance, that every expression can be understood, exactly, all by itself, without having to consider or look up any other information.