Multi-property formal verification remains a significant challenge in the chip design industry. With hundreds of property goals to verify in a design, several questions arise regarding goal ordering and grouping of properties, sharing of information across proven properties, and other heuristics to improve the verification productivity. This paper introduces SISCO, a novel method for addressing multi-property verification in complex designs. SISCO unfolds properties to a certain depth, clusters them, reorders properties within each cluster, and then uses a modified version of IC3/Property Directed Reachability (PDR) algorithm for efficient verification. The method stores the invariants of proven properties and selectively shares them while solving undecided goals. Additionally, SISCO keeps track of counter-example traces of falsified goals to assist verification. Experimental results demonstrate that clustering and ordering help solve more goals while selective invariant sharing accelerates the process. SISCO achieves a significant average improvement of 4.73× in the runtime of individual goals compared to all invariant sharing.

Constrained Reinforcement Learning (RL) aims to maximize the return while adhering to predefined constraint limits, which represent domain-specific safety requirements. In continuous control settings, where learning agents govern system actions, balancing the trade-off between reward maximization and constraint satisfaction remains a significant challenge. Policy optimization methods often exhibit instability near constraint boundaries, resulting in suboptimal training performance. To address this issue, we introduce a novel approach that integrates an adaptive incentive mechanism in addition to the reward structure to stay within the constraint bound before approaching the constraint boundary. Building on this insight, we propose Incrementally Penalized Proximal Policy Optimization (IP3O), a practical algorithm that enforces a progressively increasing penalty to stabilize training dynamics. Through empirical evaluation on benchmark environments, we demonstrate the efficacy of IP3O compared to the performance of state-of-the-art Safe RL algorithms. Furthermore, we provide theoretical guarantees by deriving a bound on the worst-case error of the optimality achieved by our algorithm.

With the growing scale of integration of solar power in the grid, the supply side uncertainties in the grid are increasing. The increase in supply side uncertainties can result in a large number of future states that need to be analyzed for secure and optimal grid operation within a short window of time. The uncertainties in solar power in the future can lead to grid congestion. The grid may force to remain congested until the grid operator solve the optimal power flow (OPF) to decide and implement nonrenewable generation dispatch to avoid congestion in response to the fluctuation in solar power. This requires an early and real-time estimation of congestion and then a real-time optimal power flow (RTOPF) to decide optimal dispatch decisions to avoid congestion. Therefore in this article, we propose a novel two-stage approach called OPF$k$nearest neighborhood (OPF$k$NN). In the first stage, we propose a machine learning (ML) binary classification problem and optimized ML model to estimate the congested/noncongested state of the grid directly from the generation data. The second stage is a neighborhood-based search approach for RTOPF to decide the optimal generation dispatch of the nonrenewable generation to avoid congestion. The proposed OPF$k$NN has been implemented on the IEEE 118 bus system and Polish 2383 bus system to demonstrate the effectiveness of our proposed approach.

Safe Reinforcement Learning (SRL) algorithms aim to learn a policy that maximizes the reward while satisfying the safety constraints. One of the challenges in SRL is that it is often difficult to balance the two objectives of reward maximization and safety constraint satisfaction. Existing algorithms utilize constraint optimization techniques like penalty-based, barrier penalty-based, and Lagrangian-based dual or primal policy optimizations methods. However, they suffer from training oscillations and approximation errors, which impact the overall learning objectives. This paper proposes the Permeable Penalty Barrier-based Policy Optimization (P2BPO) algorithm that addresses this issue by allowing a small fraction of penalty beyond the penalty barrier, and a parameter is used to control this permeability. In addition, an adaptive penalty parameter is used instead of a constant one, which is initialized with a low value and increased gradually as the agent violates the safety constraints. We have also provided a theoretical proof of the proposed method's performance guarantee bound, which ensures that P2BPO can learn a policy satisfying the safety constraints with high probability while achieving a higher expected reward. Furthermore, we compare P2BPO with other SRL algorithms on various SRL tasks and demonstrate that it achieves better rewards while adhering to the constraints.

Multi-property verification has emerged as a con-temporary challenge in the chip design industry. With designs now encompassing hundreds of properties, conventional sequential verification without information sharing is no longer preferred. Past attempts towards grouping or ordering properties based on cone-of-influence (COI) are typically ineffective for complex designs. This paper introduces PURSE, a novel approach that addresses this challenge by dynamically reordering properties for sequential and incremental solving. By identifying and prioritizing simpler properties, the process accelerates convergence. This article presents two dynamic reordering techniques guided by statistical data gathered from the IC3/Property Directed Reachability (PDR) proof engine. The study compares dynamic ordering strategies against static ordering and a default ordering based on design structure. Empirical results from various industrial designs demonstrate that our proposed methodology performs better in most cases, with up to 25% improvements in convergence.

Autonomous management of multiple services is a crucial requirement of 6G networks. In recent years, researchers have been working on using artificial intelligence(AI) to orchestrate intents, autonomously, through Intent Management Functions (IMFs). These IMFs can handle conflicting service intents and prioritize the global objective based on predefined utility function and intent priorities. However, for such frameworks to be successful in real-life scenarios, they must be flexible to business situations. Service priorities can change, and the utility function that measures the fulfillment of objectives may also vary in definition. This paper proposes a novel method that enables the IMF to adapt to unseen forms of utility functions and changes in service priorities at run-time without requiring additional training. We assume the IMF contains agents trained using multi-agent reinforcement learning (MARL) to perform actions and multiple such MARL systems are orchestrated by Ad-hoc teaming approaches. Results on a network emulator demonstrate the effectiveness of the approach, outperforming existing state-of-the-art methods that require additional training to achieve the same flexibility, thereby saving costs and increasing adaptability.

