Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code

Details Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code

2007-10-25

arxiv.org/abs/0710.4689v1

Dans Design, Automation and Test in Europe - DATE'05, Munich : Allemagne (2005)

Computer Science

Logic in Computer Science

Submitted on behalf of EDAA (http://www.edaa.com/)

Scientific paper

Development of energy and performance-efficient embedded software is increasingly relying on application of complex transformations on the critical parts of the source code. Designers applying such nontrivial source code transformations are often faced with the problem of ensuring functional equivalence of the original and transformed programs. Currently they have to rely on incomplete and time-consuming simulation. Formal automatic verification of the transformed program against the original is instead desirable. This calls for equivalence checking tools similar to the ones available for comparing digital circuits. We present such a tool to compare array-intensive programs related through a combination of important global transformations like expression propagations, loop and algebraic transformations. When the transformed program fails to pass the equivalence check, the tool provides specific feedback on the possible locations of errors.

Affiliated with

Also associated with

No associations

Rating

Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-431809