We present SuperSAGA, an agentic semi-automated formal verification framework that assists in generating, debugging, and refining SystemVerilog Assertions (SVA) from natural language specifications. Rather than relying on full manual workflows, SuperSAGA combines Large Language Models (LLMs) with Retrieval-Augmented Generation (RAG) to guide assertion development based on human-reviewed verification plans using an agentic workflow. The framework translates specifications into syntactically correct assertions, integrates feedback from formal verification tools, and supports iterative refinement using an orchestration of supervisor and subordinate agents. Evaluation on OpenTitan IP modules shows improved quantitative coverage over state of the art and reduced manual effort, demonstrating the potential of guided automation in simplifying the assertion generation process for hardware designers.

In the context of modern day embedded safety-critical systems and low-resource edge devices in particular, Sigma-Delta Neural Networks (SDNNs) offer a promising alternative to traditional Artificial Neural Networks (ANNs) by leveraging event-driven, sparse computations inspired by biological neural processing. This energy-efficient paradigm makes SDNNs well-suited for neuromorphic hardware and real-time applications, particularly in scenarios with temporal redundancy, such as video processing. However, as neural networks become integral to safety-critical systems, ensuring their robustness against adversarial perturbations is an absolute necessity. In this work, we propose an end-to-end framework for formal modeling and verification of SDNNs using Satisfiability Modulo Theory (SMT). Unlike empirical robustness evaluations, SMT-based verification provides formal guarantees by encoding SDNN behavior and adversarial robustness properties as mathematical constraints. We introduce an SMT-based formulation for encoding SDNNs with SMT constraints and define a robustness property motivated by video stream processing. Our approach systematically examines how well SDNNs can handle adversarial attacks, ensuring they work correctly in safety-critical applications. We validate our framework through experiments on temporal version of the MNIST dataset. To the best of our knowledge, this is the first formal verification framework for SDNNs, bridging the gap between neuromorphic computing and rigorous verification.

In this paper, we address the problem of safety verification for Spiking Neural Networks (SNNs) with Spiking Rectified Linear Activation (SRLA). The SNNs are obtained by first training Artificial Neural Networks (ANNs) and then translating to SNN with subsequent hyperparameter tuning. We propose a solution which tunes the temporal window hyperparameter of the translated SNN to ensure both accuracy and compliance with the safe range specification that requires the SNN outputs to remain within a safe range. We demonstrate our approach with experiments on 5 benchmark neural controllers.

In Multi-Access Edge Computing (MEC), a number of mechanisms exist to determine the optimal placement of monolithic service workflows. For applications designed as microservice workflow architectures, service placement schemes need to be revisited owing to the inherent interdependencies which exist between microservices. The dynamic environment, with stochastic user movement and service invocations, along with a large placement configuration space makes microservice placement in MEC a challenging task. Additionally, owing to user mobility, a placement scheme may need to be recalibrated, triggering service migrations to maintain the advantages offered by MEC. Existing microservice placement and migration schemes consider on-demand strategies. In this work, we take a different route and propose a Reinforcement Learning (RL) based proactive mechanism using a Learning Automata (LA) for microservice placement and migration that on one hand, keeps track of user mobility and resorts to migration when necessary, while on the other hand, keeps track of server residual capacities so that no server is overloaded. We use the San Francisco Taxi dataset to validate our approach. Experimental results show the effectiveness of our approach in comparison to other methods.

In recent times, Bounded Model Checking (BMC) engines have gained wide prominence in formal verification. Different BMC engines exist, differing in their optimization, representations and solving mechanisms used to represent and navigate the underlying state transition of the given design to be verified. The objective of this article is to examine if combinations of BMC engines can help to combine their strengths. We propose an approach that can create a sequencing of BMC engines that can reach better depth in formal verification, as opposed to executing them alone for a specified time. Our approach uses machine learning, specifically, the Multi-Armed Bandit paradigm of reinforcement learning, to predict the best-performing BMC engine for a given unrolling depth of the underlying circuit design. We evaluate our approach on a set of benchmark designs from the Hardware Model Checking Competition (HWMCC) benchmarks and show that it outperforms the state-of-the-art BMC engines in terms of the depth reached or time taken to deduce a property violation. The synthesized BMC engine sequences reach better depths than HWMCC results and the state-of-the-art technique, super_deep, for more than 80% of the cases. It also outperforms single engine runs for more than 92% of the cases where a property violation is not found within a given time duration. For designs where property violations are found within the given time duration, the synthesized sequences found the property violation in a lesser time than HWMCC for all the designs and outperformed both super_deep and single engine runs for more than 87% of the designs.

Sampling over combinatorial spaces is a fundamental problem in artificial intelligence with a wide variety of applications. Since state-of-the-art techniques heavily rely on heuristics whose rigorous analysis remains beyond the reach of current theoretical tools, the past few years have witnessed interest in the design of techniques to test the quality of samplers. The current state-of-the-art techniques, $\mathsf{Barbarik}$ and $\mathsf{Barbarik2}$, focuses on the cases where combinatorial spaces are encoded as Conjunctive Normal Form (CNF) formulas. While CNF is a general-purpose form, often techniques rely on exploiting specific representations to achieve speedup. Of particular interest are Horn clauses, which form the basis of the logic programming tools in AI. In this context, a natural question is whether it is possible to design a tester that can determine the correctness of a given Horn sampler. The primary contribution of this paper is an affirmative answer to the above question. We design the first tester, $\mathsf{Flash}$, which tests the correctness of a given Horn sampler: given a specific distribution $\mathcal{I}$ and parameters $\eta$, $\varepsilon$, and $\delta$, the tester $\mathsf{Flash}$ correctly (with probability at least $ 1-\delta$) distinguishes whether the underlying distribution of the Horn-sampler is “$\varepsilon$-close” to $\mathcal{I}$ or “$\eta$-far” from $\mathcal{I}$ by sampling only $\widetilde{\mathcal{O}}(\mathsf{tilt}^3/(\eta - \varepsilon)^4)$ samples from the Horn-sampler, where the $\mathsf{tilt}$ is the ratio of the maximum and the minimum (non-zero) probability masses of $\mathcal{I}$. We also provide a prototype implementation of $\mathsf{Flash}$ and test three state-of-the-art samplers on a set of benchmarks.

The advent of Multi-Access Edge Computing (MEC) has enabled service providers to mitigate high network latencies often encountered in accessing cloud services by deploying containerized application instances on edge servers situated near end users. MEC servers are, however, susceptible to various types of failures such as communication link failures, hardware failures and so on. A fault recovery strategy determines which MEC servers to utilize to re-deploy application containers in the event of a failure. In this work, we propose a two-fold fault recovery strategy characterized by application priority. We propose a Formal Methods driven local recovery strategy for high-priority applications. We use Stochastic Multi-Player Games as a Formal Model to characterize the interactions between the different components in an MEC environment. We use objectives specified in Probabilistic Alternating-Time Temporal Logic with a Probabilistic Model Checker to derive recovery strategies considering all possible execution scenarios of the model. For lower priority applications, we resort to a global recovery strategy by designing a greedy heuristic considering each server’s failure probability. We use benchmark datasets to validate our approach. Experimental results show an average 14% reduction in latency with our approach in comparison with other state-of-the-art methods.

