09Readiness, module arguments, and synthesis boundaries

1. Defining a module

A module definition names the interface it provides and then lists its state instances, its rules, and the definition of every method the interface promised.

Form

module moduleName(ProvidedInterfaceType);
  // state instances
  // rules
  // method definitions
endmodule

module mkAccumulator(Accumulator);
  Reg#(Bit#(8)) sum <- mkReg(0);

  method Action add(Bit#(8) x);
    sum <= sum + x;
  endmethod

  method Bit#(8) total = sum;
endmodule

A module must define every method of its provided interface. Leaving the provided interface out is the same as providing Empty.

2. Parameters, arguments, and provisos

Besides the provided interface, a module header can carry elaboration-time parameters, arguments the module consumes, and type constraints.

Form

module moduleName#(parameters)(arguments, ProvidedInterfaceType)
  provisos (constraints);
  ...
endmodule

module mkHolder#(t init)(Holder#(t))
  provisos (Bits#(t, tw));
  Reg#(t) stored <- mkReg(init);

  method Action put(t x);
    stored <= x;
  endmethod

  method t get = stored;
endmodule

Bits#(t, tw) reads "t has a bit representation, and its width is called tw". Storing t in a register needs that representation, so the proviso is required. It is checked for every concrete type the module is instantiated with. The typeclasses chapter covers provisos in full.

3. Passing values at instantiation

When you instantiate a module that has parameters and arguments using the short form, all actual values go in one parenthesized list: parameter values first, then arguments, with no # at the call.

Holder#(Bit#(8)) h <- mkHolder(8'd5);
SomeIfc unit <- mkSomeModule(4, sourceIfc,
                             clocked_by fastClock,
                             reset_by fastReset);

Every module has an implicit clock and reset. clocked_by and reset_by replace them for one instance.

Note. There is also a deprecated long form that declares the interface and then names a separate module instance on the next line, such as StackIfc#(Bit#(8)) stack(); followed by mkStack stackModule(stack);. It exists for SystemVerilog compatibility; use the short form in new code.

4. Implicit conditions of methods

Methods called from a rule can have readiness conditions of their own, called implicit conditions. A FIFO's deq and first are not ready while the FIFO is empty, and its enq is not ready while it is full.

rule move;              // no explicit condition
  outq.enq(inq.first);  // first is not ready while inq is empty
  inq.deq;
endrule

A rule is ready only when its explicit condition and the implicit condition of every method it calls are true. move names no condition, yet it cannot fire while inq is empty or outq is full. A method that is not ready blocks the whole rule; BSV never skips just that one call.

Note. An ordinary Reg has no value-dependent implicit conditions on its read or write methods. In a design made only of registers, you can decide readiness from the explicit conditions alone.

In your own modules, an if (condition) in a method header is that method's readiness condition. In a cycle where it is false, the method is not ready, and any rule that calls it does not fire at all.

Form

method ReturnType name(arguments) if (readyCondition);
  ...
endmethod

method ReturnType name if (readyCondition) = expression;

method Action enq(Bit#(8) x) if (count < 4);
  ...
endmethod

method Bit#(8) first if (count > 0) = items[0];

Implicit conditions keep invariants such as "never enqueue into a full queue" or "never dequeue from an empty one" in one place, the implementation. Calling rules do not repeat those checks.

5. A header if versus a body if

The position of the semicolon changes the meaning.

method Action guarded() if (ready);   // header if: readiness condition
  work;
endmethod

method Action conditional();          // body if: an ordinary branch
  if (ready) work;
endmethod

6. Ready, enabled, fired

Three separate judgments stand between a rule and a state change.

A failure at any stage looks the same from outside: nothing changed. When you debug, check readiness, the explicit condition, and conflicts separately. Conflicts are the subject of the rules that share state chapter.

7. Example: readiness reaches the caller

In ImplicitCondition.bsv, push is ready only while depth < 2. The rule fill in mkTop, however, has no explicit condition. rule report prints the last value and ends the simulation once b.full is true. Read the Bounded interface, the header condition on push, then fill, then report.

Predict before you run. On the first pushed line, is top now 10 or 0? What top value does report print?

package ImplicitCondition;

// The interface declares the method without its condition. The if clause
// belongs to the definition below.
interface Bounded;
  method Action push(Bit#(8) x);
  method Bit#(8) top;
  method Bool full;
endinterface

module mkBounded(Bounded);
  Reg#(Bit#(8)) stored <- mkReg(0);
  Reg#(Bit#(4)) depth  <- mkReg(0);

  // The if clause is an implicit condition. When it is false the method is
  // not ready, and every rule calling it is blocked.
  method Action push(Bit#(8) x) if (depth < 2);
    stored <= x;
    depth  <= depth + 1;
  endmethod

  method Bit#(8) top = stored;
  method Bool full = depth == 2;
endmodule

(* synthesize *)
module mkTop(Empty);
  Bounded b <- mkBounded;
  Reg#(Bit#(8)) sent <- mkReg(10);

  // No condition here mentions depth. The rule stops firing because push
  // stops being ready.
  rule fill;
    b.push(sent);
    $display("pushed %0d, top now %0d", sent, b.top);
    sent <= sent + 1;
  endrule

  rule report (b.full);
    $display("full, top = %0d", b.top);
    $finish(0);
  endrule
endmodule

endpackage

Check the result.

The decisive evidence is that there are only two pushed lines. fill contains no test of depth, yet in the cycle where push is not ready the whole of fill is disabled. The top now value on each line trails the pushed value by one step because top reads the state at the start of the cycle.

Try it yourself.

1. Change only the condition on push to depth < 3. At depth == 2, push is still ready, but full is already true and report ends the simulation. This change alone does not make a consistent three-entry capacity: readiness and the status method disagree.
2. Now change the condition to depth < 3 and full to depth == 3. A pushed 12, top now 11 line appears and the last line reports top = 12. Changing capacity means the readiness condition and the status method must describe the same limit.

8. Putting it together: a stack

8.1 Reading the code

Stack.bsv defines a four-entry stack whose element type is left open. Read it in this order:

1. The four methods of StackIfc#(type element_type) and the kind of each
2. provisos (Bits#(element_type, element_width)) on mkStack
3. The state: items, a four-element vector, and depth
4. The readiness conditions on push, pop, and top

package Stack;

import Vector::*;

export StackIfc(..), mkStack;

// An interface is a type: a named collection of methods.
// The parameter makes it work for any element type that can be
// stored in hardware.
interface StackIfc#(type element_type);
  method Action push(element_type x);
  method ActionValue#(element_type) pop;
  method element_type top;
  method Bool notEmpty;
endinterface

// A module is parameterised the same way. Provisos state what the
// compiler must know about the type for this body to be legal —
// here, that the element can be represented as bits.
module mkStack(StackIfc#(element_type))
  provisos (Bits#(element_type, element_width));

  Reg#(Vector#(4, element_type)) items <- mkRegU;
  Reg#(Bit#(3))                  depth <- mkReg(0);

  // An implicit condition. Callers cannot push a full stack; the
  // compiler makes any rule that tries wait instead.
  method Action push(element_type x) if (depth < 4);
    items <= shiftInAt0(items, x);
    depth <= depth + 1;
  endmethod

  // An ActionValue method does both: it changes state and returns a value.
  // Shifting toward index 0 is what makes the next element the new top;
  // decrementing depth alone would leave top returning the same value.
  method ActionValue#(element_type) pop if (depth > 0);
    items <= shiftInAtN(items, ?);
    depth <= depth - 1;
    return items[0];
  endmethod

  method element_type top if (depth > 0) = items[0];

  method Bool notEmpty = depth > 0;
endmodule

endpackage

Top.bsv instantiates a stack of Bit#(8). fill pushes three times, drain pops while the stack is not empty, and done confirms it is empty and stops.

package Top;

import Stack::*;
import Vector::*;

(* synthesize *)
module mkTop(Empty);

  // Instantiation binds a module to an interface with <-.
  // The element type is inferred from how the stack is used.
  StackIfc#(Bit#(8)) s <- mkStack;

  Reg#(Bit#(8)) step <- mkReg(0);

  rule fill (step < 3);
    s.push(step + 10);
    step <= step + 1;
    $display("pushed %0d", step + 10);
  endrule

  rule drain (step == 3 && s.notEmpty);
    // <- runs the ActionValue method and binds its result, the same arrow
    // that instantiates a module.
    let v <- s.pop;
    $display("popped %0d, top was %0d", v, s.top);
  endrule

  rule done (step == 3 && !s.notEmpty);
    $display("empty");
    $finish(0);
  endrule

endmodule

endpackage

8.2 Tracing the cycles

Predict before you run. After fill finishes, what are items[0] and depth? On the first popped line, are v and top was the same?

Check the result.

shiftInAt0 inserts at index 0 and shifts the other elements along by one. shiftInAtN shifts the other way, dropping the element at index 0. The value pop returns matches the top read in the same rule because both calls read the state at the start of the cycle.

Try it yourself.

1. Delete the line items <= shiftInAtN(items, ?); from pop. It still compiles, but popped 12, top was 12 appears three times: depth shrinks while index 0 never changes. Type checking does not prove state-update invariants like this one.
2. To change the stack's capacity, change the vector length, the width of depth, and the comparison in push together. If the three do not describe the same limit, the stack either overflows or stalls early.

9. Synthesizing modules

9.1 Marking a synthesis boundary

A BSV module becomes its own Verilog module when it carries the (* synthesize *) attribute or is named by bsc's -g moduleName option. Every example in this chapter marks mkTop with (* synthesize *) and compiles with -g mkTop.

A separately synthesized module must have a fully concrete interface. mkStack, whose element type is open, cannot be a synthesis boundary as it stands, so you wrap it at a concrete type:

(* synthesize *)
module mkStack8(StackIfc#(Bit#(8)));
  StackIfc#(Bit#(8)) stack <- mkStack;
  return stack;
endmodule

return stack; hands the child instance's interface back as this module's provided interface.

9.2 When an interface can become wires

At a synthesis boundary the interface turns into ports, so it must meet these conditions:

Note. A synthesis boundary can affect scheduling. Once a method argument is a single physical input port, two calls that pass different argument values in the same cycle may conflict. If the same module were inlined instead, bsc could sometimes let both calls fire together.

9.3 Other module types

The normal module type is Module#(ifc), and it is the only one that can be synthesized separately. When a definition needs a special module type, write it in brackets after module:

module [Module] mkOrdinary(Empty);
module [ModuleCollect#(item_type)] mkCollector(Empty);

ModuleCollect is an advanced mechanism that gathers items other than state and rules during elaboration. Most designs only need plain Module.

10. Common mistakes

10.1 Writing readiness as an if in the body

// Wrong: push is always ready
method Action push(Bit#(8) x);
  if (depth < 2) begin
    stored <= x;
    depth  <= depth + 1;
  end
endmethod

// Right: callers stop at the limit
method Action push(Bit#(8) x) if (depth < 2);
  stored <= x;
  depth  <= depth + 1;
endmethod

An if in the body cannot block the method, so the calling rule keeps firing. Make this change in the example of section 7, extend report's condition to b.full && sent == 13, and run it: fill still fires in the cycle where depth is 2 and prints pushed 12, top now 11. The 12 was never stored, but fill's print and its update of sent happened anyway.

10.2 Mentioning a method argument in its readiness condition

// Wrong: the readiness condition cannot see arguments
method Action push(Bit#(8) x) if (x < 100);

// Right: check the argument in the body
method Action push(Bit#(8) x) if (depth < 2);
  if (x < 100) stored <= x;
endmethod

Readiness tells a caller whether it may call the method before it chooses any argument, so the condition cannot refer to arguments. If it does, bsc reports T0004, Unbound variable `x'.

10.3 Copying a method's readiness into its callers

// Wrong: push has no condition; the caller checks instead
method Action push(Bit#(8) x);
  ...
endmethod
rule fill (depth < 2);
  b.push(sent);
endrule

// Right: the condition lives on the method
method Action push(Bit#(8) x) if (depth < 2);
  ...
endmethod
rule fill;
  b.push(sent);
endrule

A caller's condition protects only that caller. The moment another rule calls the same method, nothing stops it from going past the limit. If a rule's explicit condition is true but it does not fire, check the readiness of every method on its call path first.

11. Summary

12. Check your understanding

1. A rule calls inq.first and inq.deq and has no explicit condition. What happens while inq is empty?

   Show answer

   The implicit conditions of first and deq are false, so the whole rule is not ready and does not fire. BSV never skips only the call that is not ready.

2. A rule with no explicit condition stops firing at some point. Where should you look first?

   Show answer

   At the implicit conditions of the methods it calls. If any method along its call chain is not ready, the whole rule is disabled.

3. Why can't you put (* synthesize *) directly on mkStack, whose element type is a parameter?

   Show answer

   A synthesis boundary turns the interface into ports, so every type and width must be known. Synthesize a wrapper that provides a concrete type such as StackIfc#(Bit#(8)).

The Practice problem below has a caller that keeps going past the limit it should stop at; decide first whether the broken contract is the method kind, when a read happens, or readiness.