Multiplexer model for RTL satisfiability using MILP

Abstract

New approaches to the satisfiability problem (SAT) for register transfer level (RTL) designs combine arithmetic blocks with Boolean logic to form a mixed integer linear program (MILP). Two-to-one multiplexers with word-level inputs can be decomposed to logic gates, but it is more efficient to describe them in MILP constraints as arithmetic operators. Larger multiplexers are built using a multilevel selection tree. However, such an approach should be improved to optimise the overall efficiency in solving the SAT problem. Proposed is a new MILP model for multiplexers. Experimental results indicate a 50% decrease in the number of constraints and a reduction in MILP complexity from Omega(N-2.4) to Omega(N-1.7), measured in CPU time.