Abstract
MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

Abstract
Enhancing performance is crucial when developing applications for high-performance and embedded computing. It requires sophisticated techniques and in-depth knowledge of the application domain and target architecture. Typically, developers prioritize the application's functional requirements over extra-functional requirements. Thus, a large part of the optimization effort is shifted to performance engineers, who rely on manual effort, alongside many analysis and optimization tools that need integration. This paper focuses on memoization, which caches results of pure computations and retrieves them if a function is called with repeating arguments. We propose a methodology for allowing developers and performance engineers to apply memoization straightforwardly by automating code analysis, code transformations, and memoization-specific profiling. It helps developers with no optimization expertise to quickly set up memoization and, simultaneously, it provides performance engineers with highly customizable analysis and memoization. We provide a concrete implementation supported by a DSL, a source-to-source compiler, and a memoization framework. We evaluate the methodology and framework with publicly available benchmarks. We show how one can analyze applications to select functions with performance improvement potential, which the experiments reveal might be challenging to find, and improve some applications with minimal effort. © 2021 ACM.

Abstract
As applications move to the edge, efficiency in computing power and power/energy consumption is required. Heterogeneous computing promises to meet these requirements through application-specific hardware accelerators. Runtime adaptivity might be of paramount importance to realize the potential of hardware specialization, but further study is required on workload retargeting and offloading to reconfigurable hardware. This article presents our framework for the exploration of both offloading and hardware generation techniques. The framework is currently able to process instruction sequences from MicroBlaze, ARMv8, and riscv32imaf binaries, and to represent them as Control and Dataflow Graphs for transformation to implementations of hardware modules. We illustrate the framework's capabilities for identifying binary sequences for hardware translation with a set of 13 benchmarks.

Abstract
High-level Synthesis (HLS) is of paramount importance to leverage the use of FPGA-based accelerators by software developers. To achieve efficient FPGA implementations, code restructuring and source code annotating with HLS directives are necessary. However, this is still a manual process conducted by experienced developers. This paper proposes a step on a framework to automatically optimize C code via directives, using a source-to-source compiler on a stage before HLS. This optimization is primarily applied by strategies that select, configure, and insert directives on the code input to the Vivado HLS tool to synthesize more latency-efficient FPGA hardware. Those strategies rely on very simple but effective heuristics, which use a small set of properties extracted from the control/dataflow graphs generated from the input source code. We evaluate the framework using a variety of source codes. The experiments show that it can achieve efficient results while maintaining a low resource usage in most cases. Our experiments also compare the framework results to code optimized manually with directives, and they show that for most benchmarks used, it achieves similar results.

Abstract
FPGAs have emerged as hardware accelerators, and in the last decade, researchers have proposed new languages and frameworks to improve the efficiency when mapping computations to FPGAs. One of the main tasks when considering the mapping of software code to FPGAs is code restructuring. Code restructuring is of paramount importance to achieve efficient FPGA-based accelerators, and its automation continues to be a challenge. This paper describes our recent work on techniques to automatically restructure and annotate C code with directives optimized for HLS targeting FPGAs. The input of our approach consists of an unfolded dataflow graph (DFG), currently obtained by a trace of the program's execution, and restructured C code with HLS directives as output. Specifically, in this paper we propose algorithms to optimize the input DFGs and use isomorphic graph detection for exposing data-level parallelism. The experimental results show that our approach is able to generate efficient FPGA implementations, with significant speedups over the input unmodified source codes, and very competitive to implementations obtained by manual optimizations and by previous approaches. Furthermore, the experiments show that, using our approach, it is possible to extract data-parallelism in linear to quadratic time with respect to the number of nodes of the input DFG.

Abstract
This article presents Clava, a Clang-based source-to-source compiler, that accepts scripts written in LARA, a JavaScript-based DSL with special constructs for code queries, analysis and transformations. Clava improves Clang's source-to-source capabilities by providing a more convenient and flexible way to analyze, transform and generate C/C++ code, and provides support for building strategies that capture run-time behavior. We present the Clava framework, its main capabilities, and how it can been used. Furthermore, we show that Clava is sufficiently robust to analyze, instrument and test a set of large C/C++ application codes, such as GCC. (C) 2020 The Authors. Published by Elsevier B.V.