In artificial intelligence planning, having an explanation of a plan given by a planner is often desirable. The ability to explain various aspects of a synthesized plan to an end user not only brings in trust on the planner but also reveals insights of the planning domain and the planning process. Contrastive questions such as “Why action A instead of action B?” can be answered with a contrastive explanation that compares properties of the original plan containing A against the contrastive plan containing B. In this article, we explore a set of contrastive questions that a user of a planning tool may raise and propose a re-model and re-plan framework to provide explanations to such questions. Earlier work has reported this framework on planning instances for discrete problem domains described in the Planning Domain Definition Language (PDDL) and its variants. In this article, we propose an extension for planning instances described by PDDL+ for hybrid systems that portray a mix of discrete-continuous dynamics. Specifically, given a mixed discrete-continuous system model in PDDL+ and a plan describing the set of desirable actions on the same to achieve a destined goal, we present a framework that can integrate contrastive questions in PDDL+ and synthesize alternate plans. We present a detailed case study on our approach and propose a comparison metric to compare the original plan with the alternate ones.

With the rapid proliferation of strategic alliances between service providers, enterprises cooperate towards service quality improvement and provide lower cost service bundles. This article presents a novel solution to the minimum cost service bundle selection problem for workflows in the presence of singleton subscription costs and service bundle offerings and compatibility requirements. Given a workflow specifying a set of tasks and a set of candidate services for each task, with a set of compatibility constraints between services, the selection problem has the objective of selecting the most suitable service offering(s) for each task. In this article, we analyze the selection problem in the presence of service bundle offerings. We present a novel multi-partite hyper-graph visualization of the selection problem and analyze its hardness. Additionally we present a novel combination of ILP and abstraction refinement as a potential solution, that is shown to expedite a naïve ILP based solution. We present experiments to substantiate this claim.

In recent times, the need for low latency has made it necessary to deploy application services physically and logically close to the users rather than using the cloud for hosting services. This paradigm of computing, known as edge or fog computing, is becoming increasingly popular. An edge user allocation policy determines how to allocate service requests from mobile users to MEC servers. Current state-of-the-art techniques assume that the total resource utilization on an edge server is equal to the sum of the individual resource utilizations of services provisioned from the edge server. However, the relationship between resources utilized on an edge server with the number of service requests served from there is usually highly non-linear, hence, mathematically modelling the resource utilization is challenging. This is especially true in case of an environment with CPU-GPU co-execution, as commonly observed in modern edge computing. In this work, we provide an on-device Deep Reinforcement Learning (DRL) framework to predict the resource utilization of incoming service requests from users, thereby estimating the number of users an edge server can accommodate for a given latency threshold. We further propose an algorithm to obtain the user allocation policy. We compare the performance of the proposed DRL framework with traditional allocation approaches and show that the DRL framework outperforms deterministic approaches by at least 10% in terms of the number of users allocated.

Multi-Access Edge Computing (MEC) has emerged as a promising new paradigm allowing low latency access to services deployed on edge servers to avert network latencies often encountered in accessing cloud services. A key component of the MEC environment is an auto-scaling policy which is used to decide the overall management and scaling of container instances corresponding to individual services deployed on MEC servers to cater to traffic fluctuations. In this work, we propose a Safe Reinforcement Learning (RL)-based auto-scaling policy agent that can efficiently adapt to traffic variations to ensure adherence to service specific latency requirements. We model the MEC environment using a Markov Decision Process (MDP). We demonstrate how latency requirements can be formally expressed in Linear Temporal Logic (LTL). The LTL specification acts as a guide to the policy agent to automatically learn auto-scaling decisions that maximize the probability of satisfying the LTL formula. We introduce a quantitative reward mechanism based on the LTL formula to tailor service specific latency requirements. We prove that our reward mechanism ensures convergence of standard Safe-RL approaches. We present experimental results in practical scenarios on a test-bed setup with real-world benchmark applications to show the effectiveness of our approach in comparison to other state-of-the-art methods in literature. Furthermore, we perform extensive simulated experiments to demonstrate the effectiveness of our approach in large scale scenarios.

In recent times, Multi-Access Edge Computing (MEC) has emerged as a new paradigm allowing low-latency access to services deployed on edge nodes offering computation, storage and communication facilities. Vendors deploy their services on MEC servers to improve performance and mitigate network latencies often encountered in accessing cloud services. An allocation policy determines how to allocate service requests from users to MEC servers. A number of proposals for binding user service requests to nearby edge servers enroute have been proposed in literature. However, none of these proposals, to the best of our knowledge, provide quantitative guarantees on performance metrics. Indeed, the evolving environment, along with a large allocation configuration space makes proving performance guarantees for such allocation policies a challenging task. Further, the implications of MEC server failures on allocation policies have been relatively unexplored. To address such issues, we propose a trace driven approach to derive a formal model of allocation policies and perform quantitative verification to produce probabilistic guarantees on performance metrics. We use the San Francisco taxi dataset, the LDNS availability dataset and allocation policies from recent literature to validate our approach. Experimental results demonstrate how our model can be utilized to quantitatively compare performance metrics of service allocation policies in MEC systems.

Digital Microfluidics is an emerging technology for automating laboratory procedures in biochemistry. With more and more complex biochemical protocols getting mapped to biochip devices and microfluidics receiving a wide adoption, it is becoming indispensable to develop automated tools and synthesis platforms that can enable a smooth transformation from complex cumbersome benchtop laboratory procedures to biochip execution. Given an informal/semi-formal assay description and a target microfluidic grid architecture on which the assay has to be implemented, a synthesis tool typically translates the high-level assay operations to low-level actuation sequences that can drive the assay realization on the grid. With more and more complex biochemical assay protocols being taken up for synthesis and biochips supporting a wider variety of operations (e.g., MicroElectrode Dot Arrays (MEDAs)), the task of assay synthesis is getting intricately complex. Errors in the synthesized assay descriptions may have undesirable consequences in assay operations, leading to unacceptable outcomes after execution on the biochips. In this work, we focus on the challenge of examining the correctness of synthesized protocol descriptions, before they are taken up for realization on a microfluidic biochip. In particular, we take up a protocol description synthesized for a MEDA biochip and adopt a formal analysis method to derive correctness proofs or a violation thereof, pointing to the exact operation in the erroneous translation. We present experimental results on a few bioassay protocols and show the utility of our framework for verifiable protocol synthesis.

