Linear sifting of decision diagrams and its application in synthesis

Abstract

We propose a new algorithm, called linear sifting, for the optimization of decision diagrams that combines the efficiency of sifting and the power of linear transformations. The new algorithm is applicable to large examples, and in many cases leads to substantially more compact diagrams when compared to simple variable reordering. We also show in what sense linear transformations complement variable reordering and how the technique can be applied to verification issues. Going a step further, we discuss a synthesis scenario where-due to the complexity of the target function-it is inevitable to decompose the function in a preprocessing step. By using linear sifting it is possible to extract a linear filter and, hence, to achieve the necessary decomposition. Using this method we were able to synthesize functions with standard tools which fail otherwise.