Neuromorphic Continual Learning (NCL) paradigm leverages Spiking Neural Networks (SNNs) to enable continual learning (CL) capabilities for AI systems to adapt to dynamically changing environments. Currently, the state-of-the-art employ a memory replay-based method to maintain the old knowledge. However, this technique relies on long timesteps and compressiondecompression steps, thereby incurring significant latency and energy overheads, which are not suitable for tightly-constrained embedded AI systems (e.g., mobile agents/robotics). To address this, we propose Replay4NCL, a novel efficient memory replaybased methodology for enabling NCL in embedded AI systems. Specifically, Replay4NCL compresses the latent data (old knowledge), then replays them during the NCL training phase with small timesteps, to minimize the processing latency and energy consumption. To compensate the information loss from reduced spikes, we adjust the neuron threshold potential and learning rate settings. Experimental results on the class-incremental scenario with the Spiking Heidelberg Digits (SHD) dataset show that Replay4NCL can preserve old knowledge with Top-1 accuracy of $\mathbf{9 0. 4 3 \%}$ compared to $\mathbf{8 6. 2 2 \%}$ from the state-of-the-art, while effectively learning new tasks, achieving 4.88x latency speed-up, $\mathbf{2 0 \%}$ latent memory saving, and 36.43% energy saving. These results highlight the potential of our Replay4NCL methodology to further advances NCL capabilities for embedded AI systems.

Abstract Performance of trained neural network (NN) models, in terms of testing accuracy, has improved remarkably over the past several years, especially with the advent of deep learning. However, even the most accurate NNs can be biased toward a specific output classification due to the inherent bias in the available training datasets, which may propagate to the real-world implementations. This paper deals with the robustness bias, i.e., the bias exhibited by the trained NN by having a significantly large robustness to noise for a certain output class, as compared to the remaining output classes. The bias is shown to result from imbalanced datasets, i.e., the datasets where all output classes are not equally represented. Towards this, we propose the UnbiasedNets framework, which leverages K-means clustering and the NN’s noise tolerance to diversify the given training dataset, even from relatively smaller datasets. This generates balanced datasets and reduces the bias within the datasets themselves. To the best of our knowledge, this is the first framework catering to the robustness bias problem in NNs. We use real-world datasets to demonstrate the efficacy of the UnbiasedNets for data diversification, in case of both binary and multi-label classifiers. The results are compared to well-known tools aimed at generating balanced datasets, and illustrate how existing works have limited success while addressing the robustness bias. In contrast, UnbiasedNets provides a notable improvement over existing works, while even reducing the robustness bias significantly in some cases, as observed by comparing the NNs trained on the diversified and original datasets.

Deep brain stimulation (DBS) is a widely accepted treatment for the Parkinson's disease (PD). Traditionally, it is done in an open-loop manner, where stimulation is always ON, irrespective of the patient needs. As a consequence, patients can feel some side effects due to the continuous high-frequency stimulation. Closed-loop DBS can address this problem as it allows adjusting stimulation according to the patient need. The selection of open- or closed-loop DBS and an optimal algorithm for closed-loop DBS are some of the main challenges in DBS controller design, and typically the decision is made through sampling based simulations. In this letter, we used model checking, a formal verification technique used to exhaustively explore the complete state space of a system, for analyzing DBS controllers. We analyze the timed automata of the open-loop and closed-loop DBS controllers in response to the basal ganglia (BG) model. Furthermore, we present a formal verification approach for the closed-loop DBS controllers using timed computation tree logic (TCTL) properties, that is, safety, liveness (the property that under certain conditions, some event will eventually occur), and deadlock freeness. We show that the closed-loop DBS significantly outperforms existing open-loop DBS controllers in terms of energy efficiency. Moreover, we formally analyze the closed-loop DBS for energy efficiency and time behavior with two algorithms, the constant update algorithm and the error prediction update algorithm. Our results demonstrate that the closed-loop DBS running the error prediction update algorithm is efficient in terms of time and energy as compared to the constant update algorithm.

Over the past years, numerous studies demonstrated the vulnerability of deep neural networks (DNNs) to make correct classifications in the presence of small noise. This motivated the formal analysis of DNNs to ensure that they delineate acceptable behavior. However, in the case that the DNN’s behavior is unacceptable for the desired application, these qualitative approaches are ill equipped to determine the precise degree to which the DNN behaves unacceptably. We propose a novel quantitative DNN analysis framework, QuanDA, which not only checks whether the DNN delineates certain behavior but also provides the estimated probability of the DNN to delineate this particular behavior. Unlike the (few) available quantitative DNN analysis frameworks, QuanDA does not use any implicit assumptions on the probability distribution of the hidden nodes, which enables the framework to propagate close to real probability distributions of the hidden node values to each proceeding DNN layer. Furthermore, our framework leverages CUDA to parallelize the analysis, enabling high-speed GPU implementation for fast analysis. The applicability of the framework is demonstrated using the ACAS Xu benchmark, to provide reachability probability estimates for all network nodes. This paper also provides potential applications of QuanDA for the analysis of DNN safety properties.