In recent times, Mobile Edge Computing (MEC) has emerged as a new paradigm allowing low-latency access to services deployed on edge nodes offering computation, storage and communication facilities. Vendors deploy their services on MEC servers to improve performance and mitigate network latencies often encountered in accessing cloud services. An allocation policy determines how to allocate service requests from mobile users to MEC servers. A number of proposals for binding user service requests to nearby edge servers enroute have been proposed in literature. However, none of these proposals, to the best of our knowledge, provide quantitative performance guarantees on the quality of service metrics. Indeed, the evolving environment, along with a large allocation configuration space makes proving performance guarantees for such allocation policies a challenging task. To address such issues, we propose a trace driven approach to derive a formal model of allocation policies and perform quantitative verification to produce probabilistic guarantees on performance metrics. We use benchmark real world MEC server and user datasets and a mobility aware allocation and migration policy from recent literature to validate our model. Experimental results show our model's effectiveness in quantitatively reasoning about service allocation performance metrics in MEC systems.

In recent times, Mobile Edge Computing (MEC) has emerged as a new paradigm allowing low-latency access to services deployed on edge nodes offering computation, storage and communication facilities. Vendors deploy their services on MEC servers to improve performance and mitigate network latencies often encountered in accessing cloud services. A service placement policy determines which services are deployed on which MEC servers. A number of mechanisms exist in literature to determine the optimal placement of services considering different performance metrics. However, for applications designed as microservice workflow architectures, service placement schemes need to be re-examined through a different lens owing to the inherent interdependencies which exist between microservices. Indeed, the dynamic environment, with stochastic user movement and service invocations, along with a large placement configuration space makes microservice placement in MEC a challenging task. Additionally, owing to user mobility, a placement scheme may need to be recalibrated, triggering service migrations to maintain the advantages offered by MEC. Existing microservice placement and migration schemes consider on-demand strategies. In this work, we take a different route and propose a Reinforcement Learning based proactive mechanism for microservice placement and migration. We use the San Francisco Taxi dataset to validate our approach. Experimental results show the effectiveness of our approach in comparison to other state-of-the-art methods.

In artificial intelligence planning, having an explanation of a plan given by a planner is often desirable. The ability to explain various aspects of a synthesized plan to an end-user not only brings in trust on the planner but also reveals insights of the planning domain and the planning process. Contrastive questions such as "Why action A instead of action B?" can be answered with a contrastive explanation that compares properties of the original plan containing A against the contrastive plan containing B. In this paper, we explore a set of contrastive questions that a user of a planning tool may raise and we propose a re-model and re-plan framework to provide explanations to such questions. Earlier work has reported this framework on planning instances for discrete problem domains described in the Planning Domain Definition Language (PDDL) and its variants. In this paper, we propose an extension for planning instances described by PDDL+ for hybrid systems which portray a mix of discrete-continuous dynamics. Specifically, given a mixed discrete continuous system model in PDDL+ and a plan describing the set of desirable actions on the same to achieve a destined goal, we present a framework that can integrate contrastive questions in PDDL+ and synthesize alternate plans. We present a detailed case study on our approach and propose a comparison metric to compare the original plan with the alternate ones.

In this article, we consider the problem of droplet routing for Microelectrode-Dot-Array (MEDA) biochips. MEDA biochips today provide a host of useful features for droplet movement by making it possible to manoeuvre droplets at a much finer granularity and with significantly increased flexibility. More precisely, MEDA biochips support more degrees of freedom in navigation and volumetric manipulation such as diagonal movement, droplet reshaping, and fractional-level split-and-merge. This helps improve routing of droplets on microfluidic grids—in particular, when the space available on the grid is limited or blocked by obstacles. In this work, we discuss how these improved capabilities can be utilized in the realization of the desired routes on those biochips. To this end, we introduce a routing method that utilizes satisfiability solvers and guarantees the generation of optimal solutions, considering the set of MEDA operations we model. This significantly improves the state of the art, since previously proposed solutions either (1) relied on heuristics and, hence, were not able to guarantee the optimum or (2) only considered a subset of the MEDA features. The solution proposed in this work includes a formulation of all MEDA features, which, as illustrated by examples, allows for the determination of routing solutions with smaller completion times. Experimental evaluations confirm these findings.

Efficient service composition in real time, while satisfying desirable Quality of Service (QoS) guarantees for the composite solution has been one of the topmost research challenges in the domain of services computing. On one hand, optimal QoS aware service composition algorithms, that come with the promise of solution optimality, are inherently compute intensive, and therefore, often fail to generate the optimal solution in real time for large scale web services. On the other hand, heuristic solutions that have the ability to generate solutions fast and handle large and complex service spaces, settle for sub-optimal solution quality. The problem of balancing the trade-off between computation efficiency and optimality in service composition has alluded researchers since quite some time, and several proposals for taming the scale and complexity of web service composition have been proposed in literature. In this paper, we present a new perspective towards this trade-off in service composition based on abstraction refinement, which can be seamlessly integrated on top of any off-the-shelf service composition method to tackle the space complexity, thereby, making it more time and space efficient. Instead of considering services individually during composition, we propose a set of abstractions and corresponding refinements to form service groups based on functional characteristics. The composition and QoS satisfying solution construction steps are carried out in the abstract service space. Our abstraction refinement methods give a significant speed-up compared to traditional composition techniques, since we end up exploring a substantially smaller space on average. Experimental results on benchmarks show the efficiency of our proposed mechanism in terms of time and the number of services considered for building the QoS satisfying composite solution.

Automatic web service composition has received a significant research attention in service-oriented computing over decades of research. With increasing number of web services, providing an end-to-end Quality of Service (QoS) guarantee in responding to user queries is becoming an important concern. Multiple QoS parameters (e.g., response time, latency, throughput, reliability, availability, success rate) are associated with a service, thereby, service composition with a large number of candidate services is a challenging multi-objective optimization problem. In this article, we study the multi-constrained multi-objective QoS-aware web service composition problem and propose three different approaches to solve the same, one optimal, based on Pareto front construction, and two others based on heuristically traversing the solution space. We compare the performance of the heuristics against the optimal and show the effectiveness of our proposals over other classical approaches for the same problem setting, with experiments on WSC-2009 and ICEBE-2005 datasets.

With increasing use of runtime polymorphism and reliance on runtime type interpretation, the presence and importance of indirect branches has seen a considerable rise in recent workloads. Evidently, accurate target prediction for indirect branches has emerged as an important problem. While direction prediction of direct branches has received considerable research attention leading to efficient prediction policies and hardware structures implemented inside modern processors, proposals for target prediction for indirect branches has been relatively few. The problem of accurate target prediction for indirect branches is significantly tough since these transfer control to an address stored in a register that is known only at runtime. Unlike conditional direct branches, indirect branches can have more than two targets to be resolved at runtime, for which prediction requires a full 32-bit/64-bit address to be predicted, in contrast to just a taken or not-taken decision as needed for direction prediction of direct branches. Recent research shows indirect branches, being mispredicted more frequently, can start to dominate the overall branch misprediction cost. In modern processors, the only hardware structure available to facilitate target address prediction for indirect branches is a fixed-size Branch Target Buffer (BTB). BTB is often designed as a set associative cache for storing recent target addresses for branch instructions encountered during execution, with a motivation of being able to reuse the same addresses for future instances, thereby saving latency cycles. Evidently, designing efficient indexing schemes and replacement mechanisms for BTB structures is crucial, more so, for indirect branches, since these serve as the only prediction handle. In this paper, our objective is to examine a hierarchical BTB design for multicores with total size comparable to what exists today, with a motivation towards possible improvement of prediction accuracy by facilitating collaborative constructive learning between programs executing in different cores that encounter similar histories. Specifically, we wish to propose the concept of a small on-chip L1 BTB inside each core, supported by a larger off-chip L2 BTB shared among the cores. Our motivation towards a hierarchical BTB design is twofold. On one hand, in a multiprogramming environment, where the same program is executed in multiple cores, on different test cases, there is a significant potential of target information reuse for indirect branches, as is evident from our experiments on SPEC 2006 workloads. This is typically useful for machine learning based workloads where the training phase is often executed in different cores with the same neural network being trained on different training sets. On the other hand, with different programs in different cores, there is some chance of reuse as well, due to sharing of system libraries. The essence of our idea rests on the fact that programs executed in different cores have similar history patterns that can similarly influence the target addresses. Our design aims to decrease on the on-chip L1 BTB size while investing more storage for the off-chip shared L2 BTB. Suitable allocation and replacement policies support our hierarchical design. Initial experiments show expected accuracy benefits.

