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]:
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]:
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]:
To actually perform assignments we use this operator.
In [5]:
($==)
Out[5]:
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]:
In [7]:
x#q
Out[7]:
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.
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]:
Out[8]:
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]:
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]: