Approximate computing (AC) has gained traction as an alternative computing method for energy-efficient processing. This article proposes the exploitation of AC to address the memory wall. The proposed model predicts the memory load value using machine learning (ML). Subsequently, the ML model is a load value approximator (LVA) where the generated value is accepted as-is. The proposed LVA was tested under various approximate conditions, where 50% to 95% of the load instructions were approximated using a set of multimedia applications. The memory access operation using the proposed LVA was more than \(6\times\) faster in multiple cases. Additionally, the applications tested ran on average \(1.83\times\) faster. The peak signal-to-noise ratio (PSNR) exceeded 37 dB in several scenarios. The average normalized mean absolute error (NMAE) was 4.54%.

This paper addresses two essential memory bottlenecks: 1) memory wall, and 2) bandwidth wall. To accomplish this objective, we propose a machine learning (ML) based model that estimates the values to be loaded from the memory by a wide range of error-resilient applications. The proposed model exploits the feature of tightened value locality, which consists of a periodic load of few unique values. The proposed ML-based load value approximator (LVA) requires minimal overhead as it relies on a hash that encodes the history of events, e.g., history of accessed addresses, and values that can be extracted from the load instruction to be approximated. The proposed LVA completely eliminates memory accesses, i.e., 100% of accesses, in runtime and thus addresses the issue of memory wall and bandwidth wall. Compared to related work, our LVA delivers a maximum accuracy of 95.16% while offering a higher reduction in memory accesses.

In the healthcare context, remote monitoring based on the Internet of Things (IoT) technology is a widespread application. Underlying entities are interacting to bring up various services, so that their communication has to be ensured without defects such as deadlocks. The correct validation of these IoT applications is a major concern because of their distributed and concurrent features, as well as, the safety-critical nature of the health context. In this paper, we show how we use a model checking approach to accurately validate the behavior of an IoT-based healthcare application. We then focus on verifying three important classes of properties namely safety, liveness, and absence of deadlock. The verification is guaranteed by means of the UPPAAL model checker.

Stochastic computing allows a drastic reduction in hardware complexity using serial processing of bit streams. While the induced high computing latency can be overcome using integrated optics technology, the design of realistic optical stochastic computing architectures calls for energy efficient switching devices. Photonics Crystal (PhC) nanocavities are μm 2 scale devices offering 100fJ switching operation under picoseconds-scale switching speed. Fabrication process allows controlling the Quality factor of each nanocavity resonance, leading to opportunities to implement architectures involving cascaded gates and multi-wavelength signaling. In this paper, we investigate the design of cascaded gates architecture using nanocavities in the context of stochastic computing. We propose a transmission model considering key nanocavity device parameters, such as Quality factors, resonance wavelength, and switching efficiency. The model is calibrated with experimental measurements. We propose the design of XOR gate and multiplexer. We illustrate the use of the gates to design an edge detection filter. System-level exploration of laser power, bit-stream length and bit-error rate is carried out for the processing of gray-scale images. The results show that the proposed architecture leads to 8.5nJ/pixel energy consumption and 512ns/pixel processing time.

This paper tackles the energy efficiency optimization in wireless communication networks, where multiple unmanned aerial vehicles (UAVs) deploy power transfer towards several energy receivers (ERs) to enable their uplink data transmissions through non-orthogonal multiple access (NOMA). Utilizing a formulated closed-form expression for energy efficiency (EE), a resource allocation mechanism aiming to maximize the system's EE is developed. To address this optimization problem, two algorithms are proposed that use Lagrangian optimization and gradient descent methods. For the simulations, three different cases, depending on the ERs' service demands, are considered. Numerical results along with comparisons are given and illustrated. The results show an enhancement in the energy efficiency for the cases that consider the needs of the ERs. Moreover, in all cases, the NOMA scheme's EE results are better than OMA with respect to the optimal charging time.

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.

Approximate computing allows improving design energy efficiency at the cost of computing accuracy. Stochastic computing is an approximate computing technique, where numbers are represented as probabilities using stochastic bit streams. The serial processing of the bit streams leads to reduced hardware complexity but induces high processing latency. Silicon photonics has the potential to overcome this limitation thanks to high propagation speed of signals and high bandwidth. However, the technology remains costly, which calls for optical accelerators capable to adapt to application-specific requirements. In this paper, we propose a reconfigurable optical accelerator capable to adapt to computing accuracy, energy efficiency, and throughput objectives. The architecture can be configured to execute i) 4thorder function for high accuracy processing or ii) 2ndorder function for high-energy efficiency or high throughput purposes. Evaluations are carried out using image processing Gamma correction application. Compared to a static architecture for which accuracy is defined at design time, the proposed architecture leads to 36.8% energy overhead but increases the range of reachable accuracy by 65%.

This paper investigates the energy efficiency optimization in a wireless communication network in which an unmanned aerial vehicle (UAV) deploys information and power transfer towards co-located information and energy receivers to enable downlink and uplink data transmission through non-orthogonal multiple access (NOMA). Using a constructed closed-form expression for the energy efficiency, a resource allocation mechanism aiming at maximizing the energy efficiency of the system is developed. To this end, an algorithm which jointly takes into account the downlink and uplink stages is proposed, using Lagrangian optimization and gradient decent methods. Numerical results and comparisons are provided. In particular, the results show an enhancement in energy efficiency for the NOMA scheme compared with OMA, and that less wireless power transfer time will be needed from the UAV to simultaneously charge energy receivers when using NOMA.

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.

Parametric yield is a significant threat to the reliability of nanoscale analog and mixed-signal circuits. A critical yet challenging problem of yield estimation is to account for multiple circuit performance. In this paper, we propose a novel nonparametric statistical verification methodology to efficiently estimate the parametric yield due to 65-nm technology for multiperformance constraints. Our proposed approach exploits the fact that circuit parameters variation has different impacts on the circuit performance. Hence, a global sensitivity analysis classifies the circuit parameters according to their influence on the desired circuit performances. Based on this classification, an efficient joint recurrence verification (JRV) algorithm, a procedure inspired from DNA analysis, is performed on the most “critical/influential” parameters. A global hypothesis testing procedure is then performed based on the computed JRV metrics. We demonstrate the effectiveness of our methodology on two benchmark circuits. The acquired results show the ability of our approach to handle multiple corners and multiple performances yield problems with up to 11× speedup compared to conventional techniques with an average error smaller than 3%.