Medical cyber-physical systems in which multiple medical devices co-ordinate with each other and provide closed-loop control to the patient, have come into prominence in the recent past. One of the main challenges for such systems is guaranteeing their safety even in the presence of significant physiological variabilities among patients. Formal verification based on well-established models of patient physiology has emerged as a potential solution to this problem. However, such techniques face a significant hurdle in terms of scalability due to two main reasons; non-linearity in the physiological models, and large variations in the model parameters due to intra and inter-patient variabilities. In this work, we considered a case-study system of pre-operative and intra-operative care for diabetic patients based on a well-established insulin-infusion protocol. The system comprises a physiological model of the glucose-insulin regulatory system based on Dallaman's model integrated with a proportional-derivative controller that encodes the insulin-infusion protocol. Towards addressing the verification scalability problem, we present a solution for this case-study based on well-known model linearization techniques. We also calculated the error in linearization and incorporated the error into the linearized model. We have constructed both hybrid system model and the corresponding linearized model along with the error and have verified them using dReach and SAL verification tools, respectively. The non-linear model remained non-verifiable for a depth of 8 even after running the verification for more than 20 hours. However, the linearized model was found to be fully verifiable for all the cases and also 2x times faster than the non-linear model for a depth of 7. Therefore, safety of the nonlinear model can be verified with some approximation using the corresponding linearized model.

In multicore and multicached architectures, cache coherence is ensured with a coherence protocol. However, the performance benefits of caching diminishes due to the cost associated with the protocol implementation. In this paper, we propose a novel technique to improve the performance of multithreaded programs running on shared-memory multicore processors by embracing approximate computing. Our idea is to relax the coherence requirement selectively in order to reduce the cost associated with a cache-coherence protocol, and at the same time, ensure a bounded QoS degradation with probabilistic reliability. In particular, we detect instructions in a multithreaded program that write to shared data, we call them Shared-Write-Access-Points (SWAPs), and propose an automated statistical analysis to identify those which can tolerate coherence faults. We call such SWAPs approximable. Our experiments on 9 applications from the SPLASH 3.0 benchmarks suite reveal that an average of 57% of the tested SWAPs are approximable. To leverage this observation, we propose an adapted cache-coherence protocol that relaxes the coherence requirement on stores from approximable SWAPs. Additionally, our protocol uses stale values for load misses due to coherence, the stale value being the version at the time of invalidation. We observe an average of 15% reduction in CPU cycles and 11% reduction in energy footprint from architectural simulation of the 9 applications using our approximate execution scheme.

Digital microfluidic biochips (DMFBs) are now being extensively used to automate several biochemical laboratory protocols such as clinical analysis, point-of-care diagnostics, or DNA sequencing. In many biological assays, e.g., bacterial susceptibility tests and cellular response analysis, samples, or reagents are required in multiple concentration (or dilution) factors, satisfying certain gradient patterns such as linear, exponential, or parabolic. Dilution gradients are traditionally prepared using continuous-flow microfluidic devices. Unfortunately, most of them suffer from inflexibility and nonprogrammability, and they require large volumes of costly stock-solutions. DMFBs, on the other hand, are shown to produce, more efficiently, samples with multiple dilution factors. However, none of the existing DMFB-based algorithms utilize the properties of the gradient-profile while optimizing reactant-cost and sample-preparation time. In this paper, we explore the underlying combinatorial attributes of different gradients and harnessed them for efficient production of the desired concentration profile. For linear gradients, we present theoretical results concerning the number of mix-split operations and waste production, and prove an upper bound on on-chip storage requirement. A cost-effective method for generating a wide class of exponential gradients is also proposed. Finally, in order to handle a complex-shaped gradient, we posit a digital-geometric technique to approximate it with a sequence of linear gradients. Experimental results on various gradient-profiles are presented in support of the proposed method.

Speculative execution is an optimization technique used in modern processors by which predicted instructions are executed in advance with an objective of overlapping the latencies of slow operations. Branch prediction and load value speculation are examples of speculative execution used in modern pipelined processors to avoid execution stalls. However, speculative executions incur a performance penalty as an execution rollback when there is a misprediction. In this work, we propose to aid speculative execution with approximate computing by relaxing the execution rollback penalty associated with a misprediction. We propose a sensitivity analysis method for data and branches in a program to identify the data load and branch instructions that can be executed without any rollback in the pipeline and yet can ensure a certain user-specified quality of service of the application with a probabilistic reliability. Our analysis is based on statistical methods, particularly hypothesis testing and Bayesian analysis. We perform an architectural simulation of our proposed approximate execution and report the benefits in terms of CPU cycles and energy utilization on selected applications from the AxBench, ACCEPT, and Parsec 3.0 benchmarks suite.

In the area of biomedical engineering, digital-microfluidic biochips (DMFBs) have received considerable attention because of their capability of providing an efficient and reliable platform for conducting point-of-care clinical diagnostics. System reliability, in turn, mandates error-recoverability while implementing biochemical assays on-chip for medical applications. Unfortunately, the technology of DMFBs is not yet fully equipped to handle error-recovery from various microfluidic operations involving droplet motion and reaction. Recently, a number of cyber-physical systems have been proposed to provide real-time checking and error-recovery in assays based on the feedback received from a few on-chip checkpoints. However, to synthesize robust feedback systems for different types of DMFBs, certain practical issues need to be considered such as co-optimization of checkpoint placement, error-recoverability, and layout of droplet-routing pathways. For application-specific DMFBs, we propose here an algorithm that minimizes the number of checkpoints and determines their locations to cover every path in a given droplet-routing solution. Next, for general-purpose DMFBs, where the checkpoints are pre-deployed in specific locations, we present a checkpoint-aware routing algorithm such that every droplet-routing path passes through at least one checkpoint to enable error-recovery and to ensure physical routability of all droplets. Furthermore, we also propose strategies for executing the algorithms in reliable mode to enhance error-recoverability. The proposed methods thus provide reliability-hardening mechanisms for a wide class of cyber-physical DMFBs.

