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.

Constructing bisimulation relations between programs as a means of translation validation has been an active field of study. The problem is in general undecidable. Currently available mechanisms suffer from drawbacks such as non-termination and significant restrictions on the structures of programs to be checked. We have developed a path extension based equivalence checking method as an alternative translation validation technique to alleviate these drawbacks. In this work, path extension based equivalence checking of programs (flowcharts) is leveraged to establish a bisimulation relation between a program and its translated version by constructing the relation from the outputs of the equivalence checker.

Software designers often apply automatic or manual transformations on the array-handling source programs to improve performance of the target programs. Verdoolaege et al. (Verdoolaege et al., 2012) have proposed a method to automatically prove equivalence of the output arrays of the source and the generated transformed programs. Unlike the other approaches, the method of (Verdoolaege et al., 2012) provides the most sophisticated techniques to validate programs with non-uniform recurrences besides programs with uniform recurrences. However, if the recurrence expressions of the source and the transformed programs refer to more than one base cases of which some are non-equivalent and also if the domain of the output arrays partition based on dependences on different base cases, then some imprecision in the equivalence checking results is observed. The equivalence checker reports that the entire index spaces of the output arrays of the source program to be non-equivalent with that of the transformed program instead of the portion of the output arrays which depend on the non-equivalent base cases of the programs. In the current work, we have enhanced the method of equivalence checking of (Verdoolaege et al., 2012) so that it can precisely indicate the equivalent and non-equivalent portions of the output arrays.

Loop parallelization and loop vectorization of array-intensive programs are two common transformations applied by parallelizing compilers to convert a sequential program into a parallel program. Validation of such transformations carried out by untrusted compilers are extremely useful. This paper proposes a novel algorithm for construction of the dependence graph of the generated parallel programs. The transformations are then validated by checking equivalence of the dependence graphs of the original sequential program and the parallel program using a standard and fairly general algorithm reported elsewhere in the literature. The above equivalence checker still works even when the above parallelizing transformations are preceded by various enabling transformations except for loop collapsing which changes the dimensions of the arrays. To address the issue, the present work expands the scope of the checker to handle this special case by informing it of the correspondence between the index spaces of the corresponding arrays in the sequential and the parallel programs. The augmented algorithm is able to validate a large class of static affine programs. The proposed methods are implemented and tested against a set of available benchmark programs which are parallelized by the polyhedral auto-parallelizer LooPo and the auto-vectorizer Scout. During experiments, a bug of the compiler LooPo on loop parallelization has been detected.

Compiler optimization of array-intensive programs involves extensive application of loop transformations and arithmetic transformations. Hence, translation validation of array-intensive programs requires manipulation of intervals of integers (representing domains of array indices) and relations over such intervals to account for loop transformations and simplification of arithmetic expressions to handle arithmetic transformations. A major obstacle for verification of such programs is posed by the presence of recurrences, whereby an element of an array gets defined in a statement S inside a loop in terms of some other element(s) of the same array which have been previously defined through the same statement S. Recurrences lead to cycles in the data-dependence graph of a program which make dependence analyses and simplifications (through closed-form representations) of the data transformations difficult. Another technique which works better for recurrences does not handle arithmetic transformations. In this work, array data-dependence graphs (ADDGs) are used to represent both the original and the optimized versions of the program and a validation scheme is proposed where the cycles due to recurrences in the ADDGs are suitably abstracted as acyclic subgraphs. Thus, this work provides a unified equivalence checking framework to handle loop and arithmetic transformations along with most of the recurrences -- this combination of features had not been achieved by a single verification technique earlier.

The initial behavioural specification of any software programs goes through significant optimizing and parallelizing transformations, automated and also human guided, before being mapped to an architecture. Establishing validity of these transformations is crucial to ensure that they preserve the original behaviour. PRES+ model (Petri net based Representation of Embedded Systems) encompassing data processing is used to model parallel behaviours. Being value based with inherent scope of capturing parallelism, PRES+ models depict such data dependencies more directly; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like Finite State Machines with Data path (FSMDs) (which are essentially sequential control flow graphs (CFGs)). In this work, a path based equivalence checking method for PRES+ models is presented.

A compiler is a computer program which translates a source code into a target code, often with an objective to reduce the execution time and/or save critical resources. However, an error in the design or in the implementation of a compiler may result in software bugs in the target code obtained from that compiler. Translation validation is a formal verification approach for compilers whereby, each individual translation is followed by a validation phase which verifies that the target code produced correctly implements the source code. In this paper, we present a tool for translation validation of optimizing transformations of programs; the original and the transformed programs are modeled as Finite State Machines with Datapath having Arrays (FSMDAs) and a symbolic value propagation (SVP) based equivalence checking strategy is applied over this model to determine the correctness of the applied transformations. The tool has been demonstrated to handle uniform and non-uniform code motions, including code motions across loops, along with transformations which result in modification of control structures of programs. Moreover, arithmetic transformations such as, associative, commutative, distributive transformations, expression simplification, constant folding, etc., are also supported.

