The goal of this project is to verify the correctness of a 32-bit Brent-Kung adder circuit and a 32-bit Ladner-Fischer adder circuit. Both of these are tree adders designed to be fast for adding two numbers together at the expense of size and complexity. Verifying correctness of any 32-bit adder circuit is challenging because there are 2^64 possible inputs and doing an exhaustive simulation would take an enormous amount of time. Using HOL will make a correctness proof more manageable than an exhaustive simulation.
The project is complete. The the HOL-style netlist generator is done, the sat-based tactic is done, and the goals have been proved.
report.pdf | Project Report PDF. |
setup.sml | Project setup SML file. This file setups up the required definitions and tactics for the project. |
adders.sml | HOL-style netlists of all of the prefix and ripple-carry adder circuits. |
goals.sml | Final HOL goals for the project. |
holnetlist | Perl script to generate HOL-style netlists from Verilog netlists. |
BrentKung32.v | Verilog netlist of a 32-bit Brent-Kung adder. |
BrentKung16.v | Verilog netlist of a 16-bit Brent-Kung adder. |
LadnerFischer32.v | Verilog netlist of a 32-bit Ladner-Fischer adder. |
LadnerFischer16.v | Verilog netlist of a 16-bit Ladner-Fischer adder. |
proposal.pdf | The original project proposal. |
BrentKung32.sml | HOL-style netlist of a 32-bit Brent-Kung adder generated by holnetlist. |
BrentKung16.sml | HOL-style netlist of a 16-bit Brent-Kung adder generated by holnetlist. |
LadnerFischer32.sml | HOL-style netlist of a 32-bit Ladner-Fischer adder generated by holnetlist. |
LadnerFischer16.sml | HOL-style netlist of a 16-bit Ladner-Fischer adder generated by holnetlist. |
cells.v | Verilog code for all of the cell used by the adder cicuits. This is required to get holnetlist to work on the above Verilog files. |
test16.v | Verilog test bench for the 16-bit adders. |
test32.v | Verilog test bench for the 32-bit adders. |
testcases16.txt | Sample 16-bit test cases for the Verilog code. |
testcases32.txt | Sample 32-bit test cases for the Verilog code. |