Formal Verification of Optimizing Transformations during High-level Synthesis
| Autor: | Chandan Karfa, Purandar Bhaduri, Ramanuj Chouksey |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Bounded model checker
Computer science Computation Formal equivalence checking 0211 other engineering and technologies Translation validation 02 engineering and technology 020202 computer hardware & architecture Scheduling (computing) High-level synthesis 0202 electrical engineering electronic engineering information engineering Algorithm Formal verification 021106 design practice & management Counterexample |
| Zdroj: | ISEC |
| DOI: | 10.1145/3299771.3299797 |
| Popis: | Translation validation is the process of proving that the target code is a correct translation of the source program being compiled. In this work, we propose a translation validation method to verify code motion transformations involving loops applied during the scheduling phase of high-level synthesis (HLS). Our method is capable of ignoring false computations during translation validation. In this work, we show that how to generate a counter-trace (cTrace) using the internal information of verifier in the case of non-equivalence reported by a translation validation method. We also show how a Bounded Model Checker (CBMC) can be used to find a counterexample for a given cTrace. Experimental results demonstrate the usefulness of our method. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|