VLSI design: CP, SAT and SMT approaches

In the last couple of decades we have been witnessing a trend of shrinking and miniaturization of electronic components (transistors). Indeed, having smaller components allows to fit more of them in a given area; on the other hand, smaller transistors allows to obtain a smaller chip (in terms of area) with the same computational capabilities of a chip which uses bigger transistors. This process is called Very large-scale integration (VLSI), that is, the process of designing an integrated circuit by embedding millions or even billions of transistors on a single silicon semiconductor microchip. Given the huge number of components involved, the development of smart techniques to address this process has become critical for developing modern-day devices.

This repository describes a Combinatorial Optimization approach to the VLSI problem. In particular, three different technologies are employed to address the problem at hand, namely Constraint Programming (CP), propositional SATisfiability (SAT) and Satisfiability Modulo Theories (SMT).

Requirements

The following packages are required:

• minizinc
• z3-solver
• matplotlib
• numpy

You can install them on your own, or use the provided requirements.txt file to install them by running

$ pip install -r requirements.txt

Usage

All the solvers are executed by launching the main.py file and supplying the required technology (CP, SAT, SMT). All the other parameters are optional.

python main.py technology [-h] [-s START] [-e END] [-t TIMEOUT] [-v] [-a] [-r]
               [--solver SOLVER] [--heu HEU] [--restart RESTART]
               [--sat-search]
               [--smt-model SMT_MODEL]

Command line arguments:

Argument	Description
technology	The technology solver to use (CP/SAT/SMT)
-h, --help	Shows help message
-s START, --start START	First instance to solve (default: 1)
-e END, --end END	Last instance to solve (default: 40)
-t TIMEOUT, --timeout TIMEOUT	Sets the timeout (ms, default: 300000)
-v, --verbose	Enables verbose output (default: false)
-a, --no-area	Disables sorting circuits by area before feeding them to the solver
-r, --rotation	Enables circuits rotation (default: false)
--solver SOLVER	(CP ONLY) CP solver to use (gecode/chuffed, default: chuffed)
--heu HEU	(CP ONLY) CP search heuristic (0/1/2, default: 0)
--restart RESTART	(CP ONLY) CP restart strategy (0/1/2, default: 1)
--sat-search	(SAT ONLY) Enables Z3 custom search (default: false)
--smt-model SMT_MODEL	(SMT ONLY) SMT model to use (base/array, default: base)