A geometric approach to register transfer level satisfiability

Héctor Navarro1,  Saeid Nooshabadi2,  Juan A. Montiel-Nelson1,  Víctor Navarro-Botello1,  J. Sosa1,  José C. García1
1Institute for Applied Microelectronics, Univ. of Las Palmas de Gran Canaria, Spain, 2Gwangju Institute of Science and Technology, Republic of Korea


In this paper, inequalities of integer hull polyhedrons are used in mixed integer linear programming (MILP) to model the behavior of combinational subsystems, introducing a new solution for the satisfiability (SAT) problem at register transfer level (RTL). Since in these models the vertexes are located at integer positions, they can be used with linear programming (LP) to solve SAT problems. Unfortunately, when combining together several models to make up a compound RTL description, internal vertexes may appear forcing to declare one or more variables as integer. However, the use of these models inside an RTL SAT problem reduces the number of branches needed to solve the whole integer problem. Results show a CPU solution time reduction greater than one order of magnitude, growing with the size of the problem.