BlarneyCheck

An exhaustive property-based testing library for Blarney.

See the associated project report for additional background and documentation.

Usage

Make sure to use the --recursive flag to include the Blarney repo:

> git clone --recursive https://github.com/blarney-lang/blarneycheck.git

Alternatively set the BLARNEY_ROOT environment variable to point at a copy of Blarney.

The library resides in the 'Haskell' directory and can be imported in any Haskell code:

import BlarneyCheck

To compile a module which imports BlarneyCheck use the modified blcc script, instead of blc. Where blcc stands for BlarneyCheck compiler.

Example modules and associated test benches are provided in the 'Examples' directory. These can be simulated as a regression test with:

> ./Test/test.sh

Simulation requires GHC 8.6.5 and Verilator to be installed. The examples are also given as synthesis ready in the 'Synthesizable' directory. Simply:

> cd Examples/Synthesizable
> make <Insert_Example>.sof

This synthesizes the module and test bench. Synthesis requires Quartus to be installed on the system. To program an FPGA with the test bench run:

> make download-sof && nios2-terminal