An equivalence checking method of finite state machines with datapath based on value propagation over model paths is presented here for validation of code motion transformations commonly applied during the scheduling phase of high-level synthesis. Unlike many other reported techniques, the method is able to handle code motions across loop bodies. It consists in propagating the variable values over a path to the subsequent paths on discovery of mismatch in the values for some live variable, until the values match or the final path segments are accounted for without finding a match. Checking loop invariance of the values being propagated beyond the loops has been identified to play an important role. Along with uniform and nonuniform code motions, the method is capable of handling control structure modifications as well. The complexity analysis depicts identical worst case performance as that of a related earlier method of path extension which fails to handle code motion across loops. The method has been implemented and satisfactorily tested on the outputs of a basic block-based scheduler, a path-based scheduler, and the high-level synthesis tool SPARK for some benchmark examples.

The finite state machine with datapath (FSMD) models provide a formalism to represent any sequential behavior. Literature has many examples where this model has been successfully applied for behavioral verification of programs. All these methods, however, cannot handle an important class of programs, namely those involving arrays. This limitation is now overcome with finite state machine with datapath having arrays (FSMDA) models which are an extension of FSMD models; the corresponding equivalence checking algorithm has also been enhanced so that code motions of array-intensive behaviors can be validated. The new mechanism has been successfully tested with several examples.

The tagged signal model (TSM) is a formal framework for modeling heterogeneous embedded systems. In the present work, we provide a representation of tagged systems using the semantics of Kleene algebra. We further illustrate mechanisms for both behavioral transformational verification through equivalence checking and property verification of heterogeneous embedded systems based on this algebraic representation.

Loop transformation techniques along with arithmetic transformations are applied extensively on array and loop intensive behaviors in design of area/energy efficient systems in the domain of multimedia and signal processing applications. Ensuring correctness of such transformations is crucial for the reliability of the designed systems. In this paper, array data dependence graphs (ADDGs) are used to represent both the input and the transformed behaviors and the correctness of the transformations is ensured by proving equivalence of the two ADDGs. A slice-based equivalence checking method of ADDGs is proposed for this purpose. The method relies on the normalization of arithmetic expressions and some simplification rules to handle arithmetic transformations. Unlike many other reported techniques, our method is strong enough to handle several arithmetic transformations along with all kinds of loop transformations. Correctness and complexity of the method have been dealt with. Experimental results on several test cases demonstrate the effectiveness of the method.

A formal verification method for checking correctness of code motion techniques is presented in this article. Finite State Machine with Datapath (FSMD) models have been used to represent the input and the output behaviors of each synthesis step. The method introduces cutpoints in one FSMD, visualizes its computations as concatenation of paths from cutpoints to cutpoints, and then identifies equivalent finite path segments in the other FSMD; the process is then repeated with the FSMDs interchanged. Unlike many other reported techniques, the method is capable of verifying both uniform and nonuniform code motion techniques. It has been underlined in this work that for nonuniform code motions, identifying equivalent path segments involves model checking of some data-flow properties. Our method automatically identifies the situations where such properties are needed to be checked during equivalence checking, generates the appropriate properties, and invokes the model checking tool NuSMV to verify them. The correctness and the complexity of the method have been dealt with. Experimental results demonstrate the effectiveness of the method.

This paper proposes a methodology for performance evaluation of schedules for job-shops modeled using tag machines. The most general tag structure for capturing dependences is shown to be inadequate for the task. A new tag structure is proposed. Comparison of the method with existing ones reveals that the proposed method has no dependence on schedule length in terms of modeling efficiency and it shares the same order of complexity with existing approaches. The proposed method, however, is shown to bear promise of applicability to other models of computation and hence to heterogeneous system models having such constituent models.

A formal verification method of the datapath and controller generation phase of a high-level synthesis (HLS) process is described in this paper. The goal is achieved in two steps. In the first step, the datapath interconnection and the controller finite state machine description generated by a high-level synthesis process are analyzed to obtain the register transfer-operations executed in the datapath for a given control assertion pattern in each control step. In the second step, an equivalence checking method is deployed to establish equivalence between the input and the output behaviors of this phase. A rewriting method has been developed for the first step. Unlike many other reported techniques, our method is capable of validating pipelined and multicycle operations, if any, spanning over several states. The correctness and complexity of the presented method have been treated formally. The method is implemented and integrated with an existing HLS tool, called structured architecture synthesis tool. The experimental results on several HLS benchmarks indicate the effectiveness of the presented method.

A formal method for checking equivalence between a given behavioral specification prior to scheduling and the one produced by the scheduler is described. Finite state machine with data path (FSMD) models have been used to represent both the behaviors. The method consists of introducing cutpoints in one FSMD, visualizing its computations as concatenation of paths from cutpoints to cutpoints, and identifying equivalent finite path segments in the other FSMD; the process is then repeated with the FSMDs interchanged. Unlike many other reported techniques, this method is strong enough to work when path segments in the original behavior are merged, a common feature of scheduling. It is also capable of verifying several arithmetic transformations and many code-motion techniques employed during scheduling. Correctness and complexity of the method have been dealt with. Experimental results for several high-level synthesis benchmarks demonstrate the effectiveness of the method.

