This repository contains source codes of the hardware description language (HDL) VeriFormal, an executable simulator in OCaml and a translator that translates codes in Verilog to VeriFormal. The Isabelle/HOL source code of the HDL VeriFormal is given in the VeriFormal.zip. The C++ source code of the translator is given in Verilog-HOL translator.zip
This development in Isabelle/HOL and C++, including VeriFormal and its translater, is free software and can be used, redistributed and/or modified under the terms of the GNU General Public License as published by the Free Software Foundation: either version 3 of the License, or any later version.