User guided proof development in interactive theorem proving is a manual and time consuming activity.For automating proof searching and optimization in a higher-order logic proof assistant, we provide two metaheuristic algorithms that are based on Fitness Dependent Optimizer (FDO) and Bat Algorithm (BA).In both metaheuristic algorithms, random proof sequences are first created from a population of frequently occurring proof steps that are discovered using pattern mining techniques.Created proof sequences are then evolved till their fitness matches the fitness of the original (or target) proof sequences.Experiments are performed to investigate the performance of the proposed algorithms on different HOL4 theories.Moreover, the proposed FDO and BA-based proof searching approaches are compared with Simulated Annealing (SA) and Genetic Algorithm (GA)based methods.Results show that BA performs best, followed by FDO and SA for proof finding and optimization in HOL4.

In this article, we propose a novel model checking-based methodology that analyzes the hardware trojan (HT)-based security vulnerabilities in sequential circuits with 100% coverage while addressing the state-space explosion issue and completeness issue. In this work, the state-space explosion issue is addressed by efficiently partitioning the larger state space into corresponding smaller state spaces to enable the distributed HT-based security analysis of complex sequential circuits. We analyze multiple ISCAS89 and trust-hub benchmarks for different ASIC technologies, i.e., 65, 45, and 22 nm, to demonstrate the efficacy of our framework in identifying HT-based security vulnerabilities. The experimental results show that ForASec successfully performs the complete analysis of the given complex and large sequential circuits, and provides approximately$6\times $–$10\times $speedup in analysis time compared to the state-of-the-art model checking-based techniques.

Deep learning (DL) has been shown to be highly effective in solving various problems across numerous applications and domains, such as autonomous driving and image recognition. Due to the advent of DL, plenty of research works have explored the applicability of DL, more specifically deep neural networks (DNNs), to solve pattern recognition and computer vision challenges. More recently, researchers have focused on the topic of automated generation and exploration of DNN architectures, which tend to mostly focus on image recognition or visual data sets, primarily, due to the computer vision-related DL advancements. In this work, we propose the BioNetExplorer framework to systematically generate and explore multiple DNN architectures for biosignal processing in wearable devices. Our framework varies key neural architecture parameters to search for an embedded DNN architecture with a low hardware overhead, which can be deployed in wearable edge devices to analyze the biosignal data and to extract the relevant information, such as arrhythmia and seizure. Furthermore, BioNetExplorer reduces the exploration time by deploying genetic algorithms, such as NSGA-II, SPEA-2, etc. Our framework also enables the hardware-aware DNN architecture search by imposing user requirements and hardware constraints (storage, FLOPs, etc.) during the exploration stage, thereby limiting the number of networks explored. Moreover, BioNetExplorer can also be used to search for DNNs based on the user-required output classes; for instance, a user might require a specific output class, attributed toward ventricular fibrillation, due to genetic predisposition or a preexisting heart condition. The use of genetic algorithms reduces the exploration time, on average, by 9×, compared to exhaustive exploration. We are successful in identifying Pareto-optimal designs, which can reduce the storage overhead of DNN by ~ 30 MB for a quality loss of less than 0.5%. To enable low-cost embedded DNNs, BioNetExplorer also employs different model compression techniques to further reduce the storage overhead of the network by up to 53× for a quality loss of $ <; 0.2\%$ .

Machine learning is widely used these days to extract meaningful information out of the Zettabytes of sensors data collected daily. All applications require analyzing and understanding the data to identify trends, e.g., surveillance, exhibit some error tolerance. Approximate computing has emerged as an energy-efficient design paradigm aiming to take advantage of the intrinsic error resilience in a wide set of error-tolerant applications. Thus, inexact results could reduce power consumption, delay, area, and execution time. To increase the energy-efficiency of machine learning on FPGA, we consider approximation at the hardware level, e.g., approximate multipliers. However, errors in approximate computing heavily depend on the application, the applied inputs, and user preferences. However, dynamic partial reconfiguration has been introduced, as a key differentiating capability in recent FPGAs, to significantly reduce design area, power consumption, and reconfiguration time by adaptively changing a selective part of the FPGA design without interrupting the remaining system. Thus, integrating “Dynamic Partial Reconfiguration” (DPR) with “Approximate Computing” (AC) will significantly ameliorate the efficiency of FPGA-based design approximation. In this article, we propose hardware-efficient quality-controlled approximate accelerators, which are suitable to be implemented in FPGA-based machine learning algorithms as well as any error-resilient applications. Experimental results using three case studies of image blending, audio blending, and image filtering applications demonstrate that the proposed adaptive approximate accelerator satisfies the required quality with an accuracy of 81.82%, 80.4%, and 89.4%, respectively. On average, the partial bitstream was found to be 28.6 smaller than the full bitstream .

Approximate computing (AC) is an emerging computing paradigm suitable for intrinsic error-tolerant applications to reduce energy consumption and execution time. Different approximate techniques and designs, at both hardware and software levels, have been proposed and demonstrated the effectiveness of relaxing the average output quality constraint. However, the output quality of AC is highly input-dependent, i.e., for some input data, the output errors may reach unacceptable levels. Therefore, there is a dire need for an input-dependent tunable approximate design. With this motivation, in this article, we propose a lightweight and efficient machine-learning-based approach to build an input-aware design selector, i.e., quality controller, to adapt the approximate design in order to meet the target output quality (TOQ). For illustration purposes, we use a library of 8-bit and 16-bit energy-efficient approximate array multipliers with 20 different settings, which are commonly used in image and audio processing applications. The simulation results, based on two sets of images, including an 8 Scene Categories Dataset, which is a benchmark of images data set, demonstrate the effectiveness of the lightweight selector where the proposed tunable design achieves a significant reduction in quality loss with relatively low overhead.

