This work addresses the vulnerability of trained neural network (NN) models, particularly against scan-chainbased attacks exploiting the accessibility of activation function outputs to acquire model information such as weights and biases illicitly. Our aim is to obfuscate the interconnections among the layers in the NN model controlled by secret keys stored in tamperproof memory. Our model ensures normal functionality with the correct key while disrupting data flow and producing erroneous outputs with an incorrect key. Extensive experiments demonstrate a significant drop in accuracy when incorrect keys are used, with the accuracy drop being more pronounced when the latter layers of the model are locked. The protection technique incurs 0.3% overhead in the area and 0.1% overhead in the latency of the designs.

Many control applications in real-time cyber-physical systems are represented as Directed Acyclic Graphs ( DAGs ) due to complex interactions among their functional components, and executed on distributed heterogeneous platforms. Data communication between dependent task nodes running on different processing elements are often realized through message transmission over a public network, and are hence susceptible to multiple security threats such as snooping , alteration , and spoofing . Several alternative security protocols having varying security strengths and associated implementation overheads are available in the market, for incorporating confidentiality , integrity , and authentication on the transmitted messages. While message size and correspondingly its associated transmission overheads may be marginally increased due to the assignment of security protocols, significant computation overheads must be incurred for securing the message at the location of its source task node and for unlocking security/message extraction at the destination. Obtained security strengths and associated computation overheads vary depending on the set of protocols chosen for a given message from an available pool of protocols. Given lower bounds on the security demands of an application’s messages, selecting the appropriate protocols for each message such that a system’s overall security is maximized while satisfying constraints related to the resource, task precedence and deadline, is a challenging and computationally hard problem. In this article, we propose an efficient heuristic strategy called SHIELD for security-aware real-time scheduling of DAG-structured applications to be executed on distributed heterogeneous systems. The efficacy of the proposed scheduler is exhibited through extensive simulation-based experiments using two DAG-structured application benchmarks. Our performance evaluation results demonstrate that SHIELD significantly outperforms two greedy baseline strategies SHIELDb in terms of solution generation times (i.e., runtimes) and SHIELDf in terms of achieved security utility. Additionally, a case study on the Traction Control application in automotive systems has been included to exhibit the applicability of SHIELD in real-world settings.

Torus is a symmetric Network-on-Chip (NoC) topology with uniform node degree providing very high path diversity between a pair of source and destination. Moreover, the Wraparound Channels (WCs) in the torus can significantly reduce the hop count, thereby reducing overall communication latency. However, the WCs also create cyclic paths that may lead to a NoC deadlock. As a consequence, very few deadlock-free routing algorithms for torus-based NoC exist that do not have significant implementation overhead. Furthermore, the existing routing algorithms do not unlock the full potential of the torus-based NoC topology. In this work, we present a formal modeling-based technique for developing deadlock-free routing algorithms for torus-based NoC. This method systematically combines routing algorithms of mesh with WCs of torus to develop deadlock-free routing algorithms for torus. Using the proposed technique, we develop three novel routing algorithms and verify their deadlock-freedom using Directional Dependency Graph (DDG). We then evaluate the proposed routing algorithms using both synthetic and real traffic patterns. The primary objective of this work is to present a technique that can generate multiple routing algorithms and not the single best routing algorithm. Hence, we do not claim that the three proposed algorithms are the best-performing ones. Nevertheless, we show that they can save hop counts by more than 10% and latency by 8% compared to the competitive methods. The performance of our algorithms is comparable even with state-of-the-art Table-based rout- ing and deadlock recovery-based technique.

Deep learning tasks, especially those involving complex convolution neural networks (CNNs), are computationally intensive and pose significant challenges when implemented on hardware. Accelerating these tasks is critical for improving performance. High-level Synthesis (HLS) has the potential to automate the efficient hardware accelerator designs directly from high-level C/C++ specification of trained machine learning (ML) models. Traditional HLS tools cannot synthesize certain high-level constructs, which require manual intervention. Many source code optimizations and the selection of pragmas for HLS optimizations are crucial for generating efficient hardware accelerators with HLS. However, both of these tasks are mostly manual efforts. Recently, Large Language Models (LLMs) have shown remarkable capabilities in various generative tasks. In this work, we explore the application of LLMs to remove these manual efforts in adapting HLS for ML accelerator designs. Our framework called LLM-assisted HLS, i.e., LHS, uses LLMs to automate the resolution of synthesis issues, ensuring compatibility with HLS tools. Furthermore, our framework automates the source code modification and optimization selection through pragma insertion steps, which are crucial for optimizing the synthesized design. Our experimental results with LHS demonstrate a significant improvement in latency for deep learning tasks with underlying complex CNN models without much area overhead. Our LHS allows us to achieve up to 2690 × latency improvement. Promisingly, LHS performs better than the state-of-the-art ML accelerator design tool hls4ml in 4 out of 6 cases in the context of latency improvement at the expense of area overhead (i.e., performance to hardware gain). This work highlights the potential of LLMs to assist and accelerate the HLS process, thereby creating more efficient hardware implementation for deep learning models.

High-Level Synthesis (HLS) tools are widely used for the efficient transformations of behavioural code into equivalent hardware in Register Transfer Level (RTL). However, recent studies show that Large Language Models (LLMs) can be used to generate Verilog or equivalent hardware descriptions directly from behavioural descriptions, making LLMs a potential ‘foe’ for HLS. While LLMs can generate RTL code, they lack certain fine aspects like control over design constraints and optimizations and the inability to handle large behavioural designs. In this paper, we show how LLM can be a ‘friend’ of HLS in generating RTL directly from behavioural descriptions. Although HLS tools have matured over the years, making the input code synthesizable, applying correct pragmas and source code optimizations are still manual efforts in the HLS. LLMs can make hardware accelerator design with HLS easier by automating these manual steps. We show that LLMs are efficient in resolving synthesis issues and optimizing course code for HLS. We have used performance to hardware gain to evaluate the LLMs’ performance in optimizing code adhering to resource usage. We perform our experiments on image processing tasks as benchmarks and discuss where LLM can perform well as well as the issues faced by it when trying to maximize the performance to hardware gain.

AI-as-a-Service (AIaaS) has been emerging with model providers deploying their models on cloud and model consumers using the model. Recently, ML models are being deployed on edge devices to improve cost and response time. The widespread usage of machine learning has made the study of security in the context of Machine Learning (ML) very critical. Model extraction attacks focuses on extracting model parameters such as weights and biases which can be used to clone a ML target model deployed on the cloud or on an edge device hardware. This paper explores different types of attacks on ML models primarily focusing on model extraction attacks on ML hardware such as scan-chain and side-channel attacks. The paper present an analysis of various such attacks and their countermeasures. Possible future directions of work are also discussed.

Technology mapping of the logic synthesis tool ABC transforms homogeneous Boolean circuit representations (e.g., and-inverter graphs, majority-inverter graphs etc.) into Application-Specific Integrated Circuit (ASIC) targets using a cut-based Boolean matching algorithm. This entails exposing numerous k-feasible cuts to the mapping algorithm to identify an optimal match of supergate (combination of standard cells) that minimizes the overall delay without much area overhead. However, this process incurs significant timing overhead due to the need to evaluate boolean matching across an exponentially large number of cuts. We introduce LEAP: a novel machine learning-assisted cut sampling strategy that identifies and prioritizes high-quality cuts (based on delay) while filtering out low-quality ones for each node. Our extensive experimentation demonstrates that LEAP reduces the number of cuts exposed to the mapper by over 51% compared to the tool ABC, resulting in a 2% improvement in delay without incurring any area penalty. In addition, LEAP uses 35% fewer cuts with respect to the state-of-the-art SLAP tool with superior area-delay product in most cases.

In modern System-on-Chip (SoC) design, dependence on offshore fabrication has increased manyfold. This empowers SoC designers to meet stringent time-to-market demands. However, it also brings rogue entities into play, possessing security threats like IP piracy, counterfeiting and overbuilding. Several countermeasures have been proposed to thwart these threats. Among all, logic locking has been the most coveted. Logic locking is a design-for-trust technique which conceals the underlying functionality of the design to be protected by adding extra key-controlled gates. This work proposes a novel attack called NoBALL on logic locked designs using their Binary Decision Diagram (BDD) representation. We identify specific properties from the locked design’s BDD and perform intuitive intersection operations in order to identify the correct keys. Experimental analysis highlights that the current version of the attack can act as an alternative to the SAT attack and can even outperform it in some cases. Our attack can also be combined with SAT attack to form a more robust attack in future.

The design and synthesis of masked cryptographic hardware implementations that are secure against power side-channel attacks (PSCAs) in the presence of glitches is a challenging task. High-level synthesis (HLS) is a promising technique for generating masked hardware directly from masked software, offering opportunities for design space exploration. However, conventional HLS tools make modifications that alter the guarantee against PSCA security via masking, resulting in an insecure register transfer level (RTL). Moreover, existing HLS tools cannot place registers at designated places and balance parallel paths in a masked cryptographic design. This is necessary to stop the propagation glitches that may hamper PSCA-security. This article introduces a domain-specific HLS tool tailored to obtain a PSCA secure masked hardware implementation directly from a masked software implementation. This tool places registers at specific locations required by the glitch-robust masking gadgets, resulting in a secure RTL. Furthermore, it automatically balances parallel paths and facilitates a reduction in latency while preserving the PSCA security guaranteed by masking. Experimental results with the PRESENT Cipher’s S-box and AES Canright’s S-box masked with four state-of-the-art gadgets, show that MaskedHLS produces RTLs with 73.9% decrease in registers and 45.7% decrease in latency on an average compared to manual register insertions. The PSCA security of MaskedHLS generated RTLs is also shown with TVLA test.

The functional correctness of compiler optimization does not ensure the security properties of the source program. A functionally correct compiler optimization may introduce new security vulnerabilities in the optimized program. In a compiler, ensuring the security of every optimization is a challenging task as it applies hundreds of optimizations. Thus, this work aims to develop a translation validation (TV) of information leakage for the optimization phase of the compiler without considering any intermediate information from the compiler. Our method measures the information leakage in a path, uses a concept of leak propagation over paths and loops, and defines the relative security between the source and optimized programs. This work considers two attack models based on different observation points to access the local memory and proposes different TV approaches. The correctness and complexity of the TV method are also provided. The experimental results in the SPARK compiler on various benchmarks show that the optimized program is not relatively secure in many cases.

Many of today’s complex cyber–physical systems (CPSs) are represented as a set of independent co-executing real-time control applications, where each such application is represented as a precedence-constrained task graph. The applications execute in infinite loops, periodically acquiring data from the environment through sensors at a particular frequency, processing the same, and then producing processed data via actuators. These CPSs often execute under stringent resource constraints (such as limited energy budgets) in distributed networked environments and may be heterogeneous to be able to satisfactorily meet stipulated performance specifications. This work presents a list-based energy-aware scheduler called DVFS-enabled periodic multi-DAG real-time scheduler for heterogeneous systems (DPMRS) for a set of real-time control applications co-executing in a heterogeneous distributed environment.DPMRSintroduces a novel approach for the integrated behavioral representation of a set of co-executing real-time DAG-structured applications. Each task in this integrated representation is then scheduled by determining its relative execution start time on a particular processor, which operates at an appropriately chosen frequency when the task runs on this processor. The overall objective ofDPMRSis to minimize aggregate energy consumed in the execution of all tasks. The efficacy of the proposed scheduler has been exhibited through extensive simulation experiments using benchmark task graphs from different application domains. Additionally, a case study on automotive control systems has been included to show the applicability of the proposed work in real-world settings.

To meet application-specific performance demands, recent embedded platforms often involve the use of intricate micro-architectural designs and very small feature sizes leading to complex chips with multi-million gates. Such ultra-high gate densities often make these chips susceptible to inappropriate surges in core temperatures. Temperature surges above a specific threshold may throttle processor performance, enhance cooling costs, and reduce processor life expectancy. This work proposes a generic temperature management strategy that can be easily employed to adapt existing state-of-the-art task graph schedulers so that schedules generated by them never violate stipulated thermal bounds. The overall temperature-aware task graph scheduling problem has first been formally modeled as a constraint optimization formulation whose solution is shown to be prohibitively expensive in terms of computational overheads. Based on insights obtained through the formal model, a new fast and efficient heuristic algorithm called TMDS has been designed. Experimental evaluation over diverse test case scenarios shows that TMDS is able to deliver lower schedule lengths compared to the temperature-aware versions of four prominent makespan minimizing algorithms, namely, HEFT , PEFT , PPTS , and PSLS . Additionally, a case study with an adaptive cruise controller in automotive systems has been included to exhibit the applicability of TMDS in real-world settings.