Hadoop has become a popular framework for processing data-intensive applications in cloud environments. A core constituent of Hadoop is the scheduler, which is responsible for scheduling and monitoring the jobs and tasks, and rescheduling them in case of failures. Although fault-tolerance mechanisms have been proposed for Hadoop, the performance of Hadoop can be significantly impacted by unforeseen events in the cloud environment. In this paper, we introduce a dynamic and failure-aware framework that can be integrated within Hadoop scheduler and adjust the scheduling decisions based on collected information about the cloud environment. Our framework relies on predictions made by machine learning algorithms and scheduling policies generated by a Markovian Decision Process (MDP), to adjust its scheduling decisions on the fly. Instead of the fixed heartbeat-based failure detection commonly used in Hadoop to track active TaskTrackers (i.e., nodes that process the scheduled tasks), our proposed framework implements an adaptive algorithm that can dynamically detect the failures of the TaskTracker. To deploy our proposed framework, we have built, ATLAS+, an AdapTive Failure-Aware Scheduler for Hadoop. To assess the performance of ATLAS+, we conduct a large empirical study on a 100-node Hadoop cluster deployed on Amazon Elastic MapReduce (EMR), comparing the performance of ATLAS+ with those of three Hadoop schedulers (FIFO, Fair, and Capacity). Results show that ATLAS+ outperforms FIFO, Fair, and Capacity schedulers. ATLAS+ can reduce the number of failed jobs by up to 43 percent and the number of failed tasks by up to 59 percent. On average, ATLAS+ could reduce the total execution time of jobs by 10 minutes, which represents 40 percent of the job execution times, and by up to 3 minutes for tasks, which represents 47 percent of the task execution time. ATLAS+ also reduced CPU and memory usage by 22 and 20 percent, respectively.

Stochastic computing (SC) allows reducing hardware complexity and improving energy efficiency of error resilient applications. However, a main limitation of the computing paradigm is the low throughput induced by the intrinsic serial computing of bit-streams. In this paper, we address the implementation of SC in the optical domain, with the aim to improve the computation speed. We implement a generic optical architecture allowing the execution of polynomial functions. We propose design methods to explore the design space in order to optimize key metrics such as circuit robustness and power consumption. We show that a circuit implementing a 2ndorder polynomial degree function and operating at 1Ghz leads to 20.1pJ laser consumption per computed bit.

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.

This paper investigates the energy efficiency optimization in a wireless communication network where devices are wirelessly powered via unmanned aerial vehicle (UAV) to enable uplink data transmission. First, the path loss of the air-to-ground channels is minimized by optimizing the position of the UAV depending on the ground nodes' service demands. Then, using the optimized positioning and a closed-form expression for the energy efficiency, a resource allocation aiming at maximizing the energy efficiency is developed. To this end, two algorithms are proposed, using Lagrangian optimization and gradient decent methods. Numerical results and comparisons are provided. In particular, the results show an enhancement in energy efficiency and reduced wireless power charging time when the ground nodes' demands are taken into consideration.

Abstract Quantum computing systems promise to increase the capabilities for solving problems which classical computers cannot handle adequately, such as integers factorization. In this paper, we present a formal modeling and verification approach for optical quantum circuits, where we build a rich library of optical quantum gates and develop a proof strategy in higher-order logic to reason about optical quantum circuits automatically. The constructed library contains a variety of quantum gates ranging from 1-qubit to 3-qubit gates that are sufficient to model most existing quantum circuits. As real world applications, we present the formal analysis of several quantum circuits including quantum full adders and the Grover’s oracle circuits, for which we have proved the behavioral correctness and calculated the operational success rate, which has never been provided in the literature. We show through several case studies the efficiency of the proposed framework in terms of the scalability and modularity.

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.

Existing yield analysis methods are computationally expensive and generally encounter challenges with high-dimensional process parameters space. In this paper, we propose a new method for accelerated and reliable computation of parametric yield that combines the advantages of sparse regression and satisfiability modulo theory (SMT) solving techniques, and avoids issues in both. The key idea is to characterize the failure regions as a collection of hyperrectangles in the parameters space. Toward this goal, the method constructs sparse polynomial models based on adaptive least absolute shrinkage and selection operator to find low degree approximations of the circuit performances. A procedure inspired by statistical model checking is then introduced to assess the model accuracy. Given the constructed models, an SMT-based solving algorithm is employed to locate the failure hyperrectangles in the parameters space. The yield estimation is based on a geometric calculation of probabilistic volumes subtended by the located hyperrectangles. We demonstrate the effectiveness of our method using circuits that require expensive run-time simulation during yield evaluation. They include: an integrated ring oscillator, a 6T static RAM cell and a multistage fully-differential amplifier. Experimental results show that the proposed method is suitable for handling problems with tens of process parameters. Meanwhile, it can provide 5×-2000× speed-up over Monte Carlo methods, when a high prediction accuracy is required.

This paper presents a novel approach for improving automated analog yield optimization using a two step exploration strategy. First, a global optimization phase relies on a modified Lipschitizian optimization to sample the potential optimal sub-regions of the feasible design space. The search locates a design point near the optimal solution that is used as a starting point by a local optimization phase. The local search constructs linear interpolating surrogate models of the yield to explore the basin of convergence and to rapidly reach the global optimum. Experimental results show that our approach locates higher quality design points in terms of yield rate within less run time and without affecting the accuracy.

Abstract Reproducing a bug that caused a system to crash is an important task for uncovering the causes of the crash and providing appropriate fixes. In this paper, we propose a novel crash reproduction approach that combines directed model checking and backward slicing to identify the program statements needed to reproduce a crash. Our approach, named JCHARMING (Java CrasH Automatic Reproduction by directed Model checkING), uses information found in crash traces combined with static program slices to guide a model checking engine in an optimal way. We show that JCHARMING is efficient in reproducing bugs from 10 different open source systems. Overall, JCHARMING is able to reproduce 80% of the bugs used in this study in an average time of 19 min. Copyright © 2016 John Wiley & Sons, Ltd.