Certain data compression techniques like pruning leads to unstructured sparse Convolution Neural Network (CNN) models without directly leveraging sparsity in optimizing both memory consumption and inference latency of a model having low to medium sparsity. State-of-the-art storage techniques either optimize model size at the cost of execution latency or optimize inference latency at the overhead of the memory consumption of the model. This tradeoff is largely due to the absence of storage selection methodology addressing sparsity sensitivity , arising from varied sparsity and positions of nonzero values called sparsity structure across different sparse layers of a model. However, this issue remains unexplored due to the lack of support to handle sparse data in the current deployment standards for edge devices. This article introduces a data compaction strategy for unstructured sparse data that not only compresses nonzero data but also encodes it, leveraging the memory consumption and latency reduction benefits of both data compression and data encoding techniques . We propose a novel storage representation, named Encoded Partitioned Hybrid Sparse (EPaHS) format, which addresses sparsity sensitivity by customizing data storage based on the sparsity structure of the data. Our data compaction technique and storage solution optimizes the tradeoff between the memory consumption and inference latency of a sparse model without altering the network architecture and affecting its accuracy. Our solution easily extends to higher-dimensional data and outperforms standard storage solutions. It proves to be beneficial to all the valid mode orientations of multi-dimensional data. For an important health and wellness application, a single-lead short-time ECG classification model, EPaHS achieves up to \({\tt 16.18\%}\) reduction in size and \({\tt 15.16\%}\) reduction in latency when compared to its original model of \({\tt 42}\) MB size and \({\tt 26.35}\) sec latency, having \({\tt \approx 59\%}\) sparsity. For a ResNet50 model handling higher-dimensional data, it achieves \({\tt 21.33\%}\) size reduction and \({\tt 53.9\%}\) latency gain against the original model of \({\tt 3265}\) KB size and \({\tt 1.7}\) sec latency, having \({\tt \approx 67\%}\) sparsity.

Neural network pruning is a technique of network compression by removing weights of lower importance from an optimized neural network. Often, pruned networks are compared in terms of accuracy, which is realized in terms of rewards for Deep Reinforcement Learning (DRL) networks. However, networks that estimate control actions for safety-critical tasks, must also adhere to safety requirements along with obtaining rewards. We propose a methodology to iteratively refine the weights of a pruned neural network such that we get a sparse high-performance network without significant side effects on safety.

Integrated circuit designs are evaluated at various corners defined by choices of the design and process parameters. Considering the large number of corners and the simulation cost of covering all the corners of a large design, it is desirable to identify a subset of the corners that can potentially expose corner case bugs. In an integrated analog coverage management framework, this choice may be influenced by those corners that take one or more component analog IPs close to their individual specification boundaries. Since the admissible state space of an analog IP is multi-dimensional, the same corner may not reach the extreme behaviors for each attribute of the specification, and one needs to identify a subset that covers the extremality. This paper shows that the underlying problem is NP-hard and presents an automated methodology for selecting the corners. A formal analog coverage specification is leveraged by our algorithm, which uses a Satisfiability Modulo Theory (SMT) solver to identify the appropriate corners from the output of multiple Monte Carlo (MC) simulations. The efficacy of the proposed approach is demonstrated over industrial test cases.

The rising demand for networked embedded systems with machine intelligence has been a catalyst for sustained attempts by the research community to implement Convolutional Neural Networks (CNN) based inferencing on embedded resource-limited devices. Redesigning a CNN by removing costly multiplication operations has already shown promising results in terms of reducing inference energy usage. This paper proposes a new method for replacing multiplications in a CNN by table look-ups. Unlike existing methods that completely modify the CNN operations, the proposed methodology preserves the semantics of the major CNN operations. Conforming to the existing mechanism of the CNN layer operations ensures that the reliability of a standard CNN is preserved. It is shown that the proposed multiplication-free CNN, based on a single activation codebook, can achieve 4.7x, 5.6x, and 3.5x reduction in energy per inference in an FPGA implementation of MNIST-LeNet-5, CIFAR10-VGG-11, and Tiny ImageNet-ResNet-18 respectively. Our results show that the DietCNN approach significantly improves the resource consumption and latency of deep inference for smaller models, often used in embedded systems. Our code is available at: https://github.com/swadeykgp/DietCNN

The dynamic and evolutionary nature of service requirements in wireless networks has motivated the telecom industry to consider intelligent self-adapting Reinforcement Learning (RL) agents for controlling the growing portfolio of network services. Infusion of many new types of services is anticipated with future adoption of 6G networks, and sometimes these services will be defined by applications that are external to the network. An RL agent trained for managing the needs of a specific service type may not be ideal for managing a different service type without domain adaptation. We provide a simple heuristic for evaluating a measure of proximity between a new service and existing services, and show that the RL agent of the most proximal service rapidly adapts to the new service type through a well defined process of domain adaptation. Our approach enables a trained source policy to adapt to new situations with changed dynamics without retraining a new policy, thereby achieving significant computing and cost-effectiveness. Such domain adaptation techniques may soon provide a foundation for more generalized RL-based service management under the face of rapidly evolving service types.

With increasing design complexity, the portability of tests across different designs and platforms becomes a key criterion for accelerating verification closure. The Portable Test and Stimulus Standard (PSS) is an emerging industry standard prepared by Accellera for system-on-chip verification and testing. It provides language constructs to create a target-agnostic representation of stimulus and test scenarios reused by various users across many levels of integration. In this article, we present CoVerPlan , a comprehensive verification framework built to explore the power of action inferencing on test models written in PSS. The proposed verification framework leverages a Boolean satisfiability problem planner to unwind the actual verification flow from the PSS specifications and automatically synthesizes target-specific constraint-random testbenches and formal assertions. CoVerPlan also carries out assertion-based verification of the synthesized properties. We demonstrate the efficacy of our proposed framework over several case studies, like the Advanced Microcontroller Bus Architecture advanced peripheral bus protocol, a simple Reduced Instruction Set Computer processor, and a cache coherence protocol.

Mixed-signal assertions need to be monitored over dense time during analog simulation because analog events are not aligned with clock boundaries in general. On the other hand, simulation of large integrated circuits regularly employs clocked approximations to accelerate the simulation of the analog content in the design. Migrating the analog assertions from the continuous setting to the discrete setting is necessary to monitor compliance in the digital–analog boundary, but such migration must ensure that assertion failures are not missed due to the loss in precision. We propose the formal basis for this migration and a methodology for choosing the granularity of the clock for an assertion in the digital setting.

Coverage is a key indicator for verification progress, verification closure, and verification sign-off in an integrated circuit design. The notion of coverage management, namely, the use of coverage information across the design hierarchy to identify verification loopholes, is well understood in the digital context, but requires considerable disambiguation in the analog/mixed-signal (AMS) context. This article develops the core artifacts of AMS coverage and presents a comprehensive coverage management approach based on our tool, CoveRT. Our results, gleaned from live industrial designs, demonstrate the benefits of AMS coverage management across the design hierarchy, both in terms of identifying verification gaps, as well as in finding design bugs.

Recent advances in Reinforcement Learning (RL) combined with Deep Learning (DL) have demonstrated impressive performance in complex tasks, including autonomous driving. The use of RL agents in autonomous driving leads to a smooth human-like driving experience, but the limited interpretability of Deep Reinforcement Learning (DRL) creates a verification and certification bottleneck. Instead of relying on RL agents to learn complex tasks, we propose HPRL - Hierarchical Program-triggered Reinforcement Learning, which uses a hierarchy consisting of a structured program along with multiple RL agents, each trained to perform a relatively simple task. The focus of verification shifts to the master program under simple guarantees from the RL agents, leading to a significantly more interpretable and verifiable implementation as compared to a complex RL agent. The evaluation of the framework is demonstrated on different driving tasks, and National Highway Traffic Safety Administration (NHTSA) pre-crash scenarios using CARLA, an open-source dynamic urban simulation environment.

Adjusting the remote electrical tilt (RET) of antennas is one of the important actions targeting run-time optimization of key performance indicators (KPIs) related to service quality in wireless self-organizing networks (SONs). Reinforcement learning (RL) is one of the preferred Machine Learning methods for automating the choice of RET for all the antennas managed by a company in a region. The automated system should ensure that the system will operate within a safe region to maintain a minimum defined service quality. The safe region of operation is typically customizable based on the targeted service quality at any point in time. This customizable nature of the safe region necessitates automated learning of adaptive safety shields for steering the RL agent away from unsafe regions. This paper presents an adaptive safety shield framework that is capable of learning such shields during the training phase of the RL agent. Our adaptive safety shield framework has been evaluated in different RET scenarios, and we have shown the benefits of our proposed framework over the Baseline method currently in use and a vanilla RL-based method in terms of both safety and performance metrics.

Constructing Reinforcement Learning (RL) policies that adhere to safety requirements is an emerging field of study. RL agents learn via trial and error with an objective to optimize a reward signal. Often policies that are designed to accumulate rewards do not satisfy safety specifications. We present a methodology for counterexample guided refinement of a trained RL policy against a given safety specification. Our approach has two main components. The first component is an approach to discover failure trajectories using Bayesian optimization over multiple parameters of uncertainty from a policy learnt in a model-free setting. The second component selectively modifies the failure points of the policy using gradient-based updates. The approach has been tested on several RL environments, and we demonstrate that the policy can be made to respect the safety specifications through such targeted changes.

We aim to mine temporal causal sequences that explain observed events (consequents) in time-series traces. Causal explanations of key events in a time-series have applications in design debugging, anomaly detection, planning, root-cause analysis and many more. We make use of decision trees and interval arithmetic to mine sequences that explain defining events in the time-series. We propose modified decision tree construction metrics to handle the non-determinism introduced by the temporal dimension. The mined sequences are expressed in a readable temporal logic language that is easy to interpret. The application of the proposed methodology is illustrated through various examples.

The notion of recurrence over continuous or dense time, as required for expressinganalog and mixed-signalbehaviors, is fundamentally different from what is offered by the recurrence operators of SystemVerilog assertions (SVAs). This article introduces the formal semantics of recurrence over dense time and provides a methodology for the runtime verification of such properties using interval arithmetic. Our property language extends SVA with dense real-time intervals and predicates containing real-valued signals. We provide a tool kit that interfaces with off-the-shelf EDA tools through the standard VPI.

The increasing demand for mapping diverse embedded features onto shared electronic control units has brought about novel ways to co-design control tasks and their schedules. These techniques replace traditional implementations of control with new methods, such as pattern-based scheduling of control tasks and adaptive sharing of bandwidth among control loops through orchestration of their execution patterns. In the current practice of control design, once the static execution schedule is prepared for control tasks, no further control-related optimization is attempted for improving the control performance. We introduce, for the first time, an algorithmic mechanism that re-engineers a recurrent control task by enforcing switching between multiple control laws, which are designed for compensating the non-uniform gaps between successive executions of the control task. We establish that such post-processing of control task schedules may potentially help in improving the combined control performance of the co-scheduled control loops that are executing on a shared platform.

Coverage monitoring is fundamental to design verification. Coverage artifacts are well developed for digital integrated circuits and these aim to cover the discrete state space and logical behaviors of the design. Analog designers are similarly concerned with the operating regions of the design and its response to an infinite and dense input space. Analog variables can influence each other in far more complex ways as compared to digital variables, consequently, the notion of cross coverage, as introduced in the analog context for the first time in this paper, is of high importance in analog design verification. This paper presents the formal syntax and semantics of analog cross coverage artifacts, the methods for evaluating them using our tool kit, and most importantly, the insights that can be gained from such cross coverage analysis.

Executing a set of control loops over a shared multi-hop (wireless) control network (MCN) requires careful co-scheduling of the control tasks and the routing of sensory/actuation messages over the MCN. In this work, we establish pattern guided aperiodic execution of control loops as a resource-aware alternative to traditional fully periodic executions of a set of embedded control loops sharing a computation and the communication infrastructure. We provide a satisfiability modulo theory–based co-design framework that synthesizes loop execution patterns having optimized control cost as the underlying scheduling scheme together with the associated routing solution over the MCN. The routing solution implements the timed movement of the sensory/actuation messages of the control loops, generated according to those loop execution patterns. From the given settling time requirement of the control loops, we compute a control theoretically sound model using matrix inequalities, which gives an upper bound to the number of loop drops within the finite length loop execution pattern. Next, we show how the proposed framework can be useful for evaluating the fault tolerance of a resource-constrained shared MCN subject to communication link failure.