In this paper, we propose a novel methodology for efficiently computing the Probability Mass Function (PMF) of error at the output of a major class of approximate adders that comprise of a cascade of multiple stages of smaller approximate adder units. The proposed methodology utilizes the carry-out probability of the previous stage along with the input probabilities of the current stage to recursively computes the PMF of error of the current stage. The proposed methodology eliminates the need for exhaustive simulations and, therefore, can be used for efficiently analyzing error distribution of a wide variety of low-power large bit-width adders with cascaded approximate adder units. Experimental results demonstrate that the proposed methodology provides error estimates that commensurate with exhaustive simulations, while offering a speedup of at least 2958x for 8-bit (or larger) approximate adder configurations.

With a constant improvement in the network architectures and training methodologies, Neural Networks (NNs) are increasingly being deployed in real-world Machine Learning systems. However, despite their impressive performance on "known inputs", these NNs can fail absurdly on the "unseen inputs", especially if these real-time inputs deviate from the training dataset distributions, or contain certain types of input noise. This indicates the low noise tolerance of NNs, which is a major reason for the recent increase of adversarial attacks. This is a serious concern, particularly for safety-critical applications, where inaccurate results lead to dire consequences. We propose a novel methodology that leverages model checking for the Formal Analysis of Neural Network (FANNet) under different input noise ranges. Our methodology allows us to rigorously analyze the noise tolerance of NNs, their input node sensitivity, and the effects of training bias on their performance, e.g., in terms of classification accuracy. For evaluation, we use a feed-forward fully-connected NN architecture trained for the Leukemia classification. Our experimental results show ±11% noise tolerance for the given trained network, identify the most sensitive input nodes, and confirm the biasness of the available training dataset.

Abstract Secure and continuous operation of a smart grid substation mainly depends upon the reliable functioning of its communication network. The communication system of a smart substation is typically based on a high performance Ethernet communication network that connects various intelligent embedded devices, such as Intelligent Electronic Devices (IED) andMerging Units (MU), to ensure continuous monitoring, automation and efficient demand response of the smart substation. Traditionally, Reliability Block Diagram (RBD) and Fault Tree (FT) methods are used to develop reliability and failure models for these communication networks by considering the failure characteristics of their substation intelligent embedded devices and other components, like transformers and circuit breakers. These resulting reliability and failure models are then analyzed using paper-and-pencil methods or computer simulations, but they cannot assure accuracy in the analysis due to their inherent limitations. As an accurate alternative, we propose a methodology, based on higher-order logic theorem proving, for conducting the formal RBD and FT-based reliability and failure analysis of smart substation communication networks, respectively. This paper also describes a sound transformation of smart grid FT models to their equivalent RBDs - a well-known method to reduce the complexity of FT-based failure analysis. Some ML-based tactics have been developed to automatically compute the reliability and failure probability of smart grid substations for practical purposes.

Abstract Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection and in-vitro fertilization. Robotic cell injection systems provide the automation of the process as opposed to the manual and semi-automated cell injection systems, which require expert operators and involve time consuming processes and also have lower success rates. The automation of the cell injection process is obtained by controlling the orientation and movement of its various components, like injection manipulator, microscope etc., and planning the motion of the injection pipette by controlling the force of the injection. The conventional techniques to analyze the cell injection process include paper-and-pencil proof and computer simulation methods. However, both these techniques suffer from their inherent limitations, such as, proneness to human error for the former and the approximation of the mathematical expressions involved in the numerical algorithms for the latter. Formal methods have the capability to overcome these limitations and can provide an accurate analysis of these cell injection systems. Model checking, i.e., a state-based formal method, has been recently used for analyzing these systems. However, it involves the discretization of the differential equations capturing the continuous dynamics of the system and thus compromises on the completeness of the analysis of these safety-critical systems. In this paper, we propose a higher-order-logic theorem proving (a deductive-reasoning based formal method) based framework for analyzing the dynamical behavior of the robotic cell injection systems upto 4-DOF. The proposed analysis, based on the HOL Light theorem prover, enabled us to identify some discrepancies in the simulation and model checking based analysis of the same robotic cell injection system.

Approximate computing has emerged as an efficient design approach for applications with inherent error resilience. Low-power approximate adders (LPAAs), for instance, IMPACT and InXA, are being advocated as building blocks for approximate computing hardware. For their practical adoption, the error caused by these units needs to be pre-evaluated and compared with maximum allowable error bounds for an application. To address this problem, we present PEAL, a Probabilistic error analysis methodology for Low-power Approximate Single and Multi-layered Adder Architectures , while considering variable probabilities for each bit of input operands for a given multi-bit adder design. PEAL is highly generic, linearly scalable, and applicable to any adder type. The analysis provides probability of success, which is accurate for single-layered adder architectures and provides a lower bound for multi-layered architectures. We have shown that state-of-the-art LPAAs can serve as effective building blocks of approximate computing only when the input probabilities are either very high (>0.8) or very low (<0.2). Interestingly, none of the state-of-the-art LPAA units, which to the best of our knowledge are the most widely adopted, has demonstrated effectiveness for mid-range probabilities (0.3–0.7). We have also analytically explained the cause of this usability limitation and proposed its solution. Moreover, we have proposed a method for estimating the Mean-squared Error of datapaths composed of LPAAs, to quantify the magnitude of error introduced in the output due to approximation of the adder units.

