A new image computation method based on generalized cofactor of binary decision diagrams

摘要

In the paper, we show a new image computation method based on the BDD constrain operator. The image computation is to compute the next state set from the current state set using the logic functions, and is widely used in the formal 'verification of sequential circuits. We have shown a property on the relation between the constrain operator and the conjunction operator for transition relations of state variables. The constrain operator can reduce BDD node size compared with the conjunction operator. The new method outperforms for several ISCAS benchmarks comparing recent conjunction based methods.