The active matrix (AM)-based architecture offers many advantages over conventional digital electrowetting-on-dielectric (EWOD) microfluidic biochips, such as the capability of handling variable-size droplets, more flexible droplet movement, and precise control over droplet navigation. However, a major challenge in choosing the routing paths is to decide when the droplets are to be reshaped depending on the congestion of the intended path, or split- and route sub droplets,and merging them at their respective destinations. As the number of microelectrodes in AM-EWOD chips is large, the path selection problem becomes further complicated. In this article, we propose a negotiation-guided flow based on routing of subdroplets that obviates the explicit need for deciding when the droplets are to be manipulated, yet fully utilizing the power of droplet reshaping, splitting, and merging them to facilitate their journey. The proposed algorithm reduces routing cost and provides more freedom in deadlock avoidance in the presence of multiple routing tasks by assigning certain congestion penalty for sibling subdroplets and fluidic penalty for heterogeneous droplets. Compared to existing techniques, it reduces latest arrival time by an average of 29% for several benchmark and random test suites. Furthermore, our method is observed to provide 100% routability of nets for all test cases, whereas existing and baseline routers fail to produce feasible solutions in many instances. We also propose a reliable mode droplet routing strategy where the number of unreliable splitting operations can be reduced by paying a small penalty on latest arrival time.

In the area of biomedical engineering, digital-microfluidic biochips (DMFBs) have received considerable attention, because of their capability of providing an efficient and reliable platform for conducting point-of-care clinical diagnostics. System reliability, in turn, mandates error-recoverability while implementing biochemical assays on-chip for medical applications. Unfortunately, the technology of DMFBs is not yet fully equipped to handle error-recovery from various microfluidic operations involving droplet motion and reaction. Recently, a number of cyber-physical systems have been proposed to provide real-time checking and error-recovery in assays based on the feedback received from a few on-chip checkpoints. However, in order to synthesize robust feedback systems for different types of DMFBs, certain practical issues need to be considered such as co-optimization of checkpoint placement and layout of droplet-routing pathways. For application-specific DMFBs, we propose here an algorithm that minimizes the number of checkpoints and determines their locations to cover every path in a given droplet-routing solution. Next, for general-purpose DMFBs, where the checkpoints are pre-deployed in specific locations, we present a checkpoint-aware routing algorithm such that every droplet-routing path passes through at least one checkpoint to enable error-recovery and to ensure physical routability of all droplets. Our experiments on assay benchmarks show encouraging results in terms of latest-arrival-time and routability of droplets. The proposed methods thus provide convenient reliability-hardening mechanisms for a wide class of cyber-physical DMFBs.

Computation offloading frameworks partition an application's execution between a cloud server and the mobile device to minimize its completion time on the mobile device. An important component of an offloading framework is the partitioning algorithm that decides which tasks to execute on mobile device or cloud server. The partitioning algorithm schedules tasks of a mobile application for execution either on mobile device or cloud server to minimize the application finish time. Most offloading frameworks partition parallel applications devices using an optimization solver which takes a lot of time. We show that by allowing duplicate execution of selected tasks on both the mobile device and the remote cloud server, a polynomial algorithm exists to determine a schedule that minimizes the completion time. We use simulation on both random data and traces to show the savings in both finish time and scheduling time over existing approaches. Our trace-driven simulation on benchmark applications shows that our algorithm reduces the scheduling time by 8 times compared to a standard optimization solver while guaranteeing minimum makespan.

In this paper, we examine the problem of data dissemination and optimization in the context of a large scale distributed cyber-physical system (CPS), and propose a novel rule-based mechanism for effective observation collection and transmission. Our work rests on the idea that all observations on all parameters are not required at all times, and thereby, selective data transmission can reduce sensor workload significantly. Experiments show the efficacy of our proposal.

Advances in digital microfluidic (DMF) technologies offer a promising platform for a variety of biochemical applications, ranging from massively parallel DNA analysis and computational drug discovery to toxicity monitoring and medical diagnosis. In this paper, we address the migration problem that arises when the technology undergoes a change in the context of DMFs. Given a biochemical reaction synthesized for actuation on a given DMF architecture, we discuss how the same biochemical reaction can be ported seamlessly to an enhanced architecture, with possible modifications to the architectural parameters (e.g., clock frequency, mixer size, and mixing time) or geometric changes (e.g., change in reservoir locations or mixer positions, inclusion of new sensors or other physical resources). Complete resynthesis of the protocol for the new architecture may often become either inefficient or even infeasible due to scalability, proprietary, security, or cost issues. We propose an adaptation method for handling such technology-changes by modifying the existing actuation sequence through an incremental procedure. The foundation of our method lies in symbolic encoding and satisfiability-solvers, enriched with pertinent graph-theoretic and geometric techniques. This enables us to generate functionally correct solutions for the new target architecture without necessitating a complete resynthesis step, thereby enabling the utilization of these chips by users in biology who are not familiar with the on-chip synthesis tool-flow. We highlight the benefits of the proposed approach through extensive simulations on assay benchmarks.

In recent times, approximate computing is being increasingly adopted across the computing stack, from algorithms to computing hardware, to gain energy and performance efficiency by trading accuracy within acceptable limits. Approximation aware programming languages have been proposed where programmers can annotate data with type qualifiers (e.g., precise and approx) to denote its reliability. However, programmers need to judiciously annotate so that the accuracy loss remains within the desired limits. This can be non-trivial for large applications where error resilient and non-resilient program data may not be easily identifiable. Mis-annotation of even one data as error resilient/insensitive may result in an unacceptable output. In this paper, we present AutoSense, a framework to automatically classify resilient (insensitive) program data versus the sensitive ones with probabilistic reliability guarantee. AutoSense implements a combination of dynamic and static analysis methods for data sensitivity analysis. The dynamic analysis is based on statistical hypothesis testing, while the static analysis is based on classical data flow analysis. Experimental results compare our automated data classification with reported manual annotations on popular benchmarks used in approximate computing literature. AutoSense achieves promising reliability results compared to manual annotations and earlier methods, as evident from the experimental results.

In recent times, automated business processes and web services have become ubiquitous in diverse application spaces. Efficient composition of web services in real time while providing necessary Quality of Service (QoS) guarantees is a computationally complex problem and several heuristic based approaches have been proposed to compose the services optimally. In this article, we present the design of a scalable QoS-aware service composition mechanism that balances the computational complexity of service composition with the QoS guarantees of the composed service and achieves scalability. Our design guarantees a single QoS parameter using an intelligent search and pruning mechanism in the composed service space. We also show that our methodology yields near optimal solutions on real benchmarks. We then enhance our proposed mechanism to guarantee multiple QoS parameters using aggregation techniques. Finally, we explore search time versus solution quality tradeoff using parameterized search algorithms that produce better-quality solutions at the cost of delay. We present experimental results to show the efficiency of our proposed mechanism.

