Translation Validation of Scheduled Conditional Behavior using Petri Net based Program Models Rakshit Mittal 0 2 Soumyadip Bandyopadhyay 0 1 BITS Pilani, KK Birla Goa Campus , Goa, 403726 India Hasso-Platner Institute , Potsdam, 14482 Germany Telecom Paris, Institut Polytechnique de Paris , 91120 France -

cut-points to a cut-point without intermediary cut-points. Similarly in Fig. 1(d), cut-points are fp01; p02; p03; p04; p05; p06; p07; p08; p09; p011; p012; p013; p015g; the path cover, 1 = f 1 = hft01gi, 2 = hft04gi, 3 = hft03gi, 4 = hft02gi, 5 = hft05g; ft07gi, 6 = hft06gi, 7 = hft07gi, 8 = hft08gig.

The notion of equivalence checking is as follows: \8 paths 2 0 9 an equivalent path in 1 and vice-versa". A path-based equivalence checking module takes these sets of paths for both the Petri net models, and using the concept of path merging as well as extension of paths that we have developed, checks for equivalence between the paths and returns a Yes/No answer for the semantic equivalence between source and translated programs. The module does not give a false positive result, but since the approach is not complete, a `No' answer is interpreted as `Can't Say'. Equivalence between two expressions is checked using the Z3 SMT solver [ 3 ]. Using this approach the set of equivalent pairs of paths is fh 1; ( 1 4)i; h 2; 2jj 3i; h 3; 5i; h 4; 6i; h 5; 7i; h 6; 8ig

Capabilities and limitations: Our approach can handle several uniform and non-uniform code optimizing and parallelizing transformations for scalar programs. The major limitation of our method is that it cannot validate array handling programs. The method also incapable to validate loop shifting class of transformations.

 1. Chouksey , R. , Karfa , C. : Veri cation of scheduling of conditional behaviors in highlevel synthesis . IEEE Trans. on Very Large Scale Integration (VLSI) Systems ( 2020 ) 2. Mittal , R. , Banerjee , R. , Sarkar , S. , Bandyopadhyay , S. : Translation validation of loop involving code optimizing transformations using petri net based models of programs . In: PNSE 2020 . vol. 2651 , pp. 138 { 146 . CEUR-WS.org ( 2020 ) 3. Moura , L.D. , Bj rner, N.: Z3: an e cient smt solver . In: TACAS'08/ETAPS'08 Proceedings of the Theory and Practice of Software . pp. 337 { 340 ( 2008 )