The necessity of efficient hardware accelerators for image processing kernels is a well known problem. Unlike the conventional HDL based design process, High-level Synthesis (HLS) can directly convert behavioral (C/C++) description into RTL code and can reduce design complexity, design time as well as provide user opportunity for design space exploration. Due to the vast optimization possibilities in HLS, a proper application level behavioral characterization is necessary to understand the leverages offered by these workloads especially for facilitating parallel computation. In this work, we present a set of HLS optimization strategies derived upon exploiting the most general HLS influential characteristic features of image processing algorithms. We also present an HLS benchmark suite ImageSpec to demonstrate our strategies and their efficiency in optimizing workloads spanning diverse domains within image processing sector. We have shown that an average performance to hardware gain of 143x could be achieved over the baseline implementation using our optimization strategies.

Logic locking is a technique for the protection of hardware intellectual property (IP) from malicious entities like piracy, overproduction, reverse engineering, etc. The register transfer level (RTL) locking performs the locking on RTL description for protection of the IP even from the early design cycle. TAO [12] is such a locking scheme that employs locking during the high-level synthesis (HLS) process. In this paper, we evaluate the unlocking capability of the genetic algorithm (GA) by performing attacks on the RTLs locked using TAO based technique. We demonstrate the ability of GA to unlock TAO generated RTLs in seconds. Our GA based attack is faster as compared to the Satisfiability Modulo Theories (SMT) based attack [9]. The GA based method also converges well in most of the cases as shown in the experimental results.

Scheduling real-time applications modelled as directed acyclic graphs on heterogeneous distributed platforms is known to be a challenging as well as a computationally demanding problem. This article deals with the design of an efficient scheduler for executing a real-time task graph on a distributed platform consisting of a set of fully connected heterogeneous processors. The objective of the scheduling strategy is to minimize ageneric penalty functionwhich can be amicably adopted toward its deployment in various application domains such as real-time embedded systems, cloud/fog computing, industrial automation and IoTs, smart grids, automotive and avionic systems, etc. We have first encoded the problem as a constraint satisfaction problem and then developed an efficient list-based heuristic scheduling algorithm calledPenalty-aware REal-time Scheduler for Task graphs on heterOgeneous platforms(PRESTO), to generate a minimal penalty deadline-meeting static schedule. The generic efficacy ofPRESTOis exhibited through extensive simulation-based experiments using standard benchmark task graphs. The practical applicability ofPRESTOin diverse scenarios have further been exhibited by using the scheme in two different real-world case studies, the first of which relates to automotive embedded systems, while the second is in the domain of fog computing.

A hardware Trojan (HT) is a malicious modification of the design done by a rogue employee or a malicious foundry to leak secret information, create a backdoor for attackers, alter functionality, degrade performance and even halt the system. In Black-hat high-level synthesis (HLS) (Pilato et al., 2019), the authors have introduced a possibility of HTs insertion in the register transfer level (RTL) design by the HLS tool itself. Specifically, degradation attack (DA), battery exhaustion (BE) attack, and downgrade attack (DG) have been proposed in that work. In this study, we show how all three HTs inserted by Pilato et al. (2019) can be detected using a C-to-RTL equivalence checking framework. We have assumed that both the input C code and the Trojan-infected RTL code are available for our analysis. Specifically, our framework extracts an RTL-level finite-state machine with datapaths (RTL-FSMDs) from the HLS-generated RTL. During finite-state machine with datapath (FSMD) construction, a BE attack can be identified. Our proposed method then compares the FSMD of the input C code with the RTL-FSMD to identify the DA and the DG. The experimental results confirm the detection of HTs of the black-hat HLS tool.