Heating ventilation and air conditioning (HVAC) systems usually account for the highest percentage of overall energy usage in large-sized smart building infrastructures. The performance of HVAC control systems for large buildings strongly depend on the outside environment, building architecture, and (thermal) zone usage pattern of the building. In large buildings, HVAC system with multiple air handling units (AHUs) is required to fulfill the cooling/heating requirements. In the present work, we propose an energy-aware building resource allocation and economic model predictive control (eMPC) framework for multi-AHU-based HVAC system. The energy consumption of a multi-AHU-based HVAC system significantly depends on how long the AHUs are running, which again is governed by the zone usage demands. Our approach comprises a two-step hierarchical technique where we first minimize the running time of AHUs by suitably allocating building resources (thermal zones) to usage demands for zones. Next, we formulate a finite receding horizon control problem for trading off energy consumption against thermal comfort during HVAC operations. Given a high-level building specification and usage demand, our computer-aided design framework generates building thermal models, allocates usage demands, formulates the control scheme, and simulates it to generate power consumption statistics for the given building with usage demands. We believe that the proposed framework will help in early analysis during the design phase of energy-aware building architecture and HVAC control. The framework can also be useful from a building operator point of view for energy-aware HVAC control as well as for satisfying smart grid demand-response events by HVAC system peak power reduction through automated control actions.

Mixed-signal components, such as low dropouts (LDOs) and phase locked loops (PLLs), are widely used inside the on-chip power management fabric of low power integrated system-on-chip (SoC) designs. The digital brain of the power management logic that is responsible for regulating the power delivery to different power domains in the chip has to consider the real time latencies of the analog components, which otherwise leads to functional errors in the domains being driven. The latencies may be viewed as contracts between the digital and the analog. This article presents an approach for generating assertions for protecting such mixed-signal latency contracts and using them to rule out timing bugs in the power management logic. Our tool flow enables the verification of the power management fabric, combining a novel mixed-signal assertion checking method in a simulation setting, and a full formal verification method for the digital brain of the power management logic. To the best of our knowledge, this is the first framework where assertions are used for binding analog latency contracts on the digital logic of power management.

The traditional body of literature on analog testing deals with propagation of faults to the output nets of the circuit. Often the set of detectable faults remains unsatisfactory because suitable stimuli cannot be found for propagating certain faults to the output. Existing technology supports capturing of the state of internal nets of a circuit, thereby enhancing the scope of detecting faults by observing their effect on internal nets. This approach is feasible only if the number of internal nets probed by the built-in test structure is very few. This paper presents a structured approach that identifies the sensitive nets, namely a well chosen small subset of internal nets that are affected by these faults. We utilize the speed of DC analysis and some common behavioral aspects of analog signals to find out this subset. We report dramatic improvement in fault coverage on several circuits including benchmarks.

Assessment of the security provided by a fault attack countermeasure is challenging, given that a protected cipher may leak the key if the countermeasure is not designed correctly. This paper proposes, for the first time, a statistical framework to detect information leakage in fault attack countermeasures. Based on the concept of non-interference, we formalize the leakage for fault attacks and provide a t-test based methodology for leakage assessment. One major strength of the proposed framework is that leakage can be detected without the complete knowledge of the countermeasure algorithm, solely by observing the faulty ciphertext distributions. Experimental evaluation over a representative set of countermeasures establishes the efficacy of the proposed methodology.

Detection of faults in a mixed-signal SOC at the pre-silicon stage is a challenge, especially when it has substantial analog components. Given the time taken for simulating analog circuits, designing tests to detect faults in them is not a straightforward task. Achieving a high fault coverage without doing extensive time-consuming transient simulation of the circuit under test (CUT) has remained elusive in the analog and mixed-signal (AMS) domain. Unlike test generation approach for digital designs which leverage logical equivalence between faults, in analog circuits, there does not exist any notion of logical equivalence, and therefore each fault needs to be treated independently. In this paper, we propose to use a combination of DC operating point analysis and AC analysis of the CUT to identify equivalent faults in analog circuits. We also put forward a methodology of synthesizing inputs which will be able to detect the faults during post-silicon testing. Our studies reveal the effectiveness of this approach in identifying equivalent faults and achieving high fault coverage with considerably reduced computations. By using proposed methodology of fault classification and input signal synthesis, we have been able to achieve a high fault coverage where most of the detectable faults are successfully covered.

The support for local variables in SystemVerilog assertions significantly enhances its expressive power. Handling local variables in analog and mixed-signal (AMS) extensions of assertion languages is tricky due to the dense time interpretation of AMS assertions, and has not been adequately treated in existing literature. This paper presents an approach for interpreting local variables in AMS assertions during simulation and a tool flow that works with standard mixed-mode simulators.

Characterizing the fault space of a cipher to filter out a set of faults potentially exploitable for fault attacks (FA), is a problem with immense practical value. A quantitative knowledge of the exploitable fault space is desirable in several applications, such as security evaluation, cipher construction and implementation, design, testing of countermeasures, and so on. In this paper, we investigate this problem in the context of block ciphers. The formidable size of the fault space of a block cipher mandates the use of an automation strategy to solve this problem, which should be able to characterize each individual fault instance quickly. On the other hand, the automation strategy is expected to be applicable to most of the block cipher constructions. Existing techniques for automated fault attacks do not satisfy both of these goals simultaneously, and hence are not directly applicable in the context of exploitable fault characterization. In this paper, we present a supervised machine learning assisted automated framework, which successfully addresses both of the criteria mentioned. The key idea is to extrapolate the knowledge of some existing FAs on a cipher to rapidly figure out new attack instances. Experimental validation of this idea on two state-of-the-art block ciphers - PRESENT and LED - establishes that our approach is able to provide fairly good accuracy in identifying exploitable fault instances at a reasonable cost. Utilizing this observation, we propose a statistical framework for exploitable fault space characterization, which can provide an estimate of the success rate of an attacker corresponding to the given fault model and fault location. The framework also returns test vectors leading toward successful attacks. As a potential application, the effect of different S-Boxes on the fault space of a cipher is evaluated utilizing the framework.