In recent times, approximate computing is being looked at as a viable alternative for reducing the energy consumption of programs, while marginally compromising on the correctness of their computation. The idea behind approximate computing is to introduce approximations at various levels of the execution stack, with an attempt to realize the resource hungry computations on low resource consuming approximate hardware blocks. However approximate computing for program transformation faces a serious challenge of automatically identifying core program areas/statements where approximations can be introduced, with a quantifiable measure of the resulting program correctness compromise. Introducing approximations randomly can cause performance deterioration without much energy advantage, which is undesirable. In this paper, we introduce a verification-guided method to automatically identify program blocks which lend themselves to easy approximations, while not compromising significantly on program correctness. Our method is based on identifying regions of code which are less influential for the computation of the program outputs and therefore, can be compromised with, however still having a potential of significant resource reduction. We take the help of assertions to quantify the effect of the resulting transformations on program outputs. We show experimental results to support our proposal.

Mobile cloud computing is increasingly being used in recent times to offload parts of an application to the cloud to reduce its finish time. However, quality of offloading decisions depend on network conditions and hence many offloading solutions assume that MAC layer retransmissions will tackle transient frame errors. This can lead to suboptimal solutions, as well as, degrade service level guarantee of reducing finish time compared to execution without offloading. In this work, we propose an error-aware solution that uses run-time channel conditions to adapt the offloading decisions. We guarantee that given a failure rate bound (ϵ), offloading decisions will achieve application execution in less time than that of local execution with a probability of (1-ϵ) while operating in networks with unpredictable error characteristics. Simulation results show that at channel error rate of 20%, our heuristic provides 90% guarantee of better performance than on-device computation and reduces the mean finish time by 18% compared to execution without any offloading.

In recent times, automated business processes and web service technologies have become popular and ubiquitous for catering to diverse user needs. While providing a service, the service providers are typically expected to furnish promised QoS values for the services they deliver. However, when the services are physically deployed and invoked during a query resolution, these parameter values vary largely depending on different factors like network load, number of applications running in the server etc. In this work, we present a stochastic model of the web service composition problem. Experimental results on Web Service Challenge (WSC) benchmarks show the efficiency of our proposed mechanism.

In this work, we propose a framework for construction of an approximate environment for compositional verification using invariants learned from dynamic traces of the system and the counterexamples generated by a model checker on verifying a property on the component in isolation. We adopt a counterexample ranking methodology for eliminating possibly fictitious counterexamples by choosing a minimal subset of the invariants. We explore the aspect of choosing a threshold for counterexamples as well as assume properties which can contribute towards further refining the subset chosen and produce a stronger abstraction. Experimental results on benchmark designs shows the efficacy of our proposal.

In recent times, automated business processes and web services have become ubiquitous in diverse application spaces. Efficient composition of web services in real time while providing necessary QoS guarantees is a computationally complex problem and several heuristic based approaches have been proposed to compose services optimally. In this paper, we present the design of a scalable but approximate QoS-aware service composition mechanism which balances the computational complexity of service composition with the QoS guarantees of the composed service and achieves scalability for dynamic service composition. We present experimental results to show the efficiency of our proposed mechanism.

In this paper, we address the problem of application scheduling on user mobile devices. Given the fact that a vast number of applications may run both as in the foreground and the background, the scheduling task is a challenging one. We propose to solve this problem in this paper using clustering and iterative refinement. Results on simulated benchmarks show the efficacy of our proposal.

Software evolution has been extensively studied in the past decade for various properties and interesting patterns. In this work, we study the effect of evolution on branch prediction techniques. Typically for any program, at the hardware level, all dynamic branch prediction strategies learn the branch behaviors at run time and later re-use them to predict the direction of future branches. The duration of the learning curve depends heavily on the kind of technique used and also the complexity of the program at hand. We propose that saving the branch outcome profile from an older version and reusing it in a new version can significantly reduce this overhead and improve performance. In this paper, we discuss the effect of program evolution on the performance of branch prediction, study how the individual branches get affected during evolution, suggest a new method to reuse the branch behavior information from a previous version, and share our results on various software repositories. Preliminary results indicate our intuitions are well justified.

Making mobile applications energy efficient immensely builds user satisfaction. Apart from the fact that there are not many efficient techniques for evaluating energy consumption for applications on mobile devices, the methods used are static in nature. Static techniques assume that during the running of an application, no other process can run concurrently, and the concerned application has the entire CPU at its disposal. In this paper, we propose a novel idea of measuring the energy consumption of an application running on a mobile device considering the fact that not always the entire CPU is available. This is because the application may sometimes run in the foreground when the mobile is idle and therefore, use the maximum CPU available, at other times, there maybe other tasks being run (apart from the routine background tasks) by the user for which this application is forced to run in the background. The major highlight of this paper is in considering the concept of variable CPU availability in energy analysis. We have also suggested to model the energy consumption problem of a mobile phone as a finite state automaton, where our aim is to find if a state can be reached where the entire battery of the mobile phone is exhausted.

Microfluidic biochips are recently being advocated for on-chip implementation of several biochemical laboratory assays or protocols [1]. Such labs-on-a-chip (LoC) have brought a complete paradigm shift in DNA analysis, toxicity grading, in molecular biology, and in drug design and delivery. This technology offers a viable and low-cost platform for reducing healthcare cost of cardiovascular diseases, cancer, diabetes, for providing point-of-care (P-o-C) health services [2, 3], and for the management of bio-terrorism threats [4]. These chips are also immensely useful for rapid and accurate diagnosis of various diseases including malaria, human immunodeficiency virus infection (HIV), acquired immunodeficiency syndrome (AIDS), and for mitigating neglected tropical diseases (NTD) prevalent in the developing countries [5].

In a mobile grid computing framework where mobile devices are used as computing resources, minimizing the task offloading time remains an important issue. A task is an independent unit of execution consisting of a input data volume for execution and optionally a target-specific executable. We consider a mobile grid infrastructure where mobile devices are connected via Wi-Fi network and the grid infrastructure has a set of tasks (i.e. a set of data volumes) to be transferred to a subset of the mobile devices. In a Wi-Fi network, mobile devices usually associate themselves to the access points (APs) having the strongest radio signal. In this paper, we address the problem of AP activation (by frequency assignment) and association of AP with devices in the context of minimizing the overall data-transfer completion time. We present a constraint based formulation and also a heuristic as solutions. Simulations results are presented which contrast our proposed methods with some of the earlier works.

Cloud computing is fast emerging as a popular choice for a variety of business needs. Providing adequate fault tolerance guarantees to diverse applications is an important challenge. Fault tolerance needs vary from one application to another. Fault tolerance consumes resources. In this paper, we propose fault tolerance to be added as a service, termed here as FTaaS, which can provide both spatial and temporal redundancies. A tenant (who seeks fault tolerance services) can express its intended fault tolerance level as part of the Service Level Agreement (SLA). In this paper, we investigate a general setting, where a tenant can execute in different modes, with different fault tolerance criterion. The task of a provider (who sells fault tolerance services) is to configure his offerings in accordance to the tenants' requirements, in a way which keeps his customers satisfied and his revenue is maximized. We consider several variations of this problem in the paper. We also discuss the other side of the tenant-provider setting, wherein a tenant has multiple providers to choose from, keeping in mind the requirements he has and the cost he has to pay to avail the services. We present formulations of optimization problems related to these in this work.

