Multiplexer model for RTL satisfiability using MILP
H. Navarro, Juan Antonio Montiel-Nelson, Javier Sosa, J.C. García, D.Q.M. Fay · Electronics Letters · 2004
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 Ω(N2.4) to Ω(N1.7), measured in CPU time.