Communications - October 2011

model: sequential processes, stack-based procedure calls, traditional stack-based updatable variables, and cooperative multitasking. BSV, on the other hand, is born out of direct hardware description—state and parallel state transitions. The computer science literature has a computation model that is well suited for this, variously called Term Rewriting Systems, 13 Guarded Atomic Actions, or Rewrite Rules. It is used in many formal specification languages for complex concurrent systems, including Dijkstra’s Guarded Commands, 6 Chandy and Misra’s UNITY, 4 Lamport’s TLA+, 14 Abrial’s Event-B, 16 and many more. The following BSV excerpt illustrates a computation to sort four integers in ascending order.

Reg #(int) x1 <- mkRegU;

Reg #(int) x2 <- mkRegU;

Reg #(int) x3 <- mkRegU;

Reg #(int) x4 <- mkRegU;

rule swap12 (x1 > x2); x1 <= x2; x2 <= x1;

endrule

rule swap23 (x2 > x3); x2 <= x3; x3 <= x2;

endrule

rule swap34 (x3 > x4); x3 <= x4; x4 <= x3;

endrule

The first few lines instantiate four registers (storage elements) named x1 ... x4, containing values of type int. The mkRegU right-hand sides are the constructors, whose details are not important here.

The rule (or Guarded Atomic Action) swap12 is like a reactive process (that is, it can “fire” whenever its Boolean condition x1>x2 is true). The body of a rule is an Action and is semantically an instantaneous event. Here it is composed of two smaller Actions: one that assigns the value in x1 into x2, and vice versa. The net effect is to swap the values in the two registers. Rules swap23 and swap34 are similar.

There is no inherent sequencing between rules—a rule can fire when-

the strain is
beginning to show
as hardware chip
capacity has grown
exponentially
according to
moore’s Law and
we are called
upon to design
entire systems-
on-a-chip (socs)
of astonishing
diversity and
complexity.

ever its condition is true. Thus, in the example, it may happen that rules swap12 and swap34 perform their swaps in parallel. But what about rules that act on shared state, such as swap12 and swap23, both of which update x2? Rules have the semantics of atomic transactions, and thus, in this case, those two rules can fire only in some order (such as, sequentially). For this example, it does not matter which of the two possible orderings is chosen; the registers will eventually be sorted anyway.

The previous fragment seems repetitive—four similar registers and three similar rules—but we wrote it that way first to explain the semantics. It would more likely be written this way:

Vector#( 4,Reg#(int)) x <-replicateM (mkRegU);

for (int j= 1; j< 4; j=j + 1)
rule swap (x[j- 1]>x[j]);
x[j- 1] <= x[j];
x[j] <= x[j- 1];
endrule

This expands (“statically elaborates,” in hardware language jargon) to what is essentially the same fragment as before. Of course, the 4 here could be abstracted into a parameter. The fragment represents the classic bubble-sort algorithm of introductory programming texts—with the same O(N2) worst-case complexity—except that here the “bubbling” can happen in parallel, modulo atomicity (that is, any pair of enabled rules that do not conflict on a shared register can fire in parallel).

When atomicity requires two enabled conflicting rules to be sequenced, the order chosen can be left unspecified. This is at first alarming to hardware designers, where nondeter-minism is equated with unpredictable (bad) results. It is usually welcomed for formal specifications, however, where insisting on a schedule too early is regarded as an unnecessary over-specification. In BSV various techniques are available to nail down particular scheduling choices whenever necessary.