Dynamic thermal management (DTM) techniques are being widely used for attenuation of thermal hot spots in many-core systems. Conventionally, DTM techniques are analyzed using simulation and emulation methods, which are in-exhaustive due to their inherent limitations and cannot provide for a comprehensive comparison between DTM techniques owing to the wide range of corresponding design parameters. In order to handle the above discrepancies, we propose to use model checking, a state-space-based formal method, to model, evaluate, and compare DTM techniques across various functional and performance parameters. The suggested framework includes a modeling flow and a set of generic modules that realistically model many-core and DTM parameters like temperature, power, application, intercore communication and task migration, etc. For analysis purpose, the framework provides a common ground for comparing DTM techniques by formalizing DTM principles and performance parameters as a set of logical properties. These properties are verified for different task load configurations, e.g., multithreaded, malleable, and the applications which do not support migration. We analyze state-of-the-art central (c-) and distributed (d-) DTM techniques to demonstrate the generality and efficacy of our approach. Our formal analysis shows that the state-of-the-art cDTM technique performs better than dDTM in terms of achieving thermal stability, task migration, and communication overhead. We believe that conventional analysis methods do not facilitate such an exhaustive comparison among the DTM techniques.

Traditional learning-based approaches for runtime hardware Trojan (HT) detection require complex and expensive on-chip data acquisition frameworks, and thus incur high area and power overhead. To address these challenges, we propose to leverage the power correlation between the executing instructions of a microprocessor to establish a machine learning (ML)-based runtime HT detection framework, called MacLeR. To reduce the overhead of data acquisition, we propose a single power-port current acquisition block using current sensors in time-division multiplexing, which increases accuracy while incurring reduced area overhead. We have implemented a practical solution by analyzing multiple HT benchmarks inserted in the RTL of a system-on-chip (SoC) consisting of four LEON3 processors integrated with other IPs, such as vga_lcd, RSA, AES, Ethernet, and memory controllers. Our experimental results show that compared to state-of-the-art HT detection techniques, MacLeR achieves 10% better HT detection accuracy (i.e., 96.256%) while incurring a 7× reduction in area and power overhead (i.e., 0.025% of the area of the SoC and <; 0.07% of the power of the SoC). In addition, we also analyze the impact of process variation (PV) and aging on the extracted power profiles and the HT detection accuracy of MacLeR. Our analysis shows that variations in fine-grained power profiles due to the HTs are significantly higher compared to the variations in fine-grained power profiles caused by the PVs and aging effects. Moreover, our analysis demonstrates that on average, the HT detection accuracy drops in MacLeR is less than 1% and 9% when considering only PV and PV with worst case aging, respectively, which is ≈10× less than in the case of the state-of-the-art ML-based HT detection technique.

Approximate computing (AC) is a nascent energy-efficient computing paradigm for error-resilient applications. However, the quality control of AC is quite challenging due to its input-dependent nature. Existing solutions fail to address fine-grained input-dependent controlled approximation. In this paper, we propose an input-aware machine learning based approach for the quality control of AC. For illustration purposes, we use 20 configurations of 8-bit approximate multipliers. We evaluate these designs for all combinations of possible input data. Then, we use machine learning algorithms to efficiently make predictive decisions for the quality control of the target approximate application, based on experimentally collected training data. The key benefits of the proposed approach include: (1) fine-grained input-dependent approximation, (2) no missed approximation opportunities, (3) no rollback recovery overhead, (4) applicable to any approximate computation with error-tolerant components, and (5) flexibility in adapting various error metrics.

Approximate computing is an emerging trend in hardware and software design that leverages upon the inherent tolerance for inaccuracy in applications to optimize their power consumption, latency, and area. Due to the widespread usage of adders in digital hardware designs, numerous approximate adders, offering various error margins and area, latency and power constraints, have been proposed. Probabilistic error analysis of these adders holds a significant step in selecting an appropriate approximate adder for a given application. Traditionally, this analysis has been conducted using Monte-Carlo simulations or analytical analysis, which do not ascertain a sound and complete analysis. In order to overcome these limitations, we propose to use interactive theorem proving for error analysis of approximate adders. For this purpose, we present a higher-order-logic formalization of probability distributions and error related events encountered in approximate adders that comprise of subadder units, based on a probability theory formalization available in the HOL4 theorem prover. We also propose an algorithm for analyzing the probability of error as a metric for accurate comparison for high-speed, low-latency approximate adders with uniformly distributed inputs. For illustration purposes, we present the formal error analysis of three of the most widely acclaimed approximate adders, i.e., error tolerant adder-I, accuracy configurable adder, and generic accuracy configurable adder.

