Sequential logic add the notion of time and state to HardCaml. It basically boils down to a few functions for describing registers and memories. Simulation, however, now becomes necessary - there is no shallow embedding equivalent for sequential logic.
The sequential world lives in the HardCaml.Signal.Seq module.
In [1]:
open HardCaml
open Signal.Comb
open Signal.Seq
and most useful function here is reg
In [2]:
reg
Out[2]:
This takes a register specification, clock enable and input signal and returns the input signal delayed by 1 clock cycle.
In [3]:
let d = wire 8
let q = reg r_sync enable d
Out[3]:
Out[3]:
The enable signal can be any arbitrary 1 bit signal, including constants like vdd or (less usefully) gnd or even empty (which is equivalent to vdd).
The r_sync structure used above is one of a few predefined register specifications; r_none, r_async, r_sync and r_full. Through this structure you can configure the exact details of the register you want to describe. The predefined ones correspond to
r_none no reset or clearr_sync synchronous clearr_async asynchronous resetr_full asynchronous reset and synchronous clearHere's the structure in all it's gory details:
and register =
{
reg_clock : signal; (* clock *)
reg_clock_level : signal; (* active clock edge *)
reg_reset : signal; (* asynchronous reset *)
reg_reset_level : signal; (* asynchronous reset level *)
reg_reset_value : signal; (* asynchronous reset value *)
reg_clear : signal; (* synchronous reset *)
reg_clear_level : signal; (* synchronous reset level *)
reg_clear_value : signal; (* sycnhronous reset value *)
reg_enable : signal; (* global system enable *)
}
and this is how r_sync is defined
let r_sync =
{
reg_clock = clock; (* clock signal *)
reg_clock_level = vdd; (* rising edge *)
reg_reset = empty; (* no asyncronous reset *)
reg_reset_level = empty;
reg_reset_value = empty;
reg_clear = clear; (* synchronous clear *)
reg_clear_level = vdd; (* active high *)
reg_clear_value = empty;
reg_enable = empty;
}
Through this structure we can;
reg function is merged (anded) with the global enable given here, if any.It's probably worth asking why things are done this way. The idea is that there can be central place to set up register types which can then be globally changed to suit different FPGA/ASIC architectures.
There are a couple of other useful register oriented functions built using reg.
pipeline n spec enable d delays the input by n cycles (n>=0).
In [4]:
pipeline
Out[4]:
reg_fb is a convenient way of creating feedback loops around a register.
In [5]:
reg_fb
Out[5]:
rather than provide some input data to register the function takes the required width and a function which takes the current register value and returns the next one.
In [6]:
reg_fb r_sync enable 8 (fun d -> d +:. 1)
Out[6]:
its worth looking at how this function is implemented
In [7]:
let my_reg_fb spec enable width f =
let w = wire width in
let q = reg spec enable (f w) in
w <== q;
q
Out[7]:
wires are what allow us to use a signal before it has been fully defined. The following (illegal in OCaml) code is what we are trying to achieve.
In [8]:
let rec q = reg r_sync enable d
and d = q +:. 1
Out[8]:
The basic primitive for building memories in HardCaml is
In [9]:
memory
Out[9]:
From a RTL point of view describes an array. The we, w and d signals perform a synchronous write of d at address w when we is enabled. r provides the address for an asynchronous read the value of which is returned.
The spec argument allows the array to be reset if required though for memories this will usually be r_none which doesn't include a reset.
Finally size gives the number of elements in the memory. The widths of the r and w addresses are checked against size and must be consistent.
This primitive is sufficient to describe the asynchronous LUT based memories in FPGA devices ie memory 16 r_none ....
RAMs require a synchronous read port. This is achieved by registering either the read address (write before read) or memory output (read before write). Which is most appropriate depends on the target technology.
In [10]:
ram_rbw
Out[10]:
In [11]:
ram_wbr
Out[11]:
These have very similar interfaces to the memory primitive with the addition of re - the read enable.
If the read and write addresses correspond to the same signal these functions will describe a single port RAM. Otherwise they describe a dual port RAM with 1 read and 1 write address.
More complex RAM requirements (true dual port FPGA RAMs, for example) need to be instantiated using vendor libraries or core generators.