Redundancy based countermeasures against fault attacks are a popular choice in security-critical commercial products, owing to its high fault coverage and applications to safety/reliability. In this paper, we propose a combined attack on such countermeasures. The attack assumes a random byte/nibble fault model with existence of side-channel leakage of the final comparison, and no knowledge of the faulty ciphertext. Unlike the previously proposed biased/multiple fault attack, we just need to corrupt one computation branch. Both analytical and experimental evaluation of this attack strategy is presented on software implementations of two state-of-the-art block ciphers, AES and PRESENT, on an ATmega328P microcontroller, via side-channel measurements and a laser-based fault injection. Moreover, this work establishes that even without the knowledge of the faulty ciphertexts, one can still perform differential fault analysis attacks, given the availability of side-channel information.

In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.

Software implementation of multiple embedded control loops often share compute resources. The control performance of such implementations have been shown to improve if the sharing of bandwidth between control loops can be dynamically regulated in response to input disturbances. In the absence of a structured methodology for planning such measures, the scheduler may spend too much time in deciding the optimal scheduling pattern. Our work leverages well known results in the domain of network control systems and applies them in the context of bandwidth sharing among controllers. We provide techniques that may be used a priori for computing co-schedulable execution patterns for a given set of control loops such that stability is guaranteed under all possible disturbance scenarios. Additionally, the design of the control loops optimize the average case control performance by adaptive sharing of bandwidth under time varying input disturbances.

The EN50128 Railway Safety Standard recommends the use of formal methods for proving the correctness of the yard-specific logic, which was developed for electronic signaling and interlocking systems. We present a tool flow, which consists of three components. The core component uses a novel method for automatically generating the relevant safety properties for a yard from its control table. The second component proves the validity of the properties on the application logic by using a new theory of invariant checking. The third component leverages the suite of formal properties to prioritize site acceptance test points. Experimental results are presented on real application data for the yards in India that are demonstrating the performance of the proposed methods.

Circuits and systems that have to deal with real valued artifacts often need to be evaluated not only for correct behaviors, but also the margins by which they satisfy the design intent. Our definition of "features" formally extends the classical notion of "assertions" by overlaying constructs for specifying real valued functions over matches of assertions, thereby providing a powerful language framework for specifying real valued properties of the system. In this paper we present, for the first time, methods for formal evaluation of feature ranges on hybrid automata models which are extensively used for modeling switched control systems. We demonstrate the methodology over three case studies, namely a cruise control system, a DC-DC Buck Regulator and a Li-ion battery charger.

The acceptance criteria for analog designs are traditionally defined in terms of real-valued features defined over behavioral responses. For example, rise time, peak overshoot, and settling time are features of the response of a second-order system under a step input. Designers of analog and mixed-signal (AMS) designs typically like to see whether the relevant features lie within their specified ranges, and if so, by what margin. Assertions are capable of capturing the acceptance criteria, but they do not help in evaluating how well (or by what margin) the design satisfies the specification. We introduce the notion of Feature Indented Assertions (FIAs) for overlaying the definition of real-valued features over the syntactic fabric of AMS assertions. In this paper, we present the formal syntax and semantics of our language, FIA, and demonstrate its ability to capture a wide variety of AMS features. We present our dynamic feature evaluation tool that plugs into standard AMS simulators through Verilog Procedural Interfaces and evaluates features over simulation. At the heart of this tool, we have our interval arithmetic-based algorithm for monitoring features over continuous time and value domains. This algorithm is presented with corresponding proofs of correctness and with results over industrial testcases.

Automotive software applications implement a variety of control algorithms, with many of them being safety-critical in nature. A typical design flow starts with modeling these control algorithms using tools like MATLAB/Simulink. However, at this stage, a number of assumptions, like negligible sensor-to-actuator delay and instantaneous computation of the controller software, are often made. In particular, the details of the software implementation and the computing platform, both eventually defining the timing properties of the applications, are not accounted for. Such idealistic assumptions can cause a significant deviation of the control performance compared to what was proven at the modeling stage. This is usually addressed with multiple design iterations, which are costly and may lead to over-provisioned and thus poorly designed systems. In this paper we attempt to address this problem by proposing a design-and tool flow that integrates software-and platform-level timing information into the high-level modeling stage. We outline our proposed flow using concrete, industry-strength design tools.

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.

Simulation platforms for complex networked real time systems require random input pattern generators for simulating input distributions. They also require monitors for checking whether the output of the system satisfies the desired throughput. In this paper we study the acceptance and generation problems in a setting where the constraints defining the input distributions as well as the constraints defining the expected output distributions are specified in real time calculus (RTC). We prove that event patterns satisfying a given set of RTC constraints can be described by a ω-regular language. We propose a method for constructing an automaton that can be used for online generation of random admissible event patterns. This is significant, considering the known problems of deadlock in less informed generators for streams satisfying RTC constraints.

Abstract The design of a complex embedded control system involves integration of large number of components. These components need to interact in a timely fashion to achieve the system level end-to-end requirements. In practice, the component level timing specification consists of design attributes like component task mapping, task period and schedule definition but often lack details on their real-time (functional) requirements. As we observe, there is no systematic methodology in place for decomposing the feature level timing requirements into component level timing requirements. This paper proposes an early stagetime-budgeting methodologyto bridge the above gap. A salient proposal of this methodology is to considerparameterizedcomponent timing-requirements. A key step in the methodology involves computing a set of constraints by relating component requirements with feature requirements. This enables the separation of timing constraints from functionality decomposition, and facilitates early optimization of thecomponent time-budgetfor a complex component based embedded system. This paper formalizes the proposed methodology by using Parametric Temporal Logic. A case study involving two advanced features from the automotive domain, namely Adaptive Cruise Control and Collision Mitigation is given to demonstrate the methodology.

This paper reports for the first time, the use of a hardware-software combined bounded model checking approach for hardware-software mixed implementations of power management logic. We report significant performance gains as compared to our earlier attempt of extracting a finite quotient transition system from the control software.

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.