With the growing complexity and gradually shrinking power requirements in the system-on-chip designs, sophisticated global power management policies (which orchestrate the switching between power states of multiple power domains) are commonplace. Recent research has paved some novel ways to verify the sophisticated on-chip architectural power management decisions and analyze the verification coverage. However, one of the primary challenges in verifying such power management architectures stems from the mixed implementation of such strategies, where the local power controllers are in hardware and the global power management is implemented in software/firmware. There has been lack of effort to build a unified and automated framework for power intent verification and coverage analysis for generic power management logics. This paper tries to develop an end-to-end automated framework enabled by a tool named POWER-TRUCTOR for power intent validation.

Bug traces produced in simulation serve as the basis for patching the RTL code in order to fix a bug. It is important to prove that the patch covers all instances of the bug scenario; otherwise, the bug may return with a different valuation of the variables involved in the bug scenario. For large circuits, formal methods do not scale well enough to comprehensively eliminate the bug, and achieving adequate coverage in simulation and regression testing becomes expensive. This paper proposes formal methods for analyzing the control trace leading to the observed manifestation of the bug and verifying the robustness of the bug fix with respect to that control trace. We propose a classification of the bug fix based on the guarantee that our analysis can provide about the quality of the bug fix. Our method also prescribes the types of tests that are recommended to validate the bug fix on other types of scenarios. Since our methods are more scalable by orders of magnitude than model checking the entire design, we believe that the proposed formal methods hold immense promise in analyzing bug fixes in practice.

Bug-fixing in deeply embedded portions of the logic is typically accompanied by the postfacto addition of new assertions, which cover the bug scenario. Formally verifying the assertions defined over such deeply embedded portions of the logic is challenging because formal methods do not scale to the size of the entire logic. Verifying the assertion on the embedded logic in isolation typically throws up a large number of counterexamples, many of which are spurious because the scenarios they depict are not possible in the entire logic. In this paper, we introduce the notion of ranking the counterexamples so that only the most likely counterexamples are presented to the designer. Our ranking is based on assume properties mined from simulation traces of the entire logic. We define a metric to compute a belief for each assume property that is mined, and rank counterexamples based on their relationships with the mined assume properties. Experimental results demonstrate a remarkable correlation between the real counterexamples (if they exist) and the proposed ranking metric, thereby establishing the proposed method as a very promising verification approach.

The architectural power intent of a design defines the intended global power states of a power-managed integrated circuit. Verification of the implementation of power management logic involves the task of checking whether only the intended power states are reached. Typically, the number of global power states reachable by the global power management strategy is significantly lesser than the possible number of global power states. In this paper, we present a formal method for determining the set of reachable global power states in a power-managed design. Our approach demonstrates how this task can be further constrained as required by the verification engineer. We highlight the efficacy of the proposed methods over several test-cases.

Coverage of formal property specifications has important ramifications in design verification. Mutation coverage, a well studied approach towards specification coverage, checks whether the specification fails in the presence of a fault. Existing mutation coverage methods are broadly divided into those which inject the fault into a given implementation and those which inject the fault directly into the specification. This paper presents a theory which unifies these contrasting approaches and extends the mutation coverage approach to partial implementations where some components are given, and for the others, we only have component specifications.

Many cyber-physical systems consist of a collection of control loops implemented on multiple electronic control units (ECUs) communicating via buses such as FlexRay. Such buses support hybrid communication protocols consisting of a mix of time- and event-triggered slots. The time-triggered slots may be perfectly synchronized to the ECUs and hence result in zero communication delay, while the event-triggered slots are arbitrated using a priority-based policy and hence messages mapped onto them can suffer non-negligible delays. In this paper, we study a switching scheme where control messages are dynamically scheduled between the time-triggered and the event-triggered slots. This allows more efficient use of time-triggered slots which are often scarce and therefore should be used sparingly. Our focus is to perform a schedulability analysis for this setup, i.e., in the event of an external disturbance, can a message be switched from an event-triggered to a time-triggered slot within a specified deadline? We show that this analysis can check whether desired control performance objectives may be satisfied, with a limited number of time-triggered slots being used.

Bug-fixing in deeply embedded portions of the logic is typically accompanied by the post-facto addition to new assertions which cover the bug scenario. Formally verifying properties defined over such deeply embedded portions of the logic is challenging because formal methods do not scale to the size of the entire logic, and verifying the property on the embedded logic in isolation typically throws up a large number of counterexamples, many of which are spurious because the scenarios they depict are not possible in the entire logic. In this paper we introduce the notion of ranking the counterexamples so that only the most likely counterexamples are presented to the designer. Our ranking is based on assume properties mined from simulation traces of the entire logic. We define a metric to compute a belief for each assume property that is mined, and rank counterexamples based on their conflicts with the mined assume properties. Experimental results demonstrate an amazing correlation between the real counterexamples (if they exist) and the proposed ranking metric, thereby establishing the proposed method as a very promising verification approach.

Multiplayer games are played by a set of agents, where, at each round, all players give their moves, and the combination of their moves defines the successor states for the game. In such games, the players pursue certain goals with their moves and in that pursuit, they can form coalitions to fulfill a common objective. In this paper, we adopt this model of multiplayer coalition games in the context of 3-party systems, consisting of a module, its environment, and a controller. The winning objective of our game is given as a specification in linear temporal logic and the module and controller together attempt to satisfy the specification for all possible strategies of the environment. In this paper, we analyze the problem for various degrees of observability of the module-controller pair, and provide quantified Boolean formula-based methods for investigating the existence of a winning coalition strategy. The coalition strategy can only be fulfilled on carefully implementing both the module and the controller such that they can cooperate. We also consider the problem where the implementations of the module and the controller are available and we present a dynamic simulation-based approach for verifying whether these implementations conform to the coalition requirements. In case, they do not, we provide algorithms for designing the winning strategy for an intelligent environment to drive the coalition to a refutation.

This paper presents a formal methodology for test generation from formal specifications. Our method can be used for test generation for critical faults in component-based designs. Test generation for critical faults is done entirely using formal specifications and therefore the theory inherently guarantees that a generated test will be applicable to any implementation of the specifications. The theory makes fault analysis possible at an abstract level of design where the complete logic is not specified.

Automated methods for bug localization for hardware designs typically work on the design implementation to root-cause a given bug. This paper presents a novel debugging approach where instead of using the design implementation in the debugging process, we use causal deduction using formal properties scattered across the design to locate the bug. This has two advantages, namely, (a) the reasoning takes place in the property space instead of the state space of the implementation, which enhances scalability, and (b) new properties can be added in hindsight to perform what-if analysis, which is less expensive than modifying the implementation for each alternative. Experimental results demonstrate the scalability of the approach in debugging designs with large property suites.

