Building hada binary requires cabal being available in the system. To build hada, invoke at the project root directory
cabal build hada
Once the building is done, hada binary can be found at dist/build/hada/hada. Copy it to somewhere the system searches for executable binaries.
Use example/Plus.hs as the first example. This file redefines the
integer plus function (+)
as a new binding plus
, as shown below.
module Plus (plus) where
plus :: Int -> Int -> Int
plus = (+)
Invoking
hada path/to/examples/plus.hs -t plus
will generate a SystemVerilog file plus.sv at the same directory, whose content is the same as below.
module plus (output longint o_a1by,
input longint eta_B2,
input longint eta_B1);
always_comb o_a1by = eta_B2 + eta_B1;
endmodule
The argument -t plus
is mandatory, to specify the top binding to
be converted to SystemVerilog. In the example, it is the only
binding plus
. And the top binding is exported into a SystemVerilog
module of the same name.
plus
is defined in a functional flavor known as η-reduced that no
explicit argument is given. However, SystemVerilog always requires
explicit input/output signals to be declared. So two input signals
are added automatically to the exported module, with names
beginning with eta_
. An output signal beginning with o_
is also
created automatically.
Verification is as critical an issue as design implementation in electrical system design. hada provides verification flow based on Verilator. The idea is, hada converts the design from Haskell to SystemVerilog, which is further translated into a C++ simulator by verilator. Finally the C++-based simulator is included back into Haskell as an FFI function. All the verifications are done in Haskell domain.
hada can generates two wrapper files to ease the inclusion of the C++ simulator. One is a C++ file that includes a function for passing input values to the C++ simulator and retrieving the simulator result. The other is a Haskell file that include the C++ wrapper function as an FFI function.
Invoking hada with -w wrapper_file_prefix
will generate the two
wrapper files. For this example, invoke hada as
hada path/to/examples/plus.hs -t plus -w Wplus
creates two files Wplus.cpp and Wplus.hs whose contents are shown below.
#include <verilated.h>
#include <cstdint>
#include "Vplus.h"
extern "C" {
int64_t plus (int64_t eta_B2,
int64_t eta_B1) {
Vplus *top = new Vplus;
top->eta_B2 = eta_B2;
top->eta_B1 = eta_B1;
top->eval();
int64_t o_a1by = top->o_a1by;
top->final();
delete top;
return o_a1by;
}
}
{-# LANGUAGE ForeignFunctionInterface #-}
module Wplus (plus) where
import GHC.Types
foreign import ccall "plus" plus :: Int-> Int -> IO Int
The wrapper file prefix determines not only the C++ and Haskell wrapper files’ base names, but also the name of the module enclosing the FFI function. According to Haskell syntax, the base name of the wrapper prefix must begin with a capital letter.
The FFI function’s result type is IO Int
. Function result is
retrieved from IOMonad as it is generated by running the C++
simulator.
Now we can do a simple verification that compares the translated and verilated function with the original function as illustrated in examples/TestPlus.hs, whose contents are shown below.
import System.Exit
import Plus
import qualified Wplus
main = do test <- 12 `Wplus.plus` 34
let golden = 12 `plus` 34
if test == golden
then exitSuccess
else exitFailure
To build the test binary, the following steps are necessary.
- Invoke hada to generate plus.sv and two wrapper files Wplus.cpp and Wplus.hs.
- Generate the simulator C++ library by invoking verilator.
- Compile Wplus.cpp to an object Wplus.cpp.o.
- Compile verilator’s library object verilated.o.
- Use GHC to compile the verification code TestPlus.hs and link it with all the generated objects.
- Run the verification binary.
Please refer to examples/Plus.mk for the exact command and options for each steps.