This paper presents a verification framework that attempts to bridge the disconnect between high-level properties capturing the architectural power management strategy and the implementation of the power management control logic using low-level per-domain control signals. The novelty of the proposed framework is in demonstrating that the architectural power intent properties developed using high-level artifacts can be automatically translated into properties over low-level control sequences gleaned from UPF specifications of power domains, and that the resulting properties can be used to formally verify the global on-chip power management logic. The proposed translation uses a considerable amount of domain knowledge and is also not purely syntactic, because it requires formal extraction of timing information for the low-level control sequences. We present a tool, called POWER-TRUCTOR which enables the proposed framework, and several test cases of significant complexity to demonstrate the feasibility of the proposed framework.

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.

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.

In this paper we consider finding solutions for problems represented using AND/OR graphs, which contain tasks that can fail when executed. In our setting each node represent an atomic task which is associated with a failure probability and a rollback penalty. This paper reports the following contributions - (a) an algorithm for finding the optimal ordering of the atomic tasks in a given solution graph which minimizes the expected penalty, (b) an algorithm for finding the optimal ordering in the presence of user defined ordering constraints, and (c) a counter example showing the lack of optimal substructure property for the problem of finding the solution graph having minimum expected penalty, and a pseudo-polynomial algorithm for finding the solution graph with minimum expected penalty.

We present algorithms for generating alternative solutions for explicit acyclic AND/OR structures in non-decreasing order of cost. The proposed algorithms use a best first search technique and report the solutions using an implicit representation ordered by cost. In this paper, we present two versions of the search algorithm -- (a) an initial version of the best first search algorithm, ASG, which may present one solution more than once while generating the ordered solutions, and (b) another version, LASG, which avoids the construction of the duplicate solutions. The actual solutions can be reconstructed quickly from the implicit compact representation used. We have applied the methods on a few test domains, some of them are synthetic while the others are based on well known problems including the search space of the 5-peg Tower of Hanoi problem, the matrix-chain multiplication problem and the problem of finding secondary structure of RNA. Experimental results show the efficacy of the proposed algorithms over the existing approach. Our proposed algorithms have potential use in various domains ranging from knowledge based frameworks to service composition, where the AND/OR structure is widely used for representing problems.

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.

Sampling has been one of the key issues in simulation-based verification of analog and mixed signal (AMS) systems. Recent attempts toward extending assertion languages to the AMS domain has brought forward an obvious question. In what way should sampling be done to ensure that assertions are evaluated correctly? Increasing sampling granularity often comes with substantial simulation time overhead. On the other hand, interpolation of the analog signals between consecutive samples introduces inaccuracies in the signal values and, hence, in the truth of the assertions. This paper explores how temporal assertions are handled for inadequately sampled signals. We propose a three-valued semantics (true, false, and unknown) for AMS assertions to address the uncertainty caused by the inadequacy of samples. The evaluation algorithm reports the time intervals where additional samples are required to resolve the uncertainty, thereby paving the way for adaptive sampling refinement in assertion aware AMS simulation.

There has been considerable focus recently on research on developing assertion checking capability with analog and mixed-signal (AMS) simulators. Such tools must be able to detect failures of assertions in simulation traces and report the windows in which failures have been detected. Due to the dense real time semantics of AMS assertions, the task of identifying the minimal debugging window for each failure is not a trivial problem. This paper addresses the problem of computing the minimal debugging window in failure traces for AMS assertions and presents an algorithm which is linear in regards to the size of the assertion and the size of the trace.

We present a symbolic-event-propagation-based scheme to generate hazard-free tests for robust path delay faults. This approach identifies all robustly testable paths in a circuit and the corresponding complete set of test vectors. We address the problem of finding a minimal set of test vectors that covers all robustly testable paths. We propose greedy and simulated-annealing-based algorithms to find the same. Results on ISCAS89 benchmark circuits show a considerable reduction in test vectors for covering all robustly testable paths.

The verification community anticipates the adoption of assertions in the Analog and Mixed-Signal (AMS) domain in the near future. Several questions need to be answered before AMS assertions are brought into practice, such as: (a) How will the languages for AMS assertions be different from the ones in the digital domain? (b) Does the analog simulator have to be assertion aware? (c) If so, then how and where on the time line will the AMS assertion checker synchronize with the analog simulator? and (d) What will be the performance penalty for monitoring AMS assertions accurately over analog simulation? This article attempts to answer these questions through theoretical analysis and empirical results obtained from industrial test cases. We study logics which extend Linear Temporal Logic (LTL) with predicates over real variables, and show that further extensions allowing the binding of real-valued variables across time makes the logic undecidable. We present a toolkit which can integrate with existing AMS simulators for checking AMS assertions on practical designs. We study the problem of synchronizing the AMS simulator with the AMS assertion checker and demonstrate the performance penalty of different synchronization options.

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.

Abstract In today's organizations, the large scale deployment of wireless networks has opened up new directions in network security management. The organizational security policies aim at protecting the network resources from unauthorized accesses in the wireless local area networks (WLAN). In WLAN security policy management, the standard IP‐based access control mechanisms are not sufficient due to dynamic changes in network topology and access control states. The role‐based access control (RBAC) models may be appropriate to strengthen the security perimeter over the network resources. However, formalizing the dynamic binding of the access policies to the roles, depending on various control states, is a major challenge. In this paper, we propose a WLAN security policy management framework based on a formalspatio‐temporal RBAC(STRBAC) model. The present work primarily focuses on dynamic computation of security policies based on various control states, its formal representation using STRBAC model, and security property verification of the proposed STRBAC model. The proposed policy management framework logically partitions the WLAN topology into various security policy zones. The framework includes aCentral Authentication & Role Server(CARS) which authenticates the users (nodes) and access points (AP) and also assigns appropriate roles to the users; aGlobal Policy Server(GPS) that dynamically computes the global security policy and policy configurations for different policy zones based on local user‐role and control state information; a distributed policy zone control architecture. Each policy zone consists of aPolicy Zone Controller(WPZCon) which dynamically computes the low‐level access configurations. Finally, a SAT based verification procedure has been presented for verifying the security properties of the proposed STRBAC model. Copyright © 2010 John Wiley & Sons, Ltd.

