Probabilistic equivalence checking based on high-level decision diagrams

The paper proposes a novel method for probabilistic equivalence checking of digital systems. The method is based on representing the high-level decision diagrams as the model of digital systems by the sets of characteristic polynomials. It is shown that this representation is canonical, i.e. the sets of polynomials for equivalent diagrams are the same up to the names of the variables. However, computing the full set of polynomials is unfeasible for large diagrams as it demands checking all assignments to the control variables. In order to cope with this problem we have developed a polynomial algorithm for probabilistic equivalence checking.