This paper explores the impact of device process variations on the performance of analog circuits. We propose a new verification approach called Cross Recurrence Verification (CRV). Circuit output similarities between an ideal circuit that has parameters set to the nominal values and a non-ideal circuit with process variation due to 65nm fabrication process are computed. CRV is used to find the percentage of recurrence and the longest common output subsequence that matches the output subsequence of an ideal circuit. The performed analysis showed the potential of this novel technique to enhance/improve the verification process of Analog circuits. The proposed approach is illustrated on a five stage ring oscillator. The obtained results demonstrate the robustness, accuracy and flexibility of our methodology.

Abstract Optics technology is being increasingly used in mainstream industrial and research domains such as terrestrial telescopes, biomedical imaging and optical communication. One of the most widely used modeling approaches for such systems is Gaussian optics, which describes light as a beam. In this paper, we propose to use higher-order-logic theorem proving for the analysis of Gaussian optical systems. In particular, we present the formalization of Gaussian beams and verify the corresponding properties such as beam transformation, beam waist radius and location. Consequently, we build formal reasoning support for the analysis of quasi-optical systems. In order to demonstrate the effectiveness of our approach, we present a case study about the receiver module of a real-world Atacama Pathfinder Experiment (APEX) telescope.

Traditionally, model order reduction methods have been used to reduce the computational complexity of mathematical models of dynamic systems, while preserving their functional characteristics. This technique can also be used to fasten analog circuit simulations without sacrificing their highly nonlinear behavior. In this paper, we present an iterative approach for reducing the computational complexity of nonlinear analog circuits using piecewise linear approximations,k-means clustering, and Krylov space projection techniques. We model primary circuit inputs, design initial conditions, and circuit parameters as fuzzy variables with different distributions in qualitative simulations. We then iteratively fine-tune the reduced models until a model is achieved that meets a predefined performance and accuracy conformance criteria. We demonstrate the effectiveness of our method using several key nonlinear circuits: 1) a transmission line; 2) a ring oscillator; 3) a voltage controlled oscillator; 4) a phase-locked loop; and 5) an analog comparator circuit. Our experiments show that the reduced model simulations are fast and accurate compared with the existing techniques.

This paper presents an approach for enhancing analog circuit sizing using Satisfiability Modulo Theory (SMT). The circuit sizing problem is encoded using nonlinear constraints. An SMT-based algorithm exhaustively explores the design space, where the biasing-level design variables are conservatively tracked using a collection of hyperrectangles. The device dimensions are then determined by accurately relating biasing to geometry-level design parameters. We demonstrate the feasibility and efficiency of the proposed methodology on a two-stage amplifier and a folded cascode amplifier. Experimental results show that our approach can achieve higher quality in analog synthesis and unrivaled coverage of the design space.

Process variation presents a practical challenge on the performance of analog and mixed signal (AMS) circuits. This paper proposes a Monte Carlo-Jackknife (MC-JK) technique, a variant of Monte Carlo method, to verify process variation affecting the performance and functionality of AMS designs. We use a behavioral model to which we encompass device variation due to $65nm$ technology process. Next, we conduct hypothesis testing based on the MC-JK technique combined with Latin hypercube sampling in a statistical run-time verification environment. Experimental results demonstrate the robustness of our approach in verifying AMS circuits.

Hadoop has become the de facto standard for processing large data in today's cloud environment. The performance of Hadoop in the cloud has a direct impact on many important applications ranging from web analytic, web indexing, image and document processing to high-performance scientific computing. However, because of the scale, complexity and dynamic nature of the cloud, failures are common and these failures often impact the performance of jobs running in Hadoop. Although Hadoop possesses built-in failure detection and recovery mechanisms, several scheduled jobs still fail because of unforeseen events in the cloud environment. A single task failure can cause the failure of the whole job and unpredictable job running times. In this paper, we propose ATLAS (AdapTive faiLure-Aware Scheduler), a new scheduler for Hadoop that can adapt its scheduling decisions to events occurring in the cloud environment. Using statistical models, ATLAS predicts task failures and adjusts its scheduling decisions on the fly to reduce task failure occurrences. We implement ATLAS in the Hadoop framework of Amazon Elastic MapReduce (EMR) and perform a case study to compare its performance with those of the FIFO, Fair and Capacity schedulers. Results show that ATLAS can reduce the percentage of failed jobs by up to 28% and the percentage of failed tasks by up to 39%, and the total execution time of jobs by 10 minutes on average. ATLAS also reduces CPU and memory usages.

Magnetic Flux Leakage (MFL) sensors are commonly utilized to detect defects in oil and gas pipelines and determine their depths and sizes. As a preprocessing step, MFL data are often reduced into a representative feature set that is capable of accurately estimating pipeline defect depths. However, this estimation capability may vary depending on the features used, which necessitates the need for selecting the most relevant ones. In this paper, self-organizing maps (SOMs) are used as feature visualization tool for the purpose of selecting the most appropriate features. First, a self-organizing map (SOM), i.e., A two-dimensional discretized representation of the input space of the training samples for the features, is produced. The SOM weights for each individual input feature (weight plane) are displayed then visually analyzed. Irrelevant and redundant features can be efficiently spotted and removed. The remaining "good" features (i.e., Selected features) are then used as an input to a feed forward neural network for defect depth estimation. Experimental work has shown the effectiveness of the proposed approach. For instance, within ±5% error-tolerance range, the obtained estimation accuracy, using the SOM-based feature selection, is 93.1%, compared to 74% when all input features are used (i.e., No feature selection is performed), and within ±10% error-tolerance range, the obtained estimation accuracy, using the SOM-based feature selection, is 97.5%, compared to 86% when all the input features are used (i.e., No feature selection is performed).

Due to their inherent complexity, software systems are pledged to be released with bugs. These bugs manifest themselves on client's computers, causing crashes and undesired behaviors. Field crashes, in particular, are challenging to understand and fix as the information provided by the impacted customers are often scarce and inaccurate. To address this issue, there is a need to find ways for automatically reproducing the crash in a lab environment in order to fully understand its root causes. Crash reproduction is also an important step towards developing adequate patches. In this paper, we propose a novel crash reproduction approach, called JCHARMING (Java CrasH Automatic Reproduction by directed Model checkING). JCHARMING uses crash traces and model checking to identify program statements needed to reproduce a crash. Our approach takes advantage of the completeness provided by model checking while ignoring unneeded system states by means of information found in crash traces combined with static slices. We show the effectiveness of JCHARMING by applying it to seven different open source programs cumulating more than one million lines of code scattered in around 7000 classes. Overall, JCHARMING was able to reproduce 85% of the submitted bugs.

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.

