Guarded module


In [1]:
open HardCaml
open Signal.Comb
open Signal.Seq
open Signal.Guarded
open Signal.Types

The guarded module provides a small DSL to describe something similar to VHDL processes or Verilog always blocks.

Here's the up-down counter from an earlier tutorial described this way.


In [2]:
let up_down_counter clear up down = 
    let counter = g_reg  { r_sync with reg_clear = clear } empty 8 in
    let () = compile [
        g_when (up ^: down) [
            g_when (up) [ counter $== counter#q +:. 1 ];
            g_when (down) [ counter $== counter#q -:. 1 ];
        ]
    ] in
    counter#q


Out[2]:
val up_down_counter : t -> t -> t -> t = <fun>

This compares to VHDL as follows

architecture rtl ...
    signal counter : unsigned(7 downto 0);
begin
    process (clock) 
    begin
        if rising_edge(clock) then
            if clear='1' then
                counter <= (others=>'0');
            else
                if up xor down then
                    if up then 
                        counter <= counter + 1;
                    end if;
                    if down then 
                        counter <= counter - 1;
                    end if;
                end if;
            end if;
        end if;
    end process;
end architecture;

The first difference to note is in HardCaml the type of a guarded variable is specified before the assignments section. In VHDL (and Verilog) this is inferred using a template (sensitivity list and rising_edge). The two main functions for constructing these guarded values are g_reg and g_wire. The former describes a register which holds it's value between clock cycles. The later is for combinatorial values (a default value is provided for when there is no assignment). Here lies a useful distinction between HardCaml and VHDL/Verilog - registered and combinatorial values may be updated in the same code block.

The logic in HardCaml is specified within the list passed to the compile function. What goes into this list constitutes the Guarded DSL. The compile function takes the DSL and turns it back into structural RTL.

The main idea is to provide if/switch like statements to control when assignments occur to guarded variables.


In [3]:
g_if


Out[3]:
- : t -> statements -> statements -> statement = <fun>

g_if takes a control signal and 2 lists of guarded statements to execute dependant on the control signal. g_switch is similar except it allows multiple paths of control flow.


In [4]:
g_switch


Out[4]:
- : t -> t cases -> statement = <fun>

To actually perform assignments we use this operator.


In [5]:
($==)


Out[5]:
- : variable -> t -> statement = <fun>

The final thing to note is the only place where a guarded variable is actually allowed is the on the left hand side of an assignment. Everywhere else you use either standard HardCaml signals or other statement types. You can read guarded variables from code blocks (or outside them) using the #q method.


In [6]:
let x = g_wire gnd


Out[6]:
val x : variable = <obj>

In [7]:
x#q


Out[7]:
- : t =
Signal_wire ({s_id = 37L; s_names = []; s_width = 1; s_deps = []},
 {contents = Signal_empty})

How values update

guarded variables are not variables in the traditional sense. The semantics are closer to signals in VHDL (or non-blocking assignments in Verilog).

When multiple assignments are executed in a particular control flow within a code block the last one wins. Say we execute the following with x currently set to 1.

x = x + 2
if (true) x = x + 3

With normal variables we would expect a result of 6 (1+2+3). In actual fact we get 4 (1+3) - the x = x + 3 is the (only) statement that affects the final result.

The basic rule is the input value of x is the same for all statements in a code block. The output value (or next value of a wire or register) is the last assignment statement to execute.

Statemachines

One of the main purposes of the guarded module is to describe statemachines. As per VHDL/Verilog this is done with a switch like statement.

For convenience this is wrapped up in a special set of functions.

First here are a couple of interface signals used below.


In [8]:
let start, stall = vdd, gnd
let x = g_wire (consti 8 0)


Out[8]:
val start : t =
  Signal_const ({s_id = 1L; s_names = ["vdd"]; s_width = 1; s_deps = []},
   "1")
val stall : t =
  Signal_const ({s_id = 2L; s_names = ["gnd"]; s_width = 1; s_deps = []},
   "0")
Out[8]:
val x : variable = <obj>

This statement defines the statemachine. It returns the function machine used to declare the statemachine and state used to set the next state. The hidden value is the state register itself (not all that useful in most cases).


In [9]:
let _,machine,state = statemachine r_sync enable [ `One; `Two; `Three ]


Out[9]:
val machine : _[> `One | `Three | `Two ] cases -> statement = <fun>
val state : _[> `One | `Three | `Two ] -> statement = <fun>

Now for the statemachine. Note that the result of the machine function is just a guarded statement and it can be surrounded by arbitrary other statements (or other statemachines).


In [10]:
compile [
    machine [
        `One, [
            x $==. 10;
            g_when start [ state `Two; ];
        ];
        `Two, [
            x $==. 20;
            state `Three;
        ];
        `Three, [
            x $==. 30;
            g_when stall [ state `One; ];
        ];
    ];
]


Out[10]:
- : unit = ()