Skip to content
Verilog development and verification project for HOL4
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
ag32 term-eqtype fixes Feb 18, 2019
cakeml_connection Fix wordcountVerilogProof build error Feb 21, 2019
regexp Some documentation updates Feb 18, 2019
verilog_glue Some documentation updates Feb 18, 2019
LICENSE BSD 3-clause license Aug 20, 2018
hardwareMiscScript.sml Regexp example + extended array support in translator Dec 18, 2018

Verilog development and verification project for HOL4

Installation and setup

The development requires HOL4.

Ag32-specific setup

To build Ag32-related theories, such as the processor itself and cakeml_connection, you need to point $CAKEMLDIR to your CakeML compiler directory.

ISA generation

Translating the Silver ISA from L3 to HOL is not necessary as the already-translated ISA stored in the CakeML compiler project is used.

However, after updating the L3 ISA the following steps are required to update the HOL ISA.

First, make sure you have L3 installed.

With L3 installed, the following command in the L3 REPL (named l3, located in the bin directory in your L3 directory) will produce the HOL ISA from the L3 ISA:

HolExport.spec ("ag32.spec", "ag32");
You can’t perform that action at this time.