Counter‐example generation procedure for path‐based equivalence checkers

Path‐based equivalence checkers (PBECs) have been successfully applied for verification of programmes from diverse domains and from various stages of high‐level synthesis. In the case of non‐equivalence, PBEC provides very little information which is not sufficient for further investigation of the two programmes being compared by some human expert. In this work, the authors show how a counter‐trace ( cTrace ) can be generated in the case of non‐equivalence reported by the PBEC. Using this cTrace , they also present a procedure to find suitable initialisation values for input variables which reveal the non‐equivalence (i.e. counter‐example) by using off‐the‐shelf satisfiability modulo theories (SMT) solvers. To aid the human expert, they also show that how they can visualise this cTrace in the control and data‐flow graph of the programmes using the graph visualisation software – Graphviz. This counter‐example and visual representation of the corresponding cTrace will be helpful in debugging the root cause of the non‐equivalence. The experimental results are encouraging.