Recent developments in the fabrication technology attracted the attention of optical engineers and physicists in the area of VLSI photonics. Due to the physical nature of light-wave systems and their usage in safety critical domains such as human surgeries and high budget space missions, it is indispensable to build high assurance systems. Traditionally, the analysis of such systems has been carried out by paper-and-pencil based proofs and numerical computations. However, these techniques cannot provide perfectly accurate results due to the risk of human error and inherent approximations of numerical algorithms. In order to overcome these limitations, we propose to use higher-order logic theorem proving to improve the analysis in the domain of integrated optics or VLSI photonics. In particular, this paper provides a higher-order logic formalization of optical microresonators which are the most fundamental building blocks of many photonic devices. In order to illustrate the practical utilization of our work, we present the formal analysis of 2-D microresonator lattice optical filters.

We propose an environment for the verification of analog circuits behavioral properties, where the circuit state space bounds are first computed using qualitative simulation. Then, their specified behavioral properties are verified on these bounds. The effectiveness of the method is illustrated with a tunnel diode oscillator.

Simulation cannot give a full coverage of Phase Locked Loop (PLL) behavior in presence of process variation, jitter and varying initial conditions. Qualitative Simulation is an attracting method that computes behavior envelopes for dynamical systems over continuous ranges of their parameters. Therefore, this method can be employed to verify PLLs locking property given a model that encompasses their imperfections. Extended System of Recurrence Equations (ESREs) offer a unified modeling language to model analog and digital PLLs components. In this paper, an ESRE model is created for both PLLs and their imperfections. Then, a modified qualitative simulation algorithm is used to guarantee that the PLL locking time is sound for every possible initial condition and parameter value. We used our approach to analyze a Charge Pump-PLL for a $0.18\mu m$ fabrication process and in the presence of jitter and initial conditions uncertainties. The obtained results show an improvement of simulation coverage by computing the minimum locking time and predicting a non locking case that statistical simulation technique fails to detect.

The generation of fast models for device level circuit descriptions is a very active area of research. Model order reduction is an attractive technique for dynamical models size reduction. In this paper, we propose an approach based on clustering, curve-fitting, linearization and Krylov space projection to build reduced models for nonlinear analog circuits. We demonstrate our model order reduction method for three nonlinear circuits: a voltage controlled oscillator, an operational amplifier and a digital frequency divider. Our experimental results show that the reduced models lead to an improvement in simulation speed while guaranteeing the representation of the behavior of the original circuit design.

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.

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.

Noise and process variation present a practical limit on the performance of analog circuits. This paper proposes a methodology for modeling and verification of analog designs in the presence of shot noise, thermal noise, and process variations. The idea is to use stochastic differential equations to model noise in additive and multiplicative form and then combine process variation due to 0.18 μm technology in a statistical run-time verification environment. The efficiency of Monte-Carlo and Bootstrap statistical techniques are compared for a Colpitts oscillator and a phase locked loop-based frequency synthesizer circuit.

Large analog circuit models are very expensive to evaluate and verify. New techniques are needed to shorten time-to-market and to reduce the cost of producing a correct analog integrated circuit. Model order reduction is an approach used to reduce the computational complexity of the mathematical model of a dynamical system, while capturing its main features. This technique can be used to reduce an analog circuit model while retaining its realistic behavior. In this paper, we present an approach to model order reduction of nonlinear analog circuits. We model the circuit using fuzzy differential equations and use qualitative simulation and K-means clustering to discretion efficiently its state space. Moreover, we use a conformance checking approach to refine model order reduction steps and guarantee simulation acceleration and accuracy. In order to illustrate the effectiveness of our method, we applied it to a transmission line with nonlinear diodes and a large nonlinear ring oscillator circuit. Experimental results show that our reduced models are more than one order of magnitude faster and accurate when compared to existing methods.

We present a variant of dynamic time warping (DTW) algorithm to verify jitter properties associated with an analog and mixed signal (AMS) design. First, the AMS design with stochastic jitter component is modeled using a system of difference equations for analog and digital parts and then evaluated in a MATLAB simulation environment. Second, MonteCarlo simulation is combined with DTW and hypothesis testing to determine the probability of acceptance/rejection of those simulation results. Our approach is illustrated on analyzing the jitter effect on the “lock-time” property of a phase locked loop (PLL) based frequency synthesizer.

This paper relies on the longest closest subsequence (LCSS), a variant of the longest common subsequence (LCS), to account for noise and process variations inherited by analog circuits. The idea is to use stochastic differential equations (SDE) to model the design and integrate device variation due to the 0.18μm fabrication process in a MATLAB simulation environment. LCSS is used to find the longest and closest subsequence that matches with the subsequence of an ideal circuit. We illustrate the proposed approach on a Colpitts oscillator circuit. Advantages of the proposed methods are robustness and flexibility to account for wide range of variations.

On behalf of the organizing and program committee, we would like to welcome you to the 29thIEEE International Conference on Computer Design 2011. The International Conference on Computer Design (ICCD) encompasses a wide range of technical topics and provides an ideal environment to discuss practical and theoretical work that enables cross-pollination. The ICCD venue and program reflect this goal. This year the conference is being held at the beautiful campus of the University of Massachusetts at Amherst, United States.

Finite state machines (FSMs) are the backbone of sequential circuit design. In this paper, a new FSM watermarking scheme is proposed by making the authorship information a non-redundant property of the FSM. To overcome the vulnerability to state removal attack and minimize the design overhead, the watermark bits are seamlessly interwoven into the outputs of the existing and free transitions of state transition graph (STG). Unlike other transition-based STG watermarking, pseudo input variables have been reduced and made functionally indiscernible by the notion of reserved free literal. The assignment of reserved literals is exploited to minimize the overhead of watermarking and make the watermarked FSM fallible upon removal of any pseudo input variable. A direct and convenient detection scheme is also proposed to allow the watermark on the FSM to be publicly detectable. Experimental results on the watermarked circuits from the ISCAS'89 and IWLS'93 benchmark sets show lower or acceptably low overheads with higher tamper resilience and stronger authorship proof in comparison with related watermarking schemes for sequential functions.

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.