The presence of a functionally correct golden implementation has a significant advantage in the software development life cycle. Such a golden implementation is exploited for software development in several domains, including embedded software --- a low resource-consuming version of the golden implementation. The golden implementation gives the functionality that the program is supposed to implement, and is used as a guide during the software development process. In this paper, we investigate the possibility of using the golden implementation as a reference model in software debugging. We perform a substantial case study involving the Busybox embedded Linux utilities while treating the GNU Core Utilities as the golden or reference implementation. Our debugging method consists of dynamic slicing with respect to the observable error in both the implementations (the golden implementation as well as the buggy software). During dynamic slicing we also perform a step-by-step weakest precondition computation of the observable error with respect to the statements in the dynamic slice. The formulae computed as weakest pre-condition in the two implementations are then compared to accurately locate the root cause of a given observable error. Experimental results obtained from Busybox suggest that our method performs well in practice and is able to pinpoint all the bugs recently published in [8] that could be reproduced on Busybox version 1.4.2. The bug report produced by our approach is concise and pinpoints the program locations inside the Busybox source that contribute to the difference in behavior.

We present a new approach to bias random test generation for accelerating assertion coverage. The novelty of the proposed approach is that it treats the design under test as a black box and attempts to steer the simulation toward coverage points that are relevant for targeted assertions purely through external control. We present this approach over three different models with varying degrees of observability and control. The results demonstrate a significant speedup in assertion coverage as compared to randomized simulation.

Formal specifications of interface protocols between a design-under-test and its environment mostly consist of two types of correctness requirements, namely (a) a set of invariants that applies throughout the protocol execution and (b) a set of context-triggered properties that applies only when the protocol state belongs to a specific set of contexts. To model such requirements, an increasingly popular design choice in the assertion IP design community has been the use of abstract context state machines and state-oriented properties. In this paper, we formalize this modeling style and present algorithms for verifying such specifications. Specifically, we present a purely formal approach and a semi-formal approach for verifying such specifications. We demonstrate the use of this design style in modeling some of the industry standard protocol descriptions and present encouraging results.

In this paper, we present methods for automatic test generation from formal specifications. These are used to create intelligent test benches that are able to cover corner case behaviors in much less time. We have developed a prototype tool for intelligent test generation within the layered test bench architecture proposed in RVM. We present results on verification IPs of standard bus protocols to show the effectiveness of our approach.

The main contributions of this paper are as follows: We revisit the concept of multiplayer coalition games in the context of a 3-party system. We analyze the coalition realizability problem for different degrees of observability of the module and the controller. We show that the realizability problem can be expressed as an instance of quantified Boolean formulas (QBF), by using appropriate quantifications on the variables of the environment, the module and the controller. We then use recent QBF solvers to verify

It is essential to formally ascertain whether the register-transfer level (RTL) validation effort effectively guarantees the correctness with respect to the design's architectural intent. The design's architectural intent can be expressed in formal properties. However, due to the capacity limitations of formal verification, these architectural properties cannot be directly verified on the RTL. As a result, a set of lower level RTL properties are developed and verified against the RTL modules. In a top-down design approach, the architect would ideally like to formally guarantee the coverage of the architectural intent at the time of creating the specifications for the component RTL modules (that is, before they are passed to the designers for implementation). In this paper, the authors present: 1) a method for checking whether the RTL properties are covering the architectural properties, that is, whether verifying the RTL properties guarantees the correctness of the design's architectural intent; 2) a method to identify which architectural properties are still uncovered, that is, not guaranteed by the RTL properties; and 3) a methodology for representing the gap between the specifications in a legible form

Assume-guarantee style verification of modules relies on the appropriate modeling of the interaction of the module with its environment. Popular temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) that were originally defined for closed systems (Kripke structures) do not make any syntactic discrimination between input and output variables. As a result, these logics and their recent derivatives (such as System Verilog, Sugar, Forspec, etc) permit the specification of properties that have some semantic problems when interpreted over open systems or modules. These semantic problems are quite common in practice, but are computationally hard to detect within a given specification. In this article, we propose a new style for writing temporal specifications of open systems that helps the designer to avoid most of these problems. In the proposed style, the basic temporal operators (such asnextanduntil) are annotated withassumeconstraints over the input variables. We formalize this style through an extension of LTL, namely Open-LTL and an extension of CTL with fairness, called Open-CTL. We show that this simple syntactic separation between theassumeand theguaranteeachieves the desired results. We show that the proposed style can be integrated with traditional symbolic model-checking techniques and present a complete tool for the verification of Verilog RTL modules in isolation.

Existing methods for formal verification coverage compare a given specification with a given implementation, and evaluate the coverage gap in terms of quantitative metrics. We consider a new problem, namely to compare two formal temporal specifications and to find a set of additional temporal properties that close the coverage gap between the two specifications. In this paper we present: (1) the problem definition and motivation, (2) a methodology for computing the coverage gap between specifications, and (3) a methodology for representing the coverage gap as a collection of temporal properties that preserve the syntactic structure of the target specification.

A typical verification IP (VIP) of a bus protocol such as ARM AMBA or PCI consists of a set of assertions and associated verification aids like test-benches and coverage metrics. While, several languages have been formalized for specifying assertions (examples include OVA, Sugar, ForSpec, SVA, etc), the tasks of writing test-benches that produce protocol compliant stimuli and coverage monitors that reflect the coverage of the protocol functionality are also of significant importance. This paper presents a platform for high-level specification of a bus protocol and an automated methodology for generating a variety of verification aids that must supplement the set of assertions in a VIP.

KJ1E.LCM*-N$\t?. -! #M$ O$ ?(P($ '(\tRQ?SDI 4%\t-T *,!)"'4)U$\tVLWPXK YL*H%KZ4 (\tRQ?SDI 29000 !))D4 8950-50010 '4)U$\tVLWPXK YL*H%KZ4 (\tRQ?SD 6`Ga#:bSD=BCGc'4) ed$fRgTh3JKQ]9 Z! H,!,2@b T /\tiL4R))$Lj k(%$ Rj +%,T-. ! \tDE 28940-47920 4 28929-46860 Lj k(%$ Rj +%,T-. ! \tDE 28940 - :&< =?> %+(P$ '.\tKJKQlK jT\t '4\t# ['()W E =?> %+(P$ '.\tKJKQlK jT\t '4\t# ['()W 2 %)Qe=VN H44 *! ' \\\t;E K jT\t '4\t vDrKtwxnRnqyER 4 4 ER 28810-42690 \\\t;E K jT\t '4\t# ['()W 289 MK!)*)RM jER;4 E K jT\t '4\t# ['()W 28900-447 K *, 14%\t&(P( '. Q|SD1 .)24 I _e%E\t1b}b )*Q/>&L[~(j ;14 (P($ '.\t \\\t-!*. @MD! ?!E)1 ;PX $3LZ;'(%)* e)*! @[ E.LCTP*[ +\\\t-! ;U4)*O4 E)* % 1'4 @[ E.LCTP*[ +\\\t-! ;U4)*O4 E)* %)$ '(%)&Y 1SyU\\Ii+>&-T...