This paper describes a formal verification methodology of high-level synthesis (HLS) process. The abstraction level of the input to HLS is so high compared to thatof the output that the verification has to proceed hand-in-hand with the synthesis process. The HLS verificationis performed in three phases in this work. The verification method is based on equivalence checking of two finite state machines with data-paths(FSMDs). Unlike most reported works that targets the individual phases independently, the proposed method applies to all these three phases. The method is strong enoughto accommodate control structure modification of the original behaviour, application of several code motion techniques during scheduling and register optimization during register allocation. It can also verify the correctness of the controller. A hand-in-hand synthesis and verification tool SAST has been developed and tested for effectiveness on several HLS benchmark circuits.

This work is concerned with the development of generic, non-intrusive and flexible algorithms for the design of digital circuits with on line testing (OLT) capability. Most of the works presented in the literature on OLT have used single stuck at fault models. However, in deep submicron era single s-a fault models may not capture more than a fraction of the real defects. To cater to the problem it is now advocated that additional fault models such as Bridging faults, Transition faults, Delay faults etc. are also used. The proposed technique is one of the first works that enables on-line detection of bridging faults and provides a high value of n for the n-Detect tests. The technique can handle generic digital circuits with cell count as high as 15,000 and having the order of 2500 states. Results for design of on-line detectors for various ISCAS89 benchmark circuits are provided. The results illustrate that with marginal increase in area overhead, if compared to ones with single s-a fault coverage, the proposed scheme also provides coverage for bridging faults and high value of n for n-Detect coverage.

Verifying a sequential circuit consists in proving that the given implementation of the circuit satisfies its specification. In the present work the input-output specification of the circuit, which is required to hold for the given implementation, is assumed to be available in the form of a Tempura program segment B. It captures the desired ongoing behavior of the circuit in terms of input-output relationships that are expected to hold at various time instants of the interval in question. The implementation is given as a formula W/sub S/ of a first-order temporal equality theory, /spl Fscr/. Goal formulas of the form P /spl sup/ B have been introduced to capture the correctness property of the circuit in question. P is a formula of the equality theory /spl epsiv/ contained in /spl Fscr/ and encodes the initial state(s) of the circuit. A goal reduction paradigm has been used to formulate the proof calculus capturing the state transitions produced along the intervals. Formulas, called verification conditions (VC's), whose validity ensures the correctness of the circuit, are produced corresponding to the output equality statements in B. For finite state machines, VC's are formulas of propositional calculus and, therefore, require no temporal reasoning for their proofs. In fact, since binary decision diagram (BDD) representations are used throughout, their proofs become quite simple. The goal reduction rules proposed for iterative constructs also incorporate synthesis of invariant assertions over the states of the circuit. The proof of a nontrivial example has been presented. The paper concludes with a discussion on a broad overview of the building blocks of the verifier.

Significant modifications of the first-order rules have been developed so that they can be applied directly to algebraic expressions. The importance and implication of normalization of formulas in any theorem prover are discussed. It is shown how the properties of the domain of discourse have been taken care of either by the normalizer or by the inference rules proposed. Using a nontrivial example, the following capabilities of the verifier that would use these inference rules are highlighted: (1) closeness of the proof construction process to the human thought process; and (2) efficient handling of user provided axioms. Such capabilities make interfacing with humans easy.>

Because of the undecidability problem of program verification, it becomes necessary for an automated verifier to seek human assistance for proving theorems which fall beyond its capability. In order that the user be able to interact smoothly with the machine, it is desired that the theorems be maintained and processed by the prover in a form as close as possible to the popular algebraic notation. Motivated by the need of such an automated verifier, which works in an environment congenial to human participation and at the same time uses the methodologies of resolution provers of first-order logic, some inference rules have previously been proposed by the authors (ibid., vol.15, no.1, p.1-9, Jan. 1989) for integer arithmetic, and their completeness issues have been discussed. In the present work, the authors examine how these rules can be applied to quantified formulas vis-a-vis verification of programs involving arrays. An interesting situation, referred to as bound-extension, has been found to occur frequently in proving the quantified verification conditions of the paths in a program. A novel rule, called bound-extension rule, has been devised to consolidate and depict the various issues involved in a bound-extension process. It has been proved that the rule set proposed previously by the authors is adequate for handling a more general phenomenon, called bound-modification, which covers bound-extension in all its entirety.>

An implementation of a rule-based theorem prover for verifying iterative programs over integers is presented. The authors emphasize the overall proof construction strategy of the prover which has been able to construct the correctness proofs of all iterative programs taken from the literature. Two performance measures for the prover are proposed, and its proof construction for an array-sorting program is evaluated using these measures.>