A novel formal approach to generate high-level test vectors without ILP and SAT solvers

摘要

This paper proposes a novel formal method to generate functional test vectors using a hybrid Boolean-word canonical representation called Linear Taylor Expansion Diagram (LTED) [1] rather than utilizing SAT or ILP solvers. Our approach differs from other methods since it not only uses a canonical hybrid representation, but also generates behavioral test patterns from faulty behavior instead of checking the equivalence between the fault-free and faulty designs. After representing the faulty behavior in LTED, based on a beneficial property of this canonical representation, we will be able to distinguish the fault-free portion of the faulty design. Furthermore, it is possible to determine conditions caused the related faults are propagated to at least one of primary outputs. In order to evaluate the performance of the proposed method, it is run on some large industrial designs and experimental results are compared with those of Hybrid SAT (HSAT) approach [2].