Formally analyzing fault tolerance in datapath designs using equivalence checking
Payman Behnam, Bijan Alizadeh, Sajjad Taheri, Masahiro Fujita · 2016
In this paper, we present an efficient formal approach to check the equivalence of synthesized Register Transfer Level (RTL) against the high level specification in the presence of pipelining transformations. With the proposed equivalence checking method, fault tolerance issues when some faults happen in the designs can be formally analyzed. Equivalence checking with the specification can reason about how quickly the design can come back to normal operations when some faults happen. To increase the scalability of our proposed method, we dynamically divide the designs into several smaller parts called segments by introducing dynamic cut-points. Then we employ Modular Horner Expansion Diagram (M-HED) to check whether the specification and the implementation are equivalent or not. Our proposed method enables us to deal with the equivalence checking problem for behaviorally synthesized designs even in the presence of pipelines for nested loops. The empirical results demonstrate the efficiency and scalability of our proposed method in terms of run-time and memory usage for several large designs synthesized by a commercial behavioral synthesis tool. Average improvements in terms of the memory usage and run time in comparison with SMT- and SAT-based equivalence checking are 16.7× and 111.9×, respectively.