A SAT solver implementation in VHDL, team tussle
VHDL Python
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.
doc Updated gitignore and new files Apr 13, 2016
src Restructed the whole directory after final submission Apr 13, 2016
tests Updated gitignore and new files Apr 13, 2016
.gitignore Add License Apr 13, 2016
LICENSE Add License Apr 13, 2016
README.md Add MIT License Apr 13, 2016



A hardware SAT solver implementation in VHDL for our CS 254: Digital Logic Design course project under the guidance of Prof. Supratik Chakraborty. The team name of the members tussle, hence the name tusSAT.


You can add the sources to a project and use tusSAT_top.vhd as your top module.
You can get ready-to-import project here https://cse.iitb.ac.in/~sumith/projects/tusSAT.tar.gz.


Our project documentation is in the doc section. The code has inline comments added too.


The tests are in tests subdirectory. The testbench are some select testbenches mostly from DIMACS Satisfiability challenges. You can also generate your .vhd testbench for your own boolean expression using syntestbench.py. This converts the given boolean expression to a .vhd testbench. This has SymPy as it's dependency. More detailed instructions can be found in it's readme.

Open source

The project will be maintained open source under MIT license.
We are welcome for contributions and design suggestions. We are also open to very general VHDL suggestions as we are rookies in this area. Please open an issue in this repository or ping us.
If you send in a PR, ping @Sumith1896 or @shubham-goel for review.