Verification of Prefix Adder
Circuits Using HOL

Introduction

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.

Current Status

The project is complete. The the HOL-style netlist generator is done, the sat-based tactic is done, and the goals have been proved.

Project Files

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.

Other Related Files

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.