As research on developing assertion languages for the analog and mixed-signal (AMS) domain gains in momentum, it is increasingly being felt that extensions of existing assertion languages like property specification language and SystemVerilog assertions into the AMS domain are not adequate for expressing the analog design intent. This is largely due to the intricacy of the analog behavioral intent which cannot be captured purely in terms of logic. In this paper, we show that by using auxiliary forms of formal specifications such as abstract state machines and real-valued functions, called auxiliary functions, as references for AMS assertions, it becomes possible to model complex AMS behavioral properties. In addition, we present complexity results for the satisfiability problem of such specifications. This approach leverages the growing adoption of AMS behavioral modeling in the industry. This paper also shows that the use of auxiliary state machines allows us to separate out the scope of different analog assertions leading to significant performance gains in the assertion checking overhead.

Power Management Units (PMUs) are large integrated circuits consisting of many predesigned mixed-signal components. PMU integration poses a serious verification problem considering the size of the integrated circuit and the complexity of analog simulation. In this article we present an approach for automatic generation of behavioral models for PMU components from top-down skeleton models, fitted with parameter values estimated by bottom-up parameter extraction algorithms. It is shown that replacing PMU components with these autogenerated hybrid automata-based abstract behavioral models enables significant simulation speedup (> 20X on our industrial test cases) and helps in early detection of integration errors. The article also justifies the level of accuracy in our models with respect to the goal of verifying integrated PMUs. The approach presented in this work is implemented in the form of a tool suite called Chassis.

Recent research has indicated ways of using UPF specifications for extracting valid low-level control sequences to express the transitions between the power states of individual domains. Today there is a disconnect between the high-level architectural power management strategy which relates multiple power domains and these low-level assertions for controlling individual power domains. In this paper we attempt to bridge this disconnect by leveraging the low-level per-domain assertions for translating architectural power intent properties into global assertions over low-level signals. We show that the inter-domain properties created in this manner can be formally verified over the global power management logic.

The growing trend towards using component based design approach in embedded system development requires addressing newer system engineering challenges. These systems are usually time critical and require timing guarantees from components. The articulation of a desirable response bounds for the components is often ad-hoc and happens late in development. In this work, we present a formal methods based methodology for an early stage design space exploration. We focus on real-time response of a component as a basis for exploration and allow the developer model it using constant values or parameters. To quantify the parameters, we propose a novel constraint synthesis technique to correlate response times of interacting components. Finally, for system integration, we introduce a new notion of timing layout to specify time-budgeting for each component. The selection of a suitable layout can be made based on system optimization criteria. We have demonstrated our methodology on an automotive Adaptive Cruise Control feature.

In a typical enterprise network, correct implementation of security policies is becoming increasingly difficult owing to complex security constraints and dynamic changes in network topology. Usually, the network security policy is defined as the collection of service access rules between various network zones. The specification of the security policy is often incomplete since all possible service access paths may not be explicitly covered. This policy is implemented in the network interfaces in a distributed fashion through sets of access control (ACL) rules. Formally verifying whether the distributed ACL implementation conforms to the security policy is a major requirement. The complexity of the problem is compounded as some combination of network services may lead to inconsistent hidden access paths. Further, failure of network link(s) may result in the formation of alternative routing paths and thus the existing security implementation may defy the policy. In this study, an integrated formal verification and fault analysis framework has been proposed which derives a correct ACL implementation with respect to given policy specification and also ensures that the implementation is fault tolerant to certain number of link failures. The verification incorporates boolean modelling of the security policies and ACL implementations and then formulates a satisfiability checking problem.

In a typical enterprise network, there are several sub-networks or network zones corresponding to different departments or sections of the organization. These zones are interconnected through set of Layer-3 network devices (or routers). The service accesses within the zones and also with the external network (e.g., Internet) are usually governed by a enterprise-wide security policy. This policy is implemented through appropriate set of access control lists (ACL rules) distributed across various network interfaces of the enterprise network. Such networks faces two major security challenges, (i) conflict free representation of the security policy, and (ii) correct implementation of the policy through distributed ACL rules. This work presents a formal verification framework to analyze the security implementations in an enterprise network with respect to the organizational security policy. It generates conflict-free policy model from the enterprise-wide security policy and then formally verifies the distributed ACL implementations with respect to the conflict-free policy model. The complexity in the verification process arises from extensive use of temporal service access rules and presence of hidden service access paths in the networks. The proposed framework incorporates formal modeling of conflict-free policy specification and distributed ACL implementation in the network and finally deploys Boolean satisfiability (SAT) based verification procedure to check the conformation between the policy and implementation models.

Behavioral models for analog and mixed signal (AMS) designs are developed at various levels of abstraction, using various types of languages, to cater to a wide variety of requirements, ranging from verification, design space exploration, test generation, and application demonstration. In this paper we present a high-level formalism for capturing the AMS design intent from the specification and present techniques for automatic generation of AMS behavioral models. The proposed formalism is a language independent one, yet the design intent is modeled at a level of abstraction which enables easy translation into common modeling standards. We demonstrate the translation into VerilogA and SPICE, which are fundamentally different standards for behavioral modeling. The proposed approach is demonstrated using a family of Low Dropout Regulators (LDO) as the reference.

The industry trend appears to be moving towards designs that integrate large digital circuits with multiple analog/RF (radio frequency) interfaces. In the verification of these large integrated circuits, the number of nets that need to be monitored has been growing rapidly. Consequently, the mixed-signal design community has been feeling the need for AMS (Analog and Mixed Signal) assertions that can automatically monitor conformance with expected time-domain behavior and help in debugging deviations from the design intent. The main challenges in providing this support are (a) developing AMS assertion languages or AMS verification libraries, and (b) instrumenting existing commercial simulators to support assertion verification during simulation. In this article, we report two approaches: the first extends the Open Verification Library (OVL) to the AMS domain by integrating a new collection of AMS verification libraries; while the second extends SystemVerilog Assertions (SVA) by augmenting analog predicates into SVA. We demonstrate the use of AMS-OVL on the Cadence Virtuoso environment while emphasizing that our libraries can work in any environment that supports Verilog and Verilog-A. We also report the development of tool support for AMS-SVA using a combination of Cadence NCSIM and Synopsys VCS. We demonstrate the utility of both approaches on the verification of LP3918, an integrated power management unit (PMU) from National Semiconductors. We believe that in the absence of existing EDA (Electronic Design Automation) tools for AMS assertion verification, the proposed approaches of integrating our libraries and our tool sets with existing commercial simulators will be of considerable and immediate practical value.