Approximate multipliers are widely being advocated for energy-efficient computing in applications that exhibit an inherent tolerance to inaccuracy. In this paper, we identify three decisions for design and evaluation of approximate multiplier circuits: (1) the type of approximate full adder (FA) used to construct the multiplier, (2) the architecture, i.e., array or tree, of the multiplier and (3) the placement of sub-modules of approximate and exact multipliers in the target multiplier module. Based on FA cells implemented at the transistor level (TSMC65nm), we developed several approximate building blocks of 8x8 multipliers, as well as various implementations of higher order multipliers. These designs are evaluated based on their power, area, delay and error and the best designs are identified. We validate these designs on an image blending application using MATLAB, and compare them to related work.

The recent advancements in system-on-chip (SoC) and network-on-chip (NoC) have enormously increased the number of on-chip frequency domains that are originating from multiple on-chip clock sources. In modern battery-operated internet of things (IoT) devices, limited power budget and requirement for complex clock distribution schemes increases the usage clock multipliers. These multiple clock signal requirements are usually catered for by using frequency multipliers with clock generators. However, most of these multipliers are based on analog components that require a customized layout, involve timing uncertainties, and are power hungry and highly prone to mismatches in the process variations and environmental changes. Moreover, in modern battery-operated smart devices for IoT have very limited power budget, which makes the design of clock multipliers even more challenging. To address these issues, we propose a delay-based digital frequency multiplier, which uses 2-input XNOR gates and a true single-phase clock (TSPC) flip-flop because of pulse generation and edge detection properties, respectively. The proposed multiplier is based on the digital components, therefore, it reduces the power consumption significantly, i.e., 1.6mW, which is almost 50% lesser than other low power state-of-the-art designs. Moreover, it can operate for a wide range of input frequencies, ~400MHz to 1GHz. The Monte-Carlo simulation results are very promising as they indicate the robustness of the design against process and environmental variations.

Interactive theorem provers can overcome the scalability limitations of model checking and automated theorem provers by verifying generic circuits and universally quantified properties but they require explicit user guidance, which makes them quite uninteresting for industry usage. As a first step to overcome these issues, this paper presents a formally verified library of commonly used combinational circuits using the higher-order logic theorem prover HOL4. This library can in turn be used to verify the structural view of any arbitrary combinational circuit against its behavior with very minimal user-guidance. For illustration, we verified several combinational circuits, including a 24-bit adder/subtractor, the 8-bit shifter module of the c3540 benchmark, the 17-bit EqualZ_W module of the c2670 benchmark, a 16:1 Multiplexer, and a 512-bit Multiplier.

Low-power approximate adders provide basic building blocks for approximate computing hardware that have shown remarkable energy efficiency for error-resilient applications (like image/video processing, computer vision, etc.), especially for battery-driven portable systems. In this paper, we present a novel scalable, fast yet accurate analytical method to evaluate the output error probability of multi-bit low power adders for a predetermined probability of input bits. Our method recursively computes the error probability by considering the accurate cases only, which are considerably smaller than the erroneous ones. Our method can handle the error analysis of a wider-range of adders with negligible computational overhead. To ensure its rapid adoption in industry and academia, we have open-sourced our LabVIEW and MATLAB libraries.

Approximate circuits exploit error resilience property of applications to tradeoff computation quality (accuracy) for gaining advantage in terms of performance, power, and/or area. While state-of-the-art low-latency approximate adders provide an accuracy-area-latency configurable design space, the selection of a particular configuration from the design space is still manually done. In this paper, we analytically analyze different structural properties of low-latency approximate adders to formulate a new adder model, Quality-area optimal Low-Latency approximate Adder (QuAd). It provides an increased design space as compared to state-of-the-art, providing design points that require less logic area for the same accuracy, as compared to state-of-the-art approximate adders. Furthermore, based upon our mathematical analysis, we show that, provided a latency constraint, an adder configuration with the highest quality and lowest area requirement can effortlessly be selected from the whole design space of QuAd adder model, without requiring any optimization strategy or numerical simulation. Our experimental results validate the developed model and also the quality-area optimality of our optimal QuAd adder configuration. For functional verification and prototyping, we have used a Xilinx Virtex-6 FPGA. RTL/behavioral models and MATLAB equivalent scripts, of our proposed adder model are made open source, to facilitate further research and development.

Dynamic thermal management (DTM) techniques based on task migration provide a promising solution to mitigate thermal emergencies and thereby ensuring safe operation and reliability of Many-Core systems. These techniques can be classified as central or distributed on the basis of a central DTM controller for the whole system or individual DTM controllers for each core or set of cores in the system, respectively. However, having a trustworthy comparison between central (c-) and distributed (d-) DTM techniques to find out the most suitable one for a given system is quite challenging. This is primarily due to the systemic difference between cDTM and dDTM controllers, and the inherent non-exhaustiveness of simulation and emulation methods conventionally used for DTM analysis. In this paper, we present a novel methodology called CAnDy-TM (stands for Comparative Analysis of Dynamic Thermal Management) that employs Model Checking to perform formal comparative analysis for cDTM and dDTM techniques. We identify a set of generic functional and performance properties to provide a common ground for their comparison. We demonstrate the usability and benefits of our methodology by comparing state-of-the-art cDTM and dDTM techniques, and illustrate which technique is good w.r.t. thermal stability and other task migration parameters. Such an analysis helps in selecting the most appropriate DTM for a given chip.