We model and verify analog designs in the presence of noise and process variation using an automated theorem prover, MetiTarski. Due to the statistical nature of noise, we propose to use stochastic differential equations (SDE) to model the designs. We find a closed form solution for the SDEs, then integrate the device variation due to the 0.18¿m fabrication process and verify properties using MetiTarski. We illustrate the proposed approach on an inverting Op-Amp Integrator and a Band-Gap reference bias circuit.

On behalf of the organizing and program committee, we would like to welcome you to the 28thIEEE International Conference on Computer Design 2010. The International Conference on Computer Design (ICCD) encompasses a wide range of technical topics and provides an ideal environment to discuss practical and theoretical work that enables cross-pollination. The ICCD venue and program reflect this goal. Being a truly international venue, this year the conference is held in the exciting multi-cultural city of Amsterdam, the Netherlands.

Deep datapath and algorithm complexity have made the verification of floating-point units a very hard task. Most simulation and reachability analysis verification tools fail to verify a circuit with a deep datapath like most industrial floating-point units. Theorem proving, however, offers a better solution to handle such verification. In this paper, we have hierarchically formalized and verified a hardware implementation of the IEEE-754 table-driven floating-point exponential function algorithm using the higher-order logic (HOL) theorem prover. The high ability of abstraction in the HOL verification system allows its use for the verification task over the whole design path of the circuit, starting from gate-level implementation of the circuit up to a high-level mathematical specification.

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.

MetiTarski, an automatic theorem prover for inequalities on real-valued elementary functions, can be used to verify properties of analog circuits. First, a closed form solution to the model of the circuit is obtained. We present two techniques for obtaining the closed form solution. One is based on piecewise linear modeling and the inverse Laplace transform. The other is based on small-signal analysis and transfer function theory. Second, the properties of interest are turned into a set of inequalities involving analytic functions, which are proved automatically using MetiTarski. We verify properties concerning oscillation and the change in gain due to component tolerances.

One of the challenges faced by telecom companies is to provide robust and powerful servers that are capable to handle the great increase of the number of subscribers and to accomplish the heavy Internet-based applications that generate a tremendous traffic load. Companies evaluate their products' performance before releasing them to the market by applying a large amount of generated traffic to the telecom servers in order to measure their capability under traffic load; powerful solutions are hence needed for generating traffic and modeling various telecom protocols. In this paper, we propose a new traffic generator solution to load the mobile switching center (MSC) for the universal mobile telecommunications system (UMTS). This traffic generator loads the MSC through various mobile call scenarios such as location update, mobile call originating, mobile call terminating, and call clearing. We utilize the UML use case model to describe the functional behaviors of the traffic generator, and present the UML analysis model that provides the logical implementation of the functional behaviors of the proposed traffic generator.

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.

The correctness of group key protocols in communication systems remains a great challenge because of dynamic characteristics of group key construction as we deal with an open number of group members. In this paper, we propose a solution to model group key protocols and to verify their required properties, in particular secrecy property, using the event-B method. Event-B deals with tools allowing invariant checking, and can be used to verify group key secrecy property. We define a well-formed formal link between the group protocol model and the event-B counterpart model. Our approach is applied on a tree-based group Diffie-Hellman protocol that dynamically outputs group keys using the logical structure of a balanced binary tree.

This paper proposes an adaptive watermarking technique by modulating some closed cones in an originally optimized logic network (master design) for technology mapping. The headroom of each disjoint closed cone is evaluated based on its slack and slack sustainability. The notion of slack sustainability in conjunction with an embedding threshold enables closed cones in the critical path to be qualified as watermark hosts if their slacks can be better preserved upon remapping. The watermark is embedded by remapping only qualified disjoint closed cones randomly selected and templates constrained by the signature. This parametric formulation provides a means to capitalize on the headroom of a design to increase the signature length or strengthen the watermark resilience. With the master design, the watermarked design can be authenticated as in nonoblivious media watermarking. Experimental results show that the design can be efficiently marked by our method with low overhead.

The paper proposed a new symbolic verification methodology for proving the properties of analog and mixed signal (AMS) designs. Starting with an AMS description and a set of properties and using symbolic computation, a normal mathematical representation was extracted for the system in terms of recurrence equations. These normalized equations are used along with an induction verification strategy defined inside the computer algebra system Mathematica to prove the correctness of the properties. The methodology was applied on a third order DeltaSigma modulator

Analog and mixed signal (AMS) designs are important integrated circuits that are usually needed at the interface between the electronic system and the real world. Recently, several formal techniques have been introduced for AMS verification. In this paper, we propose a difference equations based bounded model checking approach for AMS systems. We define model checking using a combined system of difference equations for both the analog and digital parts, where the state space exploration algorithm is handled with Taylor approximations over interval domains. We illustrate our approach on the verification of several AMS designs including \Delta \Sigma modulator and oscillator circuits.

Recent advancement in hardware design urge during a transaction based model as a new intermediate design level. Supporters for the Transaction Level Modeling (TLM) trend claim its efficiency in terms of rapid prototyping and fast simulation incomparison to the classical RTL-based approach. Intuitively, from a verification point of view, faster simulation induces better coverage results. This is driven by two factors: coverage measurement and simulation guidance. In this paper, we propose to use an abstract model of the design, written in the Abstract State Machines Language(AsmL), in order to provide an adequate way for measuring the functional coverage. Then, we use this metric indefining the fitness function of a genetic algorithm proposed to improve the simulation efficiency. Finally, we compare our coverage and simulation results to:(1) random simulation at TLM; and (2) the Specman tool of Verisityat RTL.

We present in this paper a technique for the formal verification of probabilistic systems described in PMaude, a probabilistic extension of the rewriting system Maude. Our methodology is based on a numerical verification using the probabilistic symbolic model checking tool PRISM. In particular, we show how we can construct an abstract system from the runs of a model that preserve all the probabilistic properties of the latter. Then we deduce the probabilistic matrix that will be used for the verification in PRISM

In this paper we formally specify and verify an implementation of the IEEE802.11a standard physical layer based OFDM (Orthogonal Frequency Division Multiplexing) modem using the HOL (Higher Order Logic) theorem prover. The versatile expressive power of HOL helped model the original design at all abstraction levels starting from a floating-point model to the fixed-point design and then synthesized and implemented in FPGA technology. The paper also investigates the rounding error accumulated during ideal real to floating-point and fixedpoint transitions at the algorithmic level.