Design intent coverage is a formal methodology for analyzing the gap between a formal architectural specification of a design and the formal functional specifications of the component RTL blocks of the design. In this article we extend the design intent coverage methodology to hybrid specifications containing both state-machines and formal properties. We demonstrate the benefits of this extension in two domains of considerable recent interest, namely (a) the use of auxiliary state-machines in formal specifications, and (b) the use of modest sized RTL blocks in the design intent coverage analysis.

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.

A satisfiability-based technique for symbolic modeling of event propagation in a circuit is presented in this paper which captures the events in the internal nodes of the circuit with a high level of detail. The model is used to accurately measure the peak single cycle transition power consumption in combinational and sequential circuits, which is closely affected by the switching activity in the circuit. Our technique is scalable, and adapts easily to ever increasing sizes of the custom cells (building blocks) in today's industry, without compromising on accuracy and correctness.

A SAT-based modeling for event propagation in gate-level digital circuits, which is used for accurate calculation of critical delay in combinational and sequential circuits, is presented in this article. The accuracy of the critical delay estimation process depends on the accuracy with which the circuit in operation is modeled. A high level of precision in the modeling of the internal events in a circuit for the sake of greater accuracy causes a combinatorial blowup in the size of the problem, resulting in a scalability bottleneck for which most existing techniques effect a trade-off by restricting themselves to less precise models. SAT based techniques have a good track record in efficiency and scalability when the problem sizes become too large for most other methods. This article proposes a SAT-based technique for symbolic event propagation within a circuit which facilitates the estimation of the critical delay of circuits with a greater degree of accuracy, while at the same time scaling efficiently to large circuits. We report very encouraging results on the ISCAS85 and ISCAS89 benchmark circuits using the proposed technique.

The design of a large chip is typically hierarchical - large modules are recursively expanded into a collection of sub-modules. Each expansion refines the design due to the addition of level specific details. We believe that a similar approach is necessary to scale the capacity of formal property verification technology - as the design gets refined from one level to another, the formal specification must also be refined to reflect the level specific design decisions. At the heart of this approach we propose a checker that identifies the input assumptions under which the refined specification "covers" the original specification. This enables the validation engineer to focus the verification effort on the remaining input scenarios thereby reducing the number of target coverage points for simulation.

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.

Practitioners of formal property verification often work around the capacity limitations of formal verification tools by breaking down properties into smaller properties that can be checked on the sub-modules of the parent module. To support this methodology, we have developed a formal methodology for verifying whether the decomposition is indeed sound and complete, that is, whether verifying the smaller properties on the submodules actually guarantees the original property on the parent module. In practice, however designers do not write properties for all modules and thereby our previous methodology was applicable to selected cases only. In this paper we present new formal methods that allow us to handle RTL blocks in the analysis. We believe that the new approach will significantly widen the scope of the methodology, thereby enabling the validation engineer to handle much larger designs than admitted by existing formal verification tools

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

Formal property verification is increasingly being adopted by designers for module level validation. The behavior of a module is typically expressed in terms of the behavioral guarantee of the module under assumptions on its environment. Expressing such assume-guarantee properties correctly in a formal language is a nontrivial task and errors in the specification are not uncommon. In this paper we examine the main forms of specification errors for open systems, and present SAT based algorithms for verifying the specification against such errors.

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.

It is essential to formally ascertain whether the 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 limitation 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. In this paper we present: (1) a method for checking whether the RTL-properties are covering the architectural-properties, that is, whether verifying the RTL-properties guarantee the correctness of the design's architectural intent; and (2) a method to identify the coverage holes in terms of the architectural properties (or their sub-properties) that are not covered.

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...

Presents a framework for efficiently solving logic formulations of combinatorial optimization problems using heuristic search techniques. In order to integrate cost, lower-bound and upper-bound specifications with conventional logic programming languages, we augment a constraint logic programming (CLP) language with embedded constructs for specifying the cost function and with a few higher-order predicates for specifying the lower and upper bound functions. We illustrate how this simple extension vastly enhances the ease with which optimization problems involving combinations of Min and Max can be specified in the extended language CLP* and we show that CSLDNF (Constraint SLD resolution with Negation as Failure) resolution schemes are not efficient for solving optimization problems specified in this language. Therefore, we describe how any problem specified using CLP* can be converted into an implicit AND/OR graph, and present an algorithm called GenSolve which can branch-and-bound using upper and lower bound estimates, thus exploiting the full pruning power of heuristic search techniques. A technical analysis of GenSolve is provided. We also provide experimental results comparing various control strategies for solving CLP* programs.

RTL descriptions for word-level arithmetic components typically specify the architecture at the bit-level of the registers. The problem studied in this paper is to abstract the word-level functionality of a component from its bit-level specification. This is particularly useful in simulation since word-level descriptions can be simulated much faster than bit-level descriptions. Word-level abstractions are also useful for reducing the complexity of component matching since the number of words is significantly smaller than the number of bits. This paper presents an algorithm for abstraction of word-level linear functions from bit-level component descriptions. We also present complexity results for component matching which justifies the advantage of performing abstraction prior to component matching.

We propose a new style of model checking of timed transition systems, where instead of reasoning about the timing of states with specific properties, we reason about the timings of events with specific properties. This shift in paradigm appears to be useful for verification of edge triggered control paths, where we are more interested in the timings of changes in signal values. We propose a temporal logic, event-triggered timed computation tree logic (ETCTL), which allows the specification of event properties such as posedge(signal) and negedge(signal) along with real time computation tree logic (RTCTL) properties. We show that all ETCTL properties are interval independent, that is, their truth can never change on states between successive events. By virtue of the interval independent property, reasoning about timings of events (using ETCTL) is more efficient computationally than reasoning about general timed properties. We present a labeling algorithm, and suggest extensions to automata theoretic and symbolic approaches.