High-level synthesis (HLS) is a well-established framework used to translate high-level algorithmic behaviors into hardware designs. Despite the enduring research efforts, a major prevailing bottleneck of HLS is the large gap between the design and verification processes. Presently, register transfer level (RTL) simulation is the primary platform used for HLS design verification. Although most of the state-of-the-art RTL simulators provide an abstracted user-friendly platform for verification, they are undesirably slow and sometimes incomprehensible to non-field-programmable gate array experts to debug. The alternative software simulators (C simulation) introduced by commercial HLS tools render faster simulation, but are not cycle accurate and are not capable to estimate design performance. In this article, we introduce an automatic cycle-accurate simulation tool, FastSim, that manipulates certain unique features of HLS design to extract a concise, well-indented, and debug-friendly C behavior from the synthesized RTL. Our simulation tool ensures RTL correctness, provides cycle accuracy, accurate performance estimation, and renders on an average around 300 times faster simulation compared to RTL simulators and comparable performance to that of software C simulators.

Compiler optimizations can be functionally correct but not secure. In this work, we attempt to quantify the information leakage in a program for the security verification of compiler optimizations. Our work has the following contributions. We demonstrate that static taint analysis is applicable for security verification of compile optimizations. We develop a completely automated approach for quantifying the information leak in a program in the context of compiler optimizations. Our method avoids many false-positives scenarios due to implicit flow. It can handle leaks in a loop and propagates leaks over paths using the leak propagation vector. With our quantification parameters, we verify the relative security of source and transformed programs considering the optimizations phase of a compiler as a black box. Our experimental evaluations on benchmarks for various compiler optimizations in SPARK show that the SPARK compiler is actually leaky.

The fab-less IC design industry is at risk of IC counterfeiting and Intellectual Property (IP) theft by untrusted third party foundries. Logic obfuscation thwarts IP theft by locking gate-level netlists using a locking key. The complexity of circuit designs and migration to high level synthesis (HLS) expands the scope of locking to a higher abstraction. Automated RTL locking during HLS integrates obfuscation into the backend HLS tool. This is tedious and requires access to the HLS tool source code. Furthermore, recent work proposed an SMT attack on HLS-based obfuscation. In this work, we propose sn RTL locking tool HOST, to thwart the SMT attack. The HOST approach is agnostic to the HLS tool. Results show that HOST obfuscations have low overhead and thwart SMT attacks.

Abstract Testability transformation (TT) is a source‐to‐source programme transformation that aims to improve the ability of a given test generation method to generate test data for the original programme. Herein, the correctness of testability transformations is shown. Translation validation is the process of proving that the transformed programme is a correct translation of the source programme being compiled. It is widely used to verify the correctness of various compiler optimizations and transformations during scheduling. The value propagation based equivalence checking (VP) method is an efficient translation validation approach proposed to verify the correctness of various compiler optimization applied during scheduling in high‐level synthesis. VP‐based translation validation of testability transformations is proposed. In particular, it is identified that the existing VP method fails to show the equivalence for some of the TTs. A dynamic cutpoint selection scheme and an enhancement to the VP method to overcome these limitations are shown. The enhanced VP method, called VP_TT, successfully shows the equivalence for the TTs where the VP method fails. Experimental results confirm the usefulness of VP_TT in the verification of testability transformations.

The problem of scheduling Directed Acyclic Graphs in order to minimizemakespan(schedule length), is known to be a challenging and computationally hard problem. Therefore, researchers have endeavored towards the design of various heuristic solution generation techniques both for homogeneous as well as heterogeneous computing platforms. This work first presentsHMDS-Bl, a list-based heuristicmakespanminimization algorithm for task graphs on fully connected heterogeneous platforms. Subsequently,HMDS-Blhas been enhanced by empowering it with a low-overhead depth-first branch and bound based search approach, resulting in a new algorithm calledHMDS.HMDShas been equipped with a set of novel tunable pruning mechanisms, which allow the designer to obtain a judicious balance between performance (makespan) and solution generation times, depending on the specific scenario at hand. Experimental analyses using randomly generated DAGs as well as benchmark task graphs, have shown thatHMDSis able to comprehensively outperform state-of-the-art algorithms such asHEFT,PEFT,PPTS, etc., in terms of archivedmakespanswhile incurring bounded additional computation time overhead.

Register Transfer Level (RTL) locking seeks to prevent intellectual property (IP) theft of a design by locking the RTL description that functions correctly on the application of a key. This paper evaluates the security of a state-of-the-art RTL locking scheme using a satisfiability modulo theories (SMT) based algorithm to retrieve the secret key. The attack first obtains the high-level behavior of the locked RTL, and then use an SMT based formulation to find so-called distinguishing input patterns (DIP)1The attack methodology has two main advantages over the gate-level attacks. First, since the attack handles the design at the RTL, the method scales to large designs. Second, the attack does not apply separate unlocking strategies for the combinational and sequential parts of a design; it handles both styles via a unifying abstraction. We demonstrate the attack on locked RTL generated by TAO [1], a state-of-the-art RTL locking solution. Empirical results show that we can partially or completely break designs locked by TAO.

High-level synthesis (HLS) technique translates the behaviors written in high-level languages like C/C++ into register transfer level (RTL) design. Due to its complexity, proving the correctness of an HLS tool is prohibitively expensive. Translation validation is the process of proving that the target code is a correct translation of the source program being compiled. The path-based equivalence checking (PBEC) method is a widely used translation validation method for verification of the scheduling phase of HLS. The existing PBEC methods cannot handle significant control structure modification that occurs in the efficient scheduling of conditional behaviors. Hence, they produce a false-negative result. In this article, we identify some scenarios involving path merge/split where the state-of-the-art PBEC approaches fail to show the equivalence even though behaviors are equivalent. We propose a value propagation-based PBEC method along with a new cutpoint selection scheme to overcome this limitation. Our method can also handle the scenario where adjacent conditional blocks (CBs) having an equivalent conditional expression are combined into one CB. Experimental results demonstrate the usefulness of our method over the existing methods.

A formal modeling of a Network-on-Chip (NoC) using a communicating finite state machine (CFSM) is presented in this article. We have automated the CFSM model generation for NoCs with Mesh and Torus topologies. To verify deadlock in an NoC, we need to consider the formal model of all the routers in a given topology. It is not supported by the available verification tools due to the state space explosion problem. An NoC simulator gives only a warning message about a possible deadlock, which does not guarantee a real deadlock situation. Therefore, we have developed a simulation framework based on our CFSM models of NoCs in which any routing algorithm can be simulated over a given traffic pattern. Our simulation framework confirms real deadlock when simulation reaches a state from which no progress is possible. We have shown that this situation actually depicts cyclic dependencies among the different NoC components. As a proof of concept, we have implemented our simulation framework for one static routing and two adaptive routing algorithms. The experimental results show that our method is scalable. This is possible because we only check the existence of a deadlock for a given traffic pattern at a time, rather than for all possible traffic patterns. Our approach opens up a way to verify other NoC properties such as starvation, livelock, and so on for a given routing algorithm for any realistic traffic patterns.

Path‐based equivalence checkers (PBECs) have been successfully applied for verification of programmes from diverse domains and from various stages of high‐level synthesis. In the case of non‐equivalence, PBEC provides very little information which is not sufficient for further investigation of the two programmes being compared by some human expert. In this work, the authors show how a counter‐trace ( cTrace ) can be generated in the case of non‐equivalence reported by the PBEC. Using this cTrace , they also present a procedure to find suitable initialisation values for input variables which reveal the non‐equivalence (i.e. counter‐example) by using off‐the‐shelf satisfiability modulo theories (SMT) solvers. To aid the human expert, they also show that how they can visualise this cTrace in the control and data‐flow graph of the programmes using the graph visualisation software – Graphviz. This counter‐example and visual representation of the corresponding cTrace will be helpful in debugging the root cause of the non‐equivalence. The experimental results are encouraging.

Translation validation is the process of proving that the target code is a correct translation of the source program being compiled. In this paper, 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. We have also identified a scenario involving code motion across loops where the state-of-the-art translation validation method gives false positive results. Our method can prove the nonequivalence of the concerned finite state machines with data paths in this scenario. We detected a bug in the HLS tool SPARK involving loop invariant code motion using our method. Experimental results demonstrate the usefulness of our method.

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.

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.

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.