State encoding of asynchronous controllers is a challenging problem that faces a vast space of solutions. Subtle differences in the insertion of signals may result in significant variations in the complexity of the logic. This paper proposes a novel approach that models the encoding problem as Pseudo-Boolean formula. A cost function that estimates the complexity of the logic is incorporated, where the estimator of essential literals becomes one of the most important terms of the function. The new approach has been tested in 175 benchmarks with encoding conflicts, including 127 four-phase latch controllers. The presence of logic estimators in the formula contributes to an average reduction of 43% in literals when compared to a plain SAT version of the problem, at the expense of a longer runtime. When comparing to the region-based approach in petrify, an average reduction of 14% in literals is obtained.

Peer Reviewed