The importance of re-usable intellectual properties (IPs) cores is increasing due to the growing complexity of today's system-on-chip and the need for rapid prototyping. In this paper, we provide a design for verification approach of a PCI-X bus model, which is the fastest and latest extension of PCI technologies. We use two different modeling levels, namely UML and AsmL. We integrate the verification within the design phases where we use model checking and model based testing, respectively at the AsmL and SystemC levels. This case study presents an illustration of the integration of formal methods and simulations for the purpose of providing better verification results of SystemC IPs

Formal methods have been advocated for the verification of digital design where correctness is proved mathematically. In contrast to digital designs, the verification of analog and mixed signal systems is a challenging task that requires lots of expertise and deep understanding of their behavior. In this paper, we present a run-time verification methodology based on monitoring the behavior (solution flow) of analog circuits. Monitors are deterministic timed automata that can be synthesized from temporal properties. For illustration purposes, we applied our methodology on the verification of the oscillation property of a tunnel diode oscillator.

This paper proposes a framework for the incorporation of formal methods in the design flow of digital signal processing (DSP) systems in a rigorous way. In the proposed approach, DSP descriptions were modeled and verified at different abstraction levels using higher order logic based on the higher order logic (HOL) theorem prover. This framework enables the formal verification of DSP designs that in the past could only be done partially using conventional simulation techniques. To this end, a shallow embedding of DSP descriptions in HOL at the floating-point (FP), fixed-point (FXP), behavioral, register transfer level (RTL), and netlist gate levels is provided. The paper made use of existing formalization of FP theory in HOL and a parallel one developed for FXP arithmetic. The high ability of abstraction in HOL allows a seamless hierarchical verification encompassing the whole DSP design path, starting from top-level FP and FXP algorithmic descriptions down to RTL, and gate level implementations. The paper illustrates the new verification framework on the fast Fourier transform (FFT) algorithm as a case study.

