Simplifying circuits for formal verification using parametric representation

IH Moon, HH Kwak, J Kukula, T Shiple… - … Conference on Formal …, 2002 - Springer
IH Moon, HH Kwak, J Kukula, T Shiple, C Pixley
International Conference on Formal Methods in Computer-Aided Design, 2002Springer
We describe a new method to simplify combinational circuits while preserving the set of all
possible values (that is, the range) on the outputs. This method is performed iteratively and
on the fly while building BDDs of the circuits. The method is composed of three steps; 1)
identifying a cut in the circuit, 2) identifying a group of nets within the cut, 3) replacing the
logic driving the group of nets in such a way that the range of values for the entire cut is
unchanged and, hence, the range of values on circuit outputs is unchanged. Hence, we …
Abstract
We describe a new method to simplify combinational circuits while preserving the set of all possible values (that is, the range) on the outputs. This method is performed iteratively and on the fly while building BDDs of the circuits. The method is composed of three steps; 1) identifying a cut in the circuit, 2) identifying a group of nets within the cut, 3) replacing the logic driving the group of nets in such a way that the range of values for the entire cut is unchanged and, hence, the range of values on circuit outputs is unchanged. Hence, we parameterize the circuit in such a way that the range is preserved and the representation is much more efficient than the original circuit. Actually, these replacements are not done in terms of logic gates but in terms of BDDs directly. This is allowed by a new generalized parametric representation algorithm to deal with both input and output variables at the same time. We applied this method to combinational equivalence checking and the experimental results show that this technique outperforms an existing related method which replaces one logic net at a time. We also proved that the previous method is a special case of ours. This technique can be applied to various other problem domains such as symbolic simulation and image computation in model checking.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果