Validating SPARK: High Level Synthesis Compiler

Embedded systems have found applications in diverse domains. Due to the criticality of their operations, verification of embedded systems is a necessity. With the advancement of multi-core and multiprocessor systems, there has been a paradigm shift to incorporate these features in embedded systems as well. The initial behavioural specification of a system goes through significant optimizing transformations using automated high level synthesis (HLS) compiler like SPARK, before being mapped to an architecture. Establishing the validity of these transformations is crucial to ensure that correct optimizations are applied during synthesis. To model parallel behaviours, especially in embedded systems, the use of PRES+ models is advocated for. In this paper, two path based equivalence checking methods foruntimed PRES+ models are given. The experimental results demonstrate the efficiency the of the method.