Transaction-level modeling allows exploring several SoC design architectures, leading to better performance and easier verification of the final product. In this paper, we present an approach to design and verify SystemC models at the transaction level. We integrate the verification as part of the design flow where we first model both the design and the properties (written in Property Specification language) in Unifed Modeling Language (UML); then, we translate them into an intermediate format modeled with AsmL [language based on Abstract State Machines (ASM)]. The AsmL model is used to generate a finite state machine of the design, including the properties. Checking the correctness of the properties is performed on the fly while generating the state machine. Finally, we translate the verified design to SystemC and map the properties to a set of assertions (as monitors in C#) that can be reused to validate the design at lower levels by simulation. For existing SystemC designs, we propose to translate the code back to AsmL in order to apply the same verification approach. At the SystemC level, we also present a genetic algorithm to enhance the assertions coverage. We will ensure the soundness of our approach by proving the correctness of the SystemC-to-AsmL and AsmL-to-SystemC transformations. We illustrate our approach on two case studies including the PCI bus standard and a master/slave generic architecture from the SystemC library.

Sharing IP blocks in today's competitive market poses significant high security risks. Creators and owners of IP designs want assurances that their content will not be illegally redistributed by consumers, and consumers want assurances that the content they buy is legitimate. Recently, digital watermarking emerged as a candidate solution for copyright protection of IP blocks. In this paper, we propose a new approach for watermarking IP designs based on the embedding of the ownership proof as part of the IP design's finite state machine (FSM). The approach utilizes coinciding as well as unused transitions in the state transition graph of the design. Our approach increases the robustness of the watermark and allows a secure implementation, hence enabling the development of the first public-key IP watermarking scheme at the FSM level. We also define for our approach, and use experimental measures to prove its robustness.

Transaction level modeling allows several SoC design architectures to be explored, leading to better performance and easier verification of the final product. We present an approach to design and verify SystemC models at the transaction level. We integrate the verification as part of the design-flow. In this approach, we first model both the design and the properties (written in PSL - Property Specification Language) in UML. Then, we translate them into an intermediate format modeled by abstract state machines (ASM). The ASM model is used to generate an FSM of the design including the properties. Checking the correctness of the properties is performed on-the-fly while generating the state machine. Finally, we translate the verified design to SystemC and map the properties to a set of assertions (as monitors in C#) that can be re-used to validate the design at lower levels through simulation. We illustrate our approach on two case studies, the PCI bus standard and a generic master/slave architecture from the SystemC library.

In this paper, we present a technique to design and verify the look-aside (LA-1) interface standard used in network processors. Our design flow includes several refinements starting from an informal UML specification until getting to an RTL modeled in Verilog. We integrate the verification of the LA-interface in the design flow by considering two intermediate levels: (1) abstract state machines (ASM); and (2) SystemC. The first one serves the verification by model checking of a set of PSL properties, while the second includes a set of assertions to be verified by simulation. To evaluate the performance of our approach, we used the rule-base model checker to verify the same properties; and the OVL library to verify the same assertions.

The Signal Processing WorkSystem (SPW) of Cadence is an integrated framework for developing DSP and communications products. Formal verification is a complementary technique to simulation based on mathematical logic. The HOL system is an environment for interactive theorem proving in a higher-order logic. It has an open user-extensible architecture which makes it suitable for providing proof support for embedded languages. In this paper, we propose an approach to model SPW descriptions at different abstraction levels in HOL based on the shallow embedding technique. This will enable the formal verification of SPW designs which in the past could only be verified partially using conventional simulation techniques. We illustrate this novel application through a simple case study of a Notch filter.

Multiway Decision Graphs (MDGs) are efficient diagrams suitable for the modeling and automatic verification of register transfer level designs. The MDG tools provide a first-order branching time model checking, sequential equivalence checking, and combinational verification. In this paper, we present a new model checking algorithm based on language emptiness checking using MDGs. The proposed procedure makes use of the Wring tool from UC Berkeley to generate the property automaton. Language emptiness is checked on the product of this latter and the design automaton represented in terms of MDGs. Compared with the existing MDG model checking, our algorithm shows superior performance. We also conducted experimental comparison between our tool, VIS from UC Berkeley and Cadence FormalCheck.

In this paper, we present a formal hardware verification framework linking ASM with MDG. ASM (Abstract State Machine) is a state based language for describing transition systems. MDG (Multiway Decision Graphs) provides symbolic representation of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications, then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We support this work with a case study of an Island Tunnel Controller, which behavior and structure were specified in ASM then using our ASM-MDG tool successfully verified within the MDG tool.

In this paper we describe a methodology for the formal verification of a DSP chip using the HOL theorem prover. We used an iterative method to specify both the behavioral and structural descriptions of the processor. Our methodology consists of first simplifying the representations of the DSP units. We then prove for each unit that its hardware description implies its behavioral specification. Using the simplified (abstracted) description of the units we have been able to greatly reduce the cost of deducing the behavior of the processor instruction set from the hardware implementation of the processor units. The proposed methodology creates a new representation of the processor at each iteration such that its complexity can be handled by the theorem prover. This allowed us to make a proof of the full instruction set of this processor.

Modeling the environment of a design module under verification is a known practical problem in compositional verification. In this paper, we propose an approach to translate an ACTL specification into such an environment. Throughout the translation, we construct an efficient tableau for the full range of ACTL and synthesize the tableau into Verilog HDL behavior level program. The synthesized program can be used to check the properties that the system's components must guarantee. We have used the proposed environment synthesis in the compositional verification of an ATM switch fabric from Nortel Networks. Experiments show that given the theoretical compositional verification intractable limit, we can still manage to verify industry size designs.

In this paper we present practical approaches to formally verify the RTL implementation of a Telecom megacell using model checking techniques based on the FormalCheck tool. We adopted a hierarchical verification method, which relies on the built-in hierarchy of the design as the mechanism to conquer its verification complexity. We then applied a number of tool guided abstraction and reduction techniques within FormalCheck to avoid state space explosion. The case study we considered is the Transmit Master/ Receive Slave (TMRS) Telecom megacell from PMC-Sierra, Inc., implementing a SCI-PHY (Saturn Compatible Interface for ATMPHY devices) protocol. Using our approaches, we succeeded the model checking of the TMRS design and were able to uncover a number of flaws in the RTL design as well as in the documentation specification.

The performance of multistage interference cancellation (MIC) and three combining techniques, i.e., multipath decorrelating (MIC-DECO), optimum combining (MIC-OPTM), and RAKE combining (MIC-RAKE) for asynchronous quadrature phase-shift keying/direct-sequence code-division multiple access over frequency-selective multipath Rayleigh fading channels is studied. The analytical bit-error probabilities of the MIC-DECO and MIC-OPTM are derived and shown to be in a good agreement with simulation results. Both analytical and simulation results show that the MIC-DECO, MIC-OPTM, and MIC-RAKE in a multiuser environment provide a good performance close to the ideal performance in a single-user system even in the presence of channel estimation error.

In order to overcome the limitations of automated tools and the cumbersome proof process of interactive theorem proving, we adopt a hybrid approach for formal hardware verification which uses the strengths of theorem proving (HOL) with powerful mathematical tools such as induction and abstraction, and the advantages of automated tools (MDG) which support equivalence checking and model checking. The MDG system is a decision diagram based verification tool, primarily designed for hardware verification. HOL is a theorem prover built on higher-order logic.

In this paper, a multilevel-quantized soft-limiting (SL-MQ) detector for frequency hopping spread spectrum multiple access (FH-SSMA) systems is proposed and analyzed. Numerical and simulation results in frequency selective Rayleigh fading channels show that compared to the hard-limiting (HL) detector, the new SL-MQ with M=4 can improve the system capacity by almost 10% at the bit error rate level of 10/sup -3/. Furthermore, the performance of the SL-MQ has low sensitivity to the optimum value of the amplitude threshold so that it can tolerate an inaccurate estimate of the optimum in practice.

Nowadays, there exist a wide variety of verification tools. Some, like the SPIN model checker, are designed and mainly used for the verification of interleaving software systems, such as communication protocols. Others, like VIS (Verification Interacting with Synthesis), are designed and used for synchronous hardware systems verification. In this paper, we compare and contrast SPIN and VIS. In particular, we devote a special attention to the efficiency of these tools for the verification of communications protocols that can be implemented either in software or hardware. As a basis of our comparison, we formally describe and verify the ATMR (Asynchronous Transfer Mode Ring) medium access protocol using SPIN, and its hardware implementation using VIS. We believe that this study is of particular interest, as more and more protocols, like the ATM protocol stack, are being implemented in hardware in order to match high speed requirements. However, this is not a formal comparison of SPIN and VIS.

With the increasing emergence of mixed hardware/software systems, it is important to ensure the correctness of such a system formally, particularly for real-time and safety critical applications. We present a hierarchical approach to modeling and formally verifying an embedded system at higher levels of abstraction, using Multiway Decision Graphs (MDGs). We demonstrate our approach on the embedded software for a mouse controller application on a commercial microcontroller (PIG 16C71), using the MDG verification tools. Inconsistencies in the assembly code with respect to the specification, as published in the application notes of the manufacturer, were uncovered through our experiments.

A multistage interference cancellation (MIC) technique with RAKE diversity (MIC-RAKE) for QPSK asynchronous direct sequence code division multiple access (DS/CDMA) system over frequency selective multipath Rayleigh fading channels is presented. Unlike the conventional MIC, which tries to subtract the lump sum of the multiple access interference (MAI) and the self-interference (SI), the MIC-RAKE attempts to cancel the MAI and the partial SI, and to treat the residual SI as useful signal for symbol decision. The RAKE combining is employed to collect signal replicas over multiple fading paths. The upper and lower bounds on the bit error probability are derived by using a Gaussian approximation. Furthermore, the effect of the channel estimation error is studied. Analysis and simulation show that the MIC-RAKE can provide a performance close to the ideal performance of single-user system, and outperforms the conventional MIC even in the presence of channel estimation error.

An adaptive multistage parallel interference cancellation technique based on the partial interference cancellation (IC) approach of Divsalar and Simon (see Tech. Rep. 95-21, JPL Publication, 1995) was proposed by Xue, Weng, Le-Ngoc and Tahar (see Proc. of VTC'SS, Vancouver, Canada, 1999) for multipath fading channels. In this paper, the proposed technique is applied to develop a receiver structure in an AWGN environment. Unlike the scheme of Divsalar et al., the weighting factors in this proposed scheme are derived by minimizing the mean-square error between the received signal and its estimate through an LMS algorithm. Neither training sequence nor pilot signal is needed. The complexity of the proposed adaptive multistage PIC structure is much lower than that of linear multiuser detectors. Simulation results show the superior performance of the proposed receiver structure over an AWGN channel and in various conditions.

This paper introduces a multistage interference cancellation (MIC) technique with diversity reception for quadrature phase shift keying (QPSK) asynchronous direct-sequence code division multiple access (DS/CDMA) systems over frequency-selective multipath Rayleigh fading channels. Unlike the previous MIC, which tries to remove the lump sum of the multiple-access interference (MAI) and self-interference (SI), this introduced MIC attempts to cancel only the MAI and part of the SI due to the intersymbol interference, while treating the remaining SI created by the current symbol as useful information for symbol decision. In this technique, the RAKE combining is used to collect signal replicas over multiple fading paths. Upper and lower bounds on the bit error probability are derived using a Gaussian approximation and the characteristic function method. Furthermore, effects of channel estimation error on the performance are studied. Analytical and simulation results show that the introduced MIC can provide a performance extremely close to that in an ideal single-user environment and outperforms the previous MIC even in the presence of channel estimation error.

Although the multistage interference cancellation detector is simple in structure, its performance degrades when the number of active users becomes large. In some cases, the performance is even worse than that without cancellation, due to the lack of the exact knowledge of the interfering signal in cancellation. Partial interference cancellation suggested by Divsalar and Simon (see IEEE Trans. Commun., vol.46, p.258-68, 1998) tries to remedy this weakness by reducing the cost of a wrong interference estimation through a weight in each stage. This paper presents an adaptive multistage structure based on the partial interference cancellation approach. In this structure, the weights are obtained by minimizing the mean-square error between the received signal and its estimate through a least mean square (LMS) algorithm. The resulting weights contain reliability information for the hard decisions made in the previous stage. Neither a training sequence nor a pilot signal is needed in the proposed scheme, and its complexity is much lower than that of linear multiuser detectors. Simulation results show that the proposed scheme can outperform some of the existing interference cancellation methods in both the additive white Gaussian noise (AWGN) and the multipath fading channels.

In this paper, we present several techniques for modeling and formal verification of the Fairisle asynchronous transfer mode (ATM) switch fabric using multiway decision graphs (MDGs). MDGs represent a new class of decision graphs which subsumes Bryant's reduced ordered binary decision diagrams (ROBDDs) while accommodating abstract sorts and uninterpreted function symbols. The ATM device we investigated is in use for real applications in the Cambridge University Fairisle network. We modeled and verified the switch fabric at three levels of abstraction: behavior, and register transfer level (RTL) and gate levels. In a first stage, we validated the high-level specification by checking specific safety properties that reflect the behavior of the fabric in its real operating environment. Using the intermediate abstract RTL model, we hierarchically completed the verification of the original gate-level implementation of the switch fabric against the behavioral specification. Since MDGs avoid model explosion induced by data values, this work demonstrates the effectiveness of MDG based verification as an extension of ROBDD-based approaches. All the verifications were carried out automatically in a reasonable amount of CPU time.

In this paper we present several practical methods for formally verifying an Asynchronous Transfer Mode (ATM) network switching fabric using the Verification Interacting with Synthesis (VIS) tool. We produced Verilog RTL behavioral and netlist structural descriptions of the switch fabric at different levels of hierarchy and established several abstracted models of the fabric. Using various techniques presented in the paper, we provided a number of relevant liveness and safety properties expressible in CTL, and accomplished their verification in reasonable CPU time. Moreover, we performed equivalence checking between the structural and behavioral descriptions of each submodule of the implementation hierarchy.

In this paper we present our experience on model checking of an Asynchronous Transfer Mode (ATM) switch using the Verification Interacting with Synthesis (VIS) tool. The switch we considered is in use for real applications in the Cambridge Fairisle network. It is composed of four input/output port controllers and a switch fabric, and contains around 1 MB memory, 2 KB FIFO buffer and 800 registers (latches). To overcome state space explosion, we adopted several abstraction and reduction techniques to reduce the model, and applied compositional reasoning combined with a novel property division approach. Using the above techniques, we succeeded in verifying the entire switch at different hierarchy levels within reasonable CPU time.

In this paper we present our results on formally verifying the implementation of an asynchronous transfer mode (ATM) network switching fabric using a new class of decision graphs, called Multiway Decision Graphs (MDG). The design we consider is in use for real applications in the Cambridge Fairisle network. We produced the description of the hardware implementation at different levels of abstraction. We then performed the verification of an abstract description model against the description of the gate-level implementation. Using this abstract model, we accomplished the verification of specific properties that reflect the behavior of the Fairisle ATM switch fabric.

We investigate equivalence checking of the RTL hardware implementation of the Cambridge Fairisle Asynchronous Transfer Mode (ATM) 4 by 4 switch fabric against a high-level behavioral specification which has unrestricted frame size, cell length and word width. The verification is based on the reachability analysis of the product machine of the implementation and the specification, both modeled as Abstract State Machines (ASM). Multiway Decision Graphs (MDG) are used to encode both the output and transition relations of the ASMs and of the set of reachable abstract states, allowing implicit abstract state enumeration. Since MDGs avoid model explosion induced by data values, this experiment demonstrates the effectiveness of MDG-based verification as an extension of ROBDD-based approaches.

We outline a general methodology for the formal verification of instruction pipelines in RISC cores. The different kinds of conflicts, i.e. resource, data and control conflicts that can occur due to the simultaneous execution of the instructions in the pipeline, have been formally specified in higher order logic. Based on a hierarchical model for RISC processors, we have developed a constructive proof methodology, i.e. when conflicts at a specific abstraction level are detected, the conditions under which these occur are generated and explicitly output to the designer, thus easing their removal. All implemented specifications and tactics are kept general, so that they are usable for a wide range of RISC cores. In this paper, the described formalization and proof strategies are illustrated via the DLX RISC processor.

A general methodology, based on a hierarchical model of interpreters, is presented for formally verifying RISC cores. The abstraction levels used by a designer in the implementation of RISC cores, namely the instruction set level, the pipeline stage level, the phase level and the hardware implementation, are mirrored by this hierarchical model. The use of this model allows us to successively prove the correctness between two neighboring levels of abstractions, so that the verification process is simplified. The parallelism in the execution of the instructions, resulting from the pipelined architecture of RISCs is handled by splitting the proof into simplified steps. The first step shows that, under certain assumptions, no conflicts can occur between simultaneously executed instructions, and the second step shows that each instruction is implemented correctly by the sequential execution of its pipeline steps.>