Skip to main content

Deriving bisimulation relations from path based equivalence checkers

Abstract

Translation validation is an undecidable problem. Bisimulation relation based approaches, nevertheless, have been widely successful in translation validation of programs albeit with some drawbacks. These drawbacks include non-termination of the verification methodology and significant restrictions on the structures of programs to be checked for equivalence. We have developed a path based equivalence checker which propagates mismatched values over consecutive paths to alleviate these drawbacks. In this work, we show how a bisimulation relation between a program and its translated version can be constructed from the outputs of such a value propagation based equivalence checker. Moreover, none of the earlier methods that establish equivalence through construction of bisimulation relations has been shown to tackle code motions across loops; the present work demonstrates, for the first time, the existence of a bisimulation relation under such a situation.

This is a preview of subscription content, access via your institution.

References

  1. BKSM12

    Banerjee K, Karfa C, Sarkar D, Mandal C (2012) A value propagation based equivalence checking method for verification of code motion techniques. In: ISED, pp 67–71

  2. BKSM14

    Banerjee K, Karfa C, Sarkar D, Mandal C (2014) Verification of code motion techniques using value propagation. IEEE Trans. CAD ICS 33(8): 1180–1193

    Article  Google Scholar 

  3. BSM14

    Banerjee K, Sarkar D, Mandal C (2014) Extending the FSMD framework for validating code motions of array-handling programs. IEEE Trans. on CAD of ICS 33(12): 2015–2019

    Article  Google Scholar 

  4. Cam91

    Camposano R (1991) Path-based scheduling for synthesis. IEEE Trans CAD ICS 10(1): 85–93

    Article  Google Scholar 

  5. DH00

    Darte A, Huard G (2000) Loop shifting for loop compaction. J Parallel Programm 28(5): 499–534

    Article  Google Scholar 

  6. Flo67

    Floyd RW (1967) Assigning meaning to programs. In: Proceedings the 19th symposium on applied mathematics, pp 19–32

  7. GDWL92

    Gajski DD, Dutt ND, Wu AC-H, Lin SY-L (1992) High-level synthesis: introduction to chip and system design. Kluwer Academic Publishers, Norwell, MA

  8. KLG08

    Kundu S, Lerner S, Gupta R (2008) Validating high-level synthesis. In: CAV, pp 459–472

  9. KLG10

    Kundu S, Lerner S, Gupta R (2010) Translation validation of high-level synthesis. IEEE Trans CAD ICS 29(4): 566–579

    Article  Google Scholar 

  10. KMS+06

    Karfa C, Mandal C, Sarkar D, Pentakota SR, Reade C (2006) A formal verification method of scheduling in high-level synthesis. In: ISQED, pp 71–78

  11. KMS12

    Karfa C, Mandal C, Sarkar D (2012) Formal verification of code motion techniques using data-flow-driven equivalence checking. ACM Trans. Des. Autom. Electr. Syst. 17(3): 30

    Google Scholar 

  12. KRS92

    Knoop J, Ruthing O, Steffen B (1992) Lazy code motion. In: PLDI, pp 224–234

  13. KSM10

    Karfa C, Sarkar D, Mandal C (2010) Verification of datapath and controller generation phase in high-level synthesis of digital circuits. IEEE Trans. CAD ICS 29(3): 479–492

    Article  Google Scholar 

  14. KSMK08

    Karfa C, Sarkar D, Mandal C, Kumar P (2008) An equivalence-checking method for scheduling verification in high-level synthesis. IEEE Trans CAD ICS 27: 556–569

    Article  Google Scholar 

  15. LGLT13

    Li T, Guo Y, Liu W, Tang M (2013) Translation validation of scheduling in high level synthesis. In: GLSVLSI, pp 101–106

  16. LSHJ11

    Lee C-H, Shih C-H, Huang J-D, Jou J-Y (2011) Equivalence checking of scheduling with speculative code transformations in high-level synthesis. In: ASP-DAC, pp 497–502

  17. Nec00

    Necula GC (2000) Translation validation for an optimizing compiler. In: PLDI, pp 83–94

  18. PSS98

    Pnueli A, Siegel M, Singerman E (1998) Translation validation. In: TACAS, pp 151–166

  19. Rin99

    Rinard M (1999) Credible compilation. Technical report. In: Proceedings of CC 2001: International Conference on Compiler Construction

  20. RJ95

    Rahmouni M, Jerraya AA (1995) Formulation and evaluation of scheduling techniques for control flow graphs. In: EURO-DAC, pp 386–391

  21. RKS00

    Ruthing O, Knoop J, Steffen B (2000) Sparse code motion. In: POPL, pp 170–183

Download references

Author information

Affiliations

Authors

Corresponding author

Correspondence to Kunal Banerjee.

Additional information

Communicated by Jin Song Dong

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Banerjee, K., Sarkar, D. & Mandal, C. Deriving bisimulation relations from path based equivalence checkers. Form Asp Comp 29, 365–379 (2017). https://doi.org/10.1007/s00165-016-0406-y

Download citation

Keywords

  • Translation validation
  • Bisimulation relation
  • Path based equivalence checker
  • Value propagation