Transformations on the FSMD of the RTL code with combinational logic statements for equivalence checking of HLS

This paper proposes a transformation on FSMDs, after the high-level synthesis scheduling task, for formal verification of sequential circuits. In previous works, the equivalence checking between an algorithm description and a behavioral RTL, obtained after scheduling, is performed comparing state sequences of the corresponding FSMD models. Several techniques have used segments of state sequences, also known as paths, while others have used deep sequences that carry out complete computations. In both cases, conditional states generate multi sequences. However, none of them have considered that path based scheduling can produce behavioral RTL code with combinational logic composed of conditional and arithmetic operation statements in different variable dependency configurations. In these cases, the conditional statements and their branches may be associated to the same RTL FSMD state transition, causing false negative results of the equivalence checking of state sequences. In this paper, a transformation of the behavioral RTL FSMD model is proposed, in which every conditional statement produce multi sequences of states, being based on variable dependency. Obtained results show that our method is effective for the subsequent application of known equivalence checking schemes.