Globalization trends in integrated circuit (IC) design are leading to increased vulnerability of ICs against hardware Trojans (HT). Recently, several side channel parameters based techniques have been developed to detect these hardware Trojans that require golden circuit as a reference model, but due to the widespread usage of IPs, most of the system-on-chip (SoC) do not have a golden reference. Hardware Trojans in intellectual property (IP)-based SoC designs are considered as major concern for future integrated circuits. Most of the state-of-the-art runtime hardware Trojan detection techniques presume that Trojans will lead to anomaly in the SoC integration units. In this paper, we argue that an intelligent intruder may intrude the IP-based SoC without disturbing the normal SoC operation or violating any protocols. To overcome this limitation, we propose a methodology to extract the power profile of the micro-controllers instruction sets, which is in turn used to train a machine learning algorithm. In this technique, the power profile is obtained by extracting the power behavior of the micro-controllers for different assembly language instructions. This trained model is then embedded into the integrated circuits at the SoC integration level, which classifies the power profile during runtime to detect the intrusions. We applied our proposed technique on MC8051 micro-controller in VHDL, obtained the power profile of its instruction set and then applied deep learning, k-NN, decision tree and naive Bayesian based machine learning tools to train the models. The cross validation comparison of these learning algorithm, when applied to MC8051 Trojan benchmarks, shows that we can achieve 87% to 99% accuracy. To the best of our knowledge, this is the first work in which the power profile of a microprocessor's instruction set is used in conjunction with machine learning for runtime HT detection.

Approximate multipliers are gaining importance in energy-efficient computing and require careful error analysis. In this paper, we present the error probability analysis for recursive approximate multipliers with approximate partial products. Since these multipliers are constructed from smaller approximate multiplier building blocks, we propose to derive the error probability in an arbitrary bit-width multiplier from the probabilistic model of the basic building block and the probability distributions of inputs. The analysis is based on common features of recursive multipliers identified by carefully studying the behavioral model of state-of-the-art designs. By building further upon the analysis, Probability Mass Function (PMF) of error is computed by individually considering all possible error cases and their inter-dependencies. We further discuss the generalizations for approximate adder trees, signed multipliers, squarers and constant multipliers. The proposed analysis is validated by applying it to several state-of-the-art approximate multipliers and comparing with corresponding simulation results. The results show that the proposed analysis serves as an effective tool for predicting, evaluating and comparing the accuracy of various multipliers. Results show that for the majority of the recursive multipliers, we get accurate error performance evaluation. We also predict the multipliers' performance in an image processing application to demonstrate its practical significance.

Approximate adders are widely being advocated as a means to achieve performance gain in error resilient applications. In this paper, a generic methodology for analytical modeling of probability of occurrence of error and the Probability Mass Function (PMF) of error value in a selected class of approximate adders is presented, which can serve as performance metrics for the comparative analysis of various adders and their configurations. The proposed model is applicable to approximate adders that comprise of subadder units of uniform as well as non-uniform lengths. Using a systematic methodology, we derive closed form expressions for the probability of error for a number of state-of-the-art high-performance approximate adders. The probabilistic analysis is carried out for arbitrary input distributions. It can be used to study the dependence of error statistics in an adder's output on its configuration and input distribution. Moreover, it is shown that by building upon the proposed error model, we can estimate the probability of error in circuits with multiple approximate adders. We also demonstrate that, using the proposed analysis, the comparative performance of different approximate adders can be correctly predicted in practical applications of image processing.

Approximate adders are widely being advocated for developing hardware accelerators to perform complex arithmetic operations. Most of the state-of-the-art accuracy configurable approximate adders utilize some integrated Error Detection and Correction (EDC) circuitry. Consequently, the accumulated area overhead due to the EDC (integrated within individual adders) is significant. In this paper, we propose a low-cost Consolidated Error Correction (CEC) unit, that essentially corrects the accumulated error at the accelerator output. The proposed CEC is based on a mathematical model of approximation error. We integrate our CEC unit in approximate hardware accelerators deployed in different applications to demonstrate its area savings and speed enhancement compared to state-of-the-art.

The task of whole-body motion planning for humanoid robots is challenging due to its high-DOF nature, stability constraints, and the need for obstacle avoidance and movements that are efficient. Over the years, various approaches have been adopted to solve this problem such as bounding-box models and jacobian-based techniques. More commonly though, sampling-based algorithms are employed for this task since they perform admirably well in high-dimensional spaces. As an alternative, search-based planners offer improvements in terms of optimality and consistency of the solution. However, they are normally considered impractical for high-dimensional motion planning. In this paper, we present a heuristic search-based motion planning framework for humanoid robots that circumvents the drawbacks traditionally associated with search-based planners while catering to the specific requirements of humanoid motion planning. This is achieved primarily through a combination of informative yet computationally inexpensive heuristics, carefully crafted motion primitives as atomic actions, and a whole body inverse kinematics solver for achieving desired end effector orientations. The experimental results show the ability of our framework to perform complex motion planning tasks quickly and efficiently.

Single clock distribution over a large high performance chip can be very challenging. This led to evolution of globally asynchronous and locally Synchronous (GALS) systems in modern deep sub-micron (DSM) technology. In GALS mostly bundled data protocols which are based on handshake mechanism, are used for data transfer. But these protocols rely on timing assumptions between handshake signals and data values that causes timing closure problems, which poses strict constraints in system-on-chip (SoC) design. This work leverages quasi delay insensitive (QDI) designs to propose GALS design templates. This will facilitate the use of GALS systems in a conventional digital design flow with minimal intervention to interfacing modules. Modifications for two different quasi delay insensitive (QDI) asynchronous designs have been suggested, implemented and verified by using the proposed templates. Power, energy and latency have been compared for two different interfaces.

Globalization trends in integrated circuit (IC) design using deep submicron (DSM) technologies are leading to increased vulnerability of ICs against malicious intrusions. These malicious intrusions are referred as hardware Trojans. One way to address this threat is to utilize unique electrical signatures of ICs. However, this technique requires analyzing extensive sensor data to detect the intruded integrated circuits. In order to overcome this limitation, we propose to combine the signature extraction mechanism with machine learning algorithms to develop a self-learning framework that can detect the intruded integrated circuits. The proposed approach applies the lazy, eager or probabilistic learners to generate self-learning prediction model based on the electrical signatures. In order to validate this framework, we applied it on a recently proposed signature based hardware Trojan detection technique. The cross validation comparison of these learner shows that eager learners are able to detect the intrusion with 96% accuracy and also require less amount of memory and processing power compared to other machine learning techniques.

Ensuring the correctness of middleware that ensures interoperability of various medical devices is one of the biggest challenges in the e-health domain. Traditionally, these Device Interoperability Middleware (DIM) are analyzed using software testing. However, given the inherent incompleteness of testing and the randomness of the user behaviours, the analysis results are not guaranteed to be accurate. Some of these inaccuracies in analysis results could even put human life at risk. In order to overcome these limitations, we propose to use a probabilistic model checker PRISM for analyzing DIM. The proposed approach allows us to rigorously verify reliability properties of the given DIM and thus allows the designers to make appropriate measures to design more reliable systems. For illustration, we formally analyze a middleware that uses the HL7 FHIR and ontology-based description of the devices and a communication protocol to bridge the gap in heterogeneity for dealing with different vendors and incompatible data formats.

Just like any other algorithm, Dynamic Thermal Management (DTM) schemes for multi-core architectures are susceptible to errors. Moreover, due to the wide spread usage and safety-critical nature of these schemes, there is a key demand for robust verification of these schemes before deployment. Traditional analysis techniques, like simulation and emulation, are inherently incomplete and therefore they cannot guarantee a complete absence of bugs. In this paper, we present a generic formal verification methodology, based of probabilistic model checking, for verifying decentralized DTM schemes. The paper provides a general modelling approach for developing a Markovian model of any decentralized DTM scheme. Moreover, we identify a set of generic probabilistic properties that can be of an interest to DTM scheme designers. For illustration purposes, the proposed methodology is used to verify Thermal Aware Agent Based Power Economy (TAPE), which is a state-of-the-art decentralized DTM scheme.

In recent times, Wireless Sensor Networks (WSNs) have shown a great potential for monitoring physical or environmental conditions in a variety of safety and financial-critical applications, ranging from medicine to transportation and surveillance. Given the extreme conditions of most of the WSN environments, it is very important to make WSN communication resilient to network failures. Various data transport protocols have been proposed in the literature to serve this purpose. The reliability of these WSN data transport protocols is usually assessed by using Reliability Block Diagrams (RBDs). Traditionally, RBD-based reliability analyses of WSN data transport protocols is done using paper-and-pencil proofs or computer simulations, which cannot ascertain absolute correctness due to their inherent incompleteness. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL to conduct the RBD-based reliability analysis of WSN data transport protocols. In particular, the paper provides a higher-order-logic formalization of series, parallel and parallel-series RBDs. These RBDs are then used to do the formal reliability analysis of the end-to-end (e2e) data transport mechanism, and the Event to Sink Reliable Transport (ESRT) and Reliable Multi-Segment Transport (RMST) data transport protocols.

Abstract In the context of wireless sensor networks (WSNs), the ability to detect an intrusion event is the most desired characteristic. Due to the randomness in nodes scheduling algorithm and sensor deployment, probabilistic techniques are used to analyze the detection properties of WSNs. However traditional probabilistic analysis techniques, such as simulation and model checking, do not ensure accurate results, which is a severe limitation considering the mission-critical nature of most of the WSNs. In this paper, we overcome these limitations by using higher-order-logic theorem proving to formally analyze the detection properties of randomly-deployed WSNs using the randomized scheduling of nodes. Based on the probability theory, available in the HOL theorem prover, we first formally reason about the intrusion period of any occurring event. This characteristic is then built upon to develop the fundamental formalizations of the key detection metrics: the detection probability and the detection delay. For illustration purposes, we formally analyze the detection performance of a WSN deployed for border security monitoring.

Fast Health Interoperable Resources (FHIR) is the recently proposed standard from HL7. Its distinguishing features include the user friendly implementation, support of built-in terminologies and for widely-used web standards. Given the safety-critical nature of FHIR, the rigorous analysis of e-health systems using the FHIR is a dire need since they are prone to failures. As a first step towards this direction, we propose to use probabilistic model checking, i.e., a formal probabilistic analysis approach, to assess the reliability of a typical e-health system used in hospitals based on the FHIR standard. In particular, we use the PRISM model checker to analyze the Markov Decision Process (MDP) and Continuous Time Markov Chain (CTMC) models to assess the failure probabilities of the overall system.

A molecular pathway primarily refers to a chain of chemical reactions within a cell and their analysis plays a vital role in developing effective drugs for various human infectious diseases, such as Cancer and Malaria. However, the existing cell pathway analysis techniques, such as paper and pencil proof methods, graph theory and Petri Nets, are either incapable of assuring accurate results or only deal with certain biological systems, which limits the usage of these techniques in the safety-critical field of human medicine. In this paper, we propose to use higher-order-logic theorem proving to accurately deduce results of biological reactions in a pathway. The proposed framework is primarily based on Z-Syntax, which is a formal language to model molecular reactions and is based on three logical operators and four inference rules. As a first step towards this goal, we formalize these operators and inference rules in higher-order logic and provide automated reasoning support for verifying molecular reactions using the HOL4 theorem prover. For illustration purposes, we present the formal verification of a reaction involving TP53 degradation.

The accuracy of control systems analysis is of paramount importance as even minor design flaws can lead to disastrous consequences in this domain. This paper provides a higher-order-logic theorem proving based framework for the formal analysis of steady state errors in feedback control systems. In particular, we present the formalization of control system foundations, like transfer functions, summing junctions, feedback loops and pickoff points, and steady state error models for the step, ramp and parabola cases. These foundations can be built upon to formally specify a wide range of feedback control systems in higher-order logic and reason about their steady state errors within the sound core of a theorem prover. The proposed formalization is based on the complex number theory of the HOL-Light theorem prover. For illustration purposes, we present the steady state error analysis of a solar tracking control system.

Simulation is the state-of-the-art analysis technique for distributed thermal management schemes. Due to the numerous parameters involved and the distributed nature of these schemes, such non-exhaustive verification may fail to catch functional bugs in the algorithm or may report misleading performance characteristics. To overcome these limitations, we propose a methodology to perform formal verification of distributed dynamic thermal management for many-core systems. The proposed methodology is based on the SPIN model checker and the Lamport timestamps algorithm. Our methodology allows specification and verification of both functional and timing properties in a distributed many-core system. In order to illustrate the applicability and benefits of our methodology, we perform a case study on a state-of-the-art agent-based distributed thermal management scheme.

Dynamic systems that exhibit probabilistic behavior represent a large class of man-made systems such as communication networks, air traffic control, and other mission-critical systems. Evaluation of quantitative issues like performance and dependability of these systems is of paramount importance. In this paper, we propose a generalized methodology to formally reason about probabilistic systems within a theorem prover. We present a formalization of measure theory in the HOL theorem prover and use it to formalize basic concepts from the theory of probability. We also use the Lebesgue integration to formalize statistical properties of random variables. To illustrate the practical effectiveness of our methodology, we formally prove classical results from the theories of probability and information and use them in a data compression application in HOL.

Real-time systems usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism, which makes their performance analysis quite complex. Thus, traditional techniques, such as simulation, fail to produce reasonable results. Formal methods pose an interesting solution but they usually lack the capabilities to reason about quantitative time and probabilistic properties, which play a vital role in performance analysis. This paper addresses this issue by presenting a formal approach for assessing the performance of a real-time system. To describe the evolution of the system, we use a real-time rewriting logic, in which we mechanize the extraction of quantitative information from a timed model. To evaluate the performance, we first consider the set of runs obtained from different initial input values that are not equivalent modulo the equational theory associated with the model. The overall performance of the system is then evaluated as the performance of each run weighted by its probability mass function. In order to illustrate the practical effectiveness of the proposed approach, we present the formal modeling and performance analysis of a simple search engine.

Reliability analysis has become a tool of fundamental importance to virtually all electrical and computer engineers because of the extensive usage of hardware systems in safety and mission critical domains, such as medicine, military, and transportation. Due to the strong relationship between reliability theory and probabilistic notions, computer simulation techniques have been traditionally used to perform reliability analysis. However, simulation provides less accurate results and cannot handle large-scale systems due to its enormous CPU time requirements. To ensure accurate and complete reliability analysis and thus more reliable hardware designs, we propose to conduct a formal reliability analysis of systems within the sound core of a higher order logic theorem prover (HOL). In this paper, we present the higher order logic formalization of some fundamental reliability theory concepts, which can be built upon to precisely analyze the reliability of various engineering systems. The proposed approach and formalization is then utilized to analyze the repairability conditions for a reconfigurable memory array in the presence of stuck-at and coupling faults.

Automatic-repeat-request (ARQ) protocols are widely used in modern data communications to guarantee reliable transmission over imperfect physical links. The behavior of an ARQ protocol largely depends on a number of network parameters and traditionally simulation is used for their performance analysis. However, simulation provides less accurate results and usually requires enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to conduct the performance analysis of ARQ protocols in the environment of a higher-order-logic theorem prover (HOL). We present an approach to formally model the delay characteristics of ARQ protocols as a function of geometric random variable in higher-order-logic. In particular, we develop higher-order-logic models that describe the delay behavior of three basic types of ARQ protocols, i.e., Stop-and-Wait, Go-Back-N and Selective-Repeat. The paper also includes the verification of the average message delay relations for these three protocols in HOL.