Developing functional test programs for hardware testing is time-consuming and experience-wise. A functional test program’s quality is usually assessed only through expensive fault simulation campaigns during early development. This paper presents indirect quality measurements of fault detection capabilities of functional test programs to reduce the total cost of fault simulation in the early development stages. We present a methodology that analyzes the instruction trace generated by running functional test programs on-chip and building its control and dataflow graph. We use the graph to identify potential flaws that affect the program’s fault detection capabilities. We present different graph-based techniques to measure the programs’ quality indirectly. By exploiting standard debugging formats, we individuate instructions in the source code that affect the graph-based measurements. We perform experiments on an automotive device manufactured by STMicroelectronics, running functional test programs of different natures. Our results show that our metric allows test engineers to develop better functional test programs without basing their development solely on fault simulation campaigns.

The in-circuit test checks whether the board’s electrical and electronic components have been correctly soldered when producing printed circuit boards. When such a test is performed using a flying-probe tester, the cost of testing is mainly related to the time required for moving probes over the board and the time necessary for defining such movements, tuning the optimization on the number of devices that will eventually be tested. Since the 2000s, flying probe testing has been gaining popularity. Still, despite its industrial relevance, the research has been impaired by the lack of publicly available benchmarks for testing the new algorithms and comparing the different ideas. This paper presents an open test set of realistic boards, ranging from a few thousand to half a million test points, together with a tool for generating more samples. It also presents an optimizer for flying probe tests composed of two separate planners: one global detecting test that could be performed together and reordered to obtain a more efficient probing sequence, and one local, implementing the probe movements and taking care of specific board features. The test set will eventually be used to present a quantitative evaluation of the performance of the proposed approach.

Precise residential load modeling is indispensable for crafting effective demand-side management strategies and simulating realistic household power consumption under diverse conditions. This paper introduces a novel generative framework, leveraging the power of Generative Adversarial Networks (GANs), to synthesize highly realistic daily activity patterns. By training on detailed Italian time-use data, the model captures nuanced behavioral statistics, reflecting the inherent variability of human routines. Furthermore, incorporating conditional generation based on the day of the week allows for contextually rich and adaptable simulations, capturing weekly lifestyle variations. Household power profiles are reconstructed by meticulously mapping the generated activities to the characteristic power signatures of common household appliances, resulting in simulations that exhibit strong concordance with empirical load data at both granular, appliance-level, and aggregated household levels. Critically, our GAN-based approach demonstrably accelerates simulation throughput compared to conventional Markov chain methodologies, enabling the efficient and scalable analysis of complex residential energy scenarios, and opening avenues for real-time applications and large-scale urban energy studies.

In recent years, there has been an exponential growth in the size and complexity of System-on-Chip (SoC) designs targeting different specialized applications. The cost of an undetected bug in these systems is much higher than in traditional processors, as it may imply loss of property or life. Despite decades of research on simulation and formal methods for debugging and verification, the problem is exacerbated by the ever-shrinking time-to-market and ever-increasing demand to churn out billions of devices. In this work, we propose VeriBug, which leverages recent advances in deep learning (DL) to accelerate debugging at the Register-Transfer level (RTL) and generates explanations of likely root causes. Our experiments show that VeriBug can achieve an average bug localization coverage of 82.5% on open-source designs and a wide variety of injected bugs.

Low-cost light-scattering particulate matter sensors are often advocated for dense monitoring networks. Recent literature has focused on evaluating their performance. Nonetheless, low-cost sensors are also considered unreliable and imprecise. Consequently, exploring techniques for anomaly detection, resilient calibration, and improvement of data quality should be more discussed. In this study, we analyze a year-long acquisition campaign by positioning 56 low-cost light-scattering sensors near the inlet of an official particulate matter monitoring station. We use the collected measurements to design and test a data processing pipeline composed of different stages, including fault detection, filtering, outlier removal, and calibration. These can be used in large-scale deployment scenarios where the quantity of sensors data can be too high to be analyzed manually. Our framework also exploits sensor redundancy to improve reliability and accuracy. Our results show that the proposed data processing framework produces more reliable measurements, reduces errors, and increases the correlation with the official reference.

In smart grids, consumers can be involved in demand response programs to reduce the total power consumption of their households during the peak hours of the day. Unfortunately, nowadays, utility companies are facing important challenges in the implementation of demand response programs because of their negative impact on the comfort of end-users. In this article, we cluster the different operation modes of household appliances based on the analysis of their power signatures. For this purpose, we implement an autoencoder neural network to create a better data representation of the power signatures. Then, we cluster the different operational programs by using aK-means algorithm fitted to the new data representation. To test our methodology, we study the operation modes of some washing machines and dishwashers whose power signatures were derived from both submeters and nonintrusive load monitoring techniques. Our clustering analysis reveals the existence of multiple working programs showing well-defined features in terms of both average energy consumption and duration. Our results can then be used to improve demand response programs by reducing their impact on the comfort of end-users. Furthermore, end-users can rely on our framework to favor lighter operation modes and reduce their overall energy consumption.

Testing and validation check a hardware device or a software application against the desired design requirements. They are a vital part of all steps of system engineering and typically account for a significant percentage of the overall development cost. This paper presents a novel technique to provide a quick preliminary evaluation of functional test procedures of various natures, ranging from Software-Based Self-Test to Burn-In Functional Stress and System-level tests. We define a new metric called “connectivity”, which is fast to compute and can be used to guide functional program development. The method does not require logic or fault simulations, and it is based on the analysis of the execution trace generated by the functional program. To summarize our process, we first obtain the trace directly from the chip, running the software through a debugger. Then, we create a graph representation of the program data flow. Finally, we analyze the graph to identify instructions that negatively impact the final coverage. We perform experiments on an automotive device manufactured by STMicroelectronics, and we demonstrate the effectiveness of the approach in terms of computation time and beneficial effects on the fault coverage.

Electric infrastructures have been pushed forward to handle tasks they were not originally designed to perform. To improve reliability and efficiency, state-of-the-art power grids include improved security, reduced peak loads, increased integration of renewable sources, and lower operational costs. In this framework, “smart grids” are built around bidirectional communication technologies, where “smart meters” communicate with all other entities and collect data from the power grid, offering specific features to each actor playing in the energy marketplace. In this article, to overcome some of the challenges raised by smart grids and smart meters, we propose a distributed metering infrastructure, which provides bidirectional communication, self-configuration, and autoupdate capabilities. Our 3-phase smart meters follow the basics Internet of Things principles and have the ability to run, either onboard or distributed on the network, multiple algorithms for smart grid management. These algorithms can be freely added, updated, or removed on the fly, thanks to the autoupdate feature of the system. Moreover, to reduce costs and improve scalability, we prove that it is possible to implement our smart meters using only off-the-shelf and inexpensive hardware devices. A digital real-time simulator (i.e., Opal-RT) has been used to assess the capabilities of both the infrastructure and the meter. Our experimental analysis shows that the latency introduced by the data transmission over the Internet is compliant with the limits imposed by the IEC 61850 standard. As a consequence, our architecture does not affect the operational status of the smart grid, making it a viable solution to support the deployment of novel services.

With the explosion of off-the-shelf SoCs in terms of size and the advent of novel techniques related to failure modes, commercial ATPG and fault simulation engines can often be insufficient to measure the coverage of very specific metrics. In these cases, many researchers firstly store the simulation trace during the analysis phase. Then, they collect the desired statistics during a post-processing step. In this framework, the so-called Value Change Dump (VCD) is a very commonly used file format to record simulation traces. The target of this paper is twofold. From the one hand, we illustrate some Burn-In (BI) related metrics which cannot be evaluated by current commercial fault simulators and ATPG engines. These metrics are indeed based on a post-processing analysis of memory dumps in VCD format. From the other hand, we mitigate the evaluation time and the memory required to analyze huge VCD files by exploiting optimization techniques coming from modern programming features and smart parallelization. Adopting this strategy, we can analyze simulation dumps of more than 250 GBytes in less than one hour, showing improvements of two orders of magnitude over previous tools, with a consequent higher scalability and testability power.

This paper presents a simple 7/2-approximation algorithm for the Maximum Duo-Preservation String Mapping (MPSM) problem. This problem is complementary to the classical and well studied min common string partition problem (MCSP), that computes the minimal edit distance between two strings when the only operation allowed is to shift blocks of characters. The algorithm improves on the previously best-known 4-approximation algorithm by computing a simple local optimum.

In order to make model checking applicable to realistic problems, simplification techniques are essential. Models may be simplified eliminating the variables that do not appear in the cone-of-influence (COI) of the properties under verification. Efficient COI computation is thus required. Algorithms based on depth-first visits may become cumbersome when they must be applied several times; for instance, when multiple properties must be verified on the same model. An alternative is to resort to graph-labeling methods, trading-off time for memory. Modeling the problem in terms of graphs, this paper develops a technique based on bitmaps that keeps the amount of memory needed within acceptable limits. The paper also describes a portfolio of optimizations of the original algorithm that allow even more reductions in memory usage. Experimental results show that the basic algorithm and its optimized versions perform very well on standard benchmark circuits used in the model-checking community. Copyright © 2015 John Wiley & Sons, Ltd.

In the framework of symbolic model checking, BDD-based approximate reachability is potentially much more scalable than its exact counterpart. However, its practical applicability is highly limited by its static approach to abstraction, and the intrinsic difficulty to find an acceptable trade-off between accuracy and memory/time complexity. In this paper, we apply SAT-based cube generalization, a core step of the IC3 model checking algorithm, to BDD-based over-approximate reachability analysis. More specifically, we use cube generalization, in both its inductive and non-inductive versions, to tighten BDD-based over-approximate representations of state sets computed by Machine by Machine (MBM) and Frame by Frame (FBF) algorithms. The resulting approach benefits from the orthogonal power of BDD and CNF representations, and it improves the scalability and applicability in verification of BDD-based methods. Experimental results confirm that this approach can provide tighter representations of reachable state sets and more powerful fully BDD-based engines, as well as potential applications of BDDs as invariants or constraints in SAT-based model checking.

This paper introduces a new technique for a fast computation of the Cone-Of-Influence (COI) of multiple properties. It specifically addresses frameworks where multiple properties belongs to the same model, and they partially or fully share their COI. In order to avoid multiple repeated visits of the same circuit sub-graph representation, it proposes a new algorithm, which performs a single topological visit of the variable dependency graph. It also studies mutual relationships among different properties, based on the overlapping of their COIs. It finally considers state variable scoring, based on their own COIs and/or their appearance in multiple COIs, as a new statistic for variable sorting and grouping/clustering in various Model Checking algorithms. Preliminary results show the advantages, and potential applications of these ideas.

This article describes a multithreaded, portfolio-based approach to model checking, where multiple cores are exploited as the underlying computing framework to support concurrent execution of cooperative engines. We introduce a portfolio-based approach to model checking. Our portfolio is first driven by an approximate runtime predictor that provides a heuristic approximation to a perfect oracle and suggests which engines are more suitable for each verification instance. Scalability and robustness of the overall model-checking effort highly rely on a concurrent, multithreaded model of execution. Following similar approaches in related application fields, we dovetail data partitioning, focused on proving several properties in parallel, and engine partitioning, based on concurrent runs of different model-checking engines competing for completion of the same problem. We investigate concurrency not only to effectively exploit several available engines, which operate independently, but also to show that a cooperative effort is possible. In this case, we adopt a straightforward, light-weight, model of inter-engine communication and data sharing. We provide a detailed description of the ideas, algorithms, and experimental results obtained on the benchmarks from the Hardware Model Checking Competition suites (HWMCC'10 and HWMCC'11).

This work revisits the formulation of interpolation sequences, in order to better understand their relationships with Bounded Model Checking and with other Unbounded Model Checking approaches relying on standard interpolation. We first focus on different Bounded Model Checking schemes (bound, exact and exact-assume), pointing out their impact on the interpolation-based strategy. Then, we compare the abstraction ability of interpolation sequences with standard interpolation, highlighting their convergence at potentially different sequential depths. We finally propose a tight integration of interpolation sequences with an abstraction-refinement strategy. Our contributions are first presented from a theoretical standpoint, then supported by experimental results (on academic and industrial benchmarks) adopting a state-of-the-art academic tool.

Interpolant-based model checking has been shown to be effective on large verification instances, as it efficiently combines automated abstraction and reachability fixed-point checks. On the other hand, methods based on variable quantification have proved their ability to remove free inputs, thus projecting the search space over state variables. In this paper, we propose an integrated approach which combines the abstraction power of interpolation with techniques that rely on and-inverter graph (AIG) and/or binary decision diagram (BDD) representations of states, directly supporting variable quantification and fixed-point checks. The underlying idea of this combination is to adopt AIG or BDD-based quantifications to limit and restrict the search space and the complexity of the interpolant-based approach. The exploited strategies, most of which are individually well known, are integrated with a new flavor, specifically designed to improve their effectiveness on difficult verification instances. Experimental results, specifically oriented to hard-to-solve verification problems, show the robustness of our approach.

The task graph cost-optimal scheduling problem consists in scheduling a certain number of interdependent tasks onto a set of heterogeneous processors (characterized by idle and running rates per time unit), minimizing the cost of the entire process. This paper provides a novel formulation for this scheduling puzzle, in which an optimal solution is computed through a sequence of binate covering problems, hinged within a bounded model checking paradigm. In this approach, each covering instance, providing a min-cost trace for a given schedule depth, can be solved with several strategies, resorting to minimum-cost satisfiability solvers or pseudo-Boolean optimization tools. Unfortunately, all direct resolution methods show very low efficiency and scalability. As a consequence, we introduce a specialized method to solve the same sequence of problems, based on a traditional all-solution SAT solver. This approach follows the “circuit cofactoring” strategy, as it exploits a powerful technique to capture a large set of solutions for any new SAT counter-example. The overall method is completed with a branch-and-bound heuristic which evaluates lower and upper bounds of the schedule length, to reduce the state space that has to be visited. Our results show that the proposed strategy significantly improves the blind binate covering schema, and it outperforms general purpose state-of-the-art tools.

Constraints represent a key component of state-of-the-art verification tools based on compositional approaches and assume-guarantee reasoning. In recent years, most of the research efforts on verification constraints have focused on defining formats and techniques to encode, or to synthesize, constraints starting from the specification of the design. In this paper, we analyze the impact of constraints on the performance of model checking tools, and we discuss how to effectively exploit them. We also introduce an approach to explicitly derive verification constraints hidden in the design and/or in the property under verification. Such constraints may simply come from true design constraints, embedded within the properties, or may be generated in the general effort to reduce or partition the state space. Experimental results show that, in both cases, we can reap benefits for the overall verification process in several hard-to-solve designs, where we obtain speed-ups of more than one order of magnitude.

This paper describes optimized techniques to efficiently compute and reap benefits from inductive invariants within satisfiability (SAT)-based model checking. We address sequential circuit verification and consider both equivalences and implications between pairs of nodes in the logic networks. First, we present a very efficient dynamic procedure, based on equivalence classes and incremental SAT, specifically oriented to reduce the set of checked invariants. Then, we show how to effectively integrate the computation of inductive invariants within state-of-the-art SAT-based model-checking procedures. Experiments (on more than 600 designs) show the robustness of our approach on verification instances on which stand-alone techniques fail.

Interpolant-based model checking has been shown effective on large verification instances, as it efficiently combines automated abstraction and fixed-point checks. On the other hand, methods based on variable quantification have proved their ability to remove free inputs, thus projecting the search space over state variables. In this paper we propose an integrated approach combining the abstraction power of interpolation with techniques relying on AIG and/or BDD representations of states, supporting variable quantification and fixed-point checks. The underlying idea of this combination is to adopt AIG- or BDD-based quantifications to limit and restrict the search space (and the complexity) of the interpolant-based approach. The exploited strategies, individually well-known, are integrated with a new flavor, specifically designed to improve their effectiveness on large verification instances. Experimental results, oriented to hard-to-solve verification problems, show the robustness of our approach.

SAT--based Unbounded Model Checking based on Craig Interpolants is often able to overcome BDDs and other SAT--based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, as they abstract away several nonrelevant details of the proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant--based dynamic abstraction to reduce the support of computed interpolants. Subsequently, we propose new advances in interpolant compaction by redundancy removal. Finally, we introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. These techniques heavily rely on an effective application of the incremental SAT paradigm. The experimental results proposed in this paper are specifically oriented to prove properties, rather than disproving them, i.e., they target complete verification instead of simply hunting bugs. They show how this methodology is able to stretch the applicability of interpolant--based Model Checking to larger and deeper verification instances.

This paper addresses SAT-based Unbounded Model Checking based on Craig Interpolants. This recently introduced methodology is often able to outperform BDDs and other SAT-based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, and abstract away several details non relevant for proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant-based dynamic abstraction to reduce the support of the computed interpolant. Second, we propose new advances in interpolant compaction by redundancy removal. Both techniques rely on an effective application of the incremental SAT paradigm. Finally, we also introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. Experimental results are specifically oriented to prove properties, rather than disproving them (bug hunting). They show how the methodology is able to extend the applicability of interpolant based Model Checking to larger and deeper verification instances.

A non-canonical circuit-based state set representation is used to perform quantifier elimination efficiently. The novelty of this approach lies in adapting equivalence checking and logic synthesis techniques to the goal of compacting circuit based state set representations resulting from existential quantification. The method can be efficiently combined with other verification approaches such as inductive and SAT-based pre-image verifications.

The usefulness of Bounded Model Checking (BMC) based on propositional satisfiability (SAT) methods has recently proven its efficacy for bug hunting. BDD based tools are able to verify broader sets of properties (e.g. CTL formulas) but recent experimental comparisons between SAT and BDDs in formal verification lead to the conclusion that SAT approaches are more robust and scalable than BDD techniques.In this work we extend BDD-based verification to larger circuit and problem sizes, so that it can indeed compete with SAT based tools. The approach we propose solves Bounded Model Checking problems using BDDs. In order to cope with larger models it exploits approximate traversals, yet it is exact, i.e. it does not produce false negatives or positives. It reaps relevant performance enhancements from mixed forward and backward, approximate and exact traversals, guided search, conjunctive decompositions and generalized cofactor based BDD simplifications.We experimentally compare our tool with BMC in NuSMV using mchaff as SAT engine, and we show that BDDs are able to accomplish large verification tasks, and they can better cope with increasing sequential depths.

The core computation in BDD-based symbolic synthesis and verification is forming the image and pre-image of sets of states under the transition relation characterizing the sequential behavior of the design. Computing an image or a pre-image consists of ordering the latch transition relations, clustering them and eventually re-ordering the clusters. Existing algorithms are mainly limited by memory resources. To make them as efficient as possible, we address a set of heuristics with the main target of minimizing the memory used during image computation. They include a dynamic heuristic to order the latch relations, a dynamic framework to cluster them, and the application of conjunctive partitioning during image computation. We provide and integrate a set of algorithms and we report references and comparisons with recent work. Experimental results are given to demonstrate the efficiency and robustness of the approach.

We address BDD based reachability analysis, which is the core technique of symbolic sequential verification and Model Checking. Within this framework, non purely breadth-first and guided traversals have shown their value to improve efficiency by reducing memory consumption for BDD representation. We propose a guided search strategy exploiting performance statistics. These activity figures are gathered through a continuous and dynamic learning process on a variable-by-variable basis. This technique is currently integrated with the reachability analysis routine, as it is fully compatible with dynamic reordering and allows multiple partial traversal phases. We thus move away from the static and manual schemes, which are one of the main limitations of previous approaches. Experiments are given to demonstrate the efficiency and robustness of the approach.

Sequential verification methods based on reachability analysis are still limited by the size of the BDDs involved in computations. Extending their applicability to larger and real circuits is still a key issue. Within this framework, we explore a new way to improve symbolic traversal performance, working on the representation of state sets. We exploit retiming to reduce the number of latches of a FSM, and to relocate them in order to obtain a simplified state set representation. We consider retiming as a temporary state space transformation to increase the efficiency of sequential verification. We discuss it as a state space transformation and we formally analyze the conditions under which such a transformation is equivalence preserving for a given property under verification. We lower image computation cost, and we reduce the size of BDDs representing intermediate results and state sets. Experimental results show considerable memory and time improvements on some benchmark and home made circuits. 1

Symbolic techniques have undergone major improvements in the last few gears. Nevertheless, applications are still limited by memory size and time constraints. As a consequence, extending their applicability to larger and real circuits is still a key issue. Within this framework, we introduce "activity profiles" as a novel technique to characterize finite state machines described by their transition relation. In our methodology, a "learning phase" is used to collect activity measures. They are gathered, in an inexpensive way, for each binary decision diagram node of the transition relation. They indicate the activity the node has been involved in, as an estimate of its correlation with space and/or time costs. The above information can be used for several purposes. In particular, we present an application of activity profiles in the field of reachability analysis, to enhance memory and time performance of traversals. More specifically, we use transition relation subsetting in order to traverse the state transition graph in a nonpurely breadth-first, guided and multistep fashion. Comparisons with other state-of-the-art approaches show that our sequence of partial traversals produces "best-ever" results for all the large benchmarks analyzed.

Symbolic methods are often considered the state-of-the-art technique for validating digital circuits.Due to their complexity and unpredictable run-time behavior, however, their potential is currently limited to small-to-medium circuits.Logic simulation privileges capacity, it is nicely scalable, flexible, and it has a predictable run-time behavior.For this reason, it is the common choice for validating large circuits.Simulation, however, typically visits only a small fraction of the state space: The discovery of bugs heavily relies on the expertise of the designer of the test stimuli.In this paper we consider a symbolic simulation approach to the validation problem.Our objective is to trade-off between formal and numerical methods in order to simulate a circuit with a "very large number" of input combinations and sequences in parallel.We demonstrate larger capacity with respect to symbolic techniques and better efficiency with respect to cycle-based simulation.We show that it is possible to symbolically simulate very large trace sets in parallel (over 100 symbolic inputs) for the largest ISCAS benchmark circuits, using 96Mbytes of memory.

Symbolic techniques have undergone major improvements in the last few years.Nevertheless they are still limited by the size of the involved BDDs, and extending their applicability to larger and real circuits is a key issue.Within this framework, we introduce "activity profiles" as a novel technique to characterize transition relations.In our methodology a learning phase is used to collect activity measures, related to time and space cost, for each BDD node of the transition relation.We use inexpensive reachability analysis as learning technique, and we operate within inner steps of image computations involving the transition relation and state sets.The above informations can be used for several purposes.In particular, we present an application of activity profiles in the field of reachability analysis itself.We propose transition relation subsetting and partial traversals of the state transition graph.We show that a sequence of partial traversals is able to complete a reachability analysis problem with smaller memory requirement and improved time performance.

In this paper we address the problem of computing silent paths in an Finite State Machine (FSM). These paths are characterized by no observable activity under constant inputs, and can be used for a variety of applications, from verification, to synthesis, to simulation. First, we describe a new approach to compute the Timed Transition Relation of an FSM. Then, we concentrate on applying the methodology to simulation of reactive behaviours. In this field, we automatically extract a BDD-based behavioral model from the RT or gate level description. The behavioral model as able to "jump" in time and to avoid the simulation of internal events. Finally, we discuss a set of promising experimental results in a simulation environment under the Ptolemy simulator.

Binary decision diagrams (BDD's) are a state-of-the-art core technique for the symbolic representation and manipulation of Boolean functions, relations and finite sets. Many computer-aided design (CAD) applications resort to them, but size and time efficiency restrict their applicability to medium-small designs. We concentrate on complex operators used in symbolic manipulation. We analyze and optimize their performance by means of new dynamic partitioning strategies. We propose a novel quick algorithm for the estimation of cofactor size, and a technique to choose splitting variables according to their discrimination power, so that their cofactors may be optimized by different variable orderings (tending to the more flexible FBDDs). Furthermore, we analyze time efficiency and the impact of hashing/caching on BDD-based operators. We finally include an experimental observation of memory usage and running time for operators applied in symbolic manipulation.

Binary Decision Diagrams (BDDs) are the state-of-the-art technique for many synthesis, verification and testing problems in CAD for VLSI. Many researchers proposed optimized BDD—based representations, but in many complex applications the (working) memory required is still too much. Virtual memory is no alternative solution, because if the working set size for a program is large and memory accesses are random, an extremely large number of page faults significantly modifies the performance of the software. This paper proposes a solution to this problem for a specific application, namely BDD—based exploration of large state spaces, an issue often found in CAD for VLSI. Our ‘divide—and—conquer’ approach for reachability analysis is based on decomposition of state sets carried out at different levels and on an effective use of mass memory. As a result, we are able to explore the state space of large Finite State Machines. At the same time, the technique we develop is orthogonal to a variety of symbolic techniques and graph manipulation procedures and it allows reducing complexity of very common operations. Experimental results, on well known synchronous benchmarks usually used in the field of CAD for VLSI, show that this approach is particularly effective on larger problems as decomposition decreases the amount of working memory, avoids page faulting and makes the overall process more efficient. © 1998 John Wiley & Sons, Ltd.

BDDs are the state-of-the-art technique for representing and manipulating Boolean functions. Their introduction caused a major leap forward in synthesis, verification, and testing. However, they are often unmanageable because of the large amount of nodes. To attack this problem, we insert auxiliary variables that decompose monolithic BDDs in smaller ones. This method works very well for Boolean function representation. As far as combinational circuits are concerned, representing their functions is the main issue. Going into the sequential domain, we focus on traversal techniques. We show that, once we have Boolean functions in decomposed form, symbolic manipulations are viable and efficient. We investigate the relation between auxiliary variables and static and dynamic ordering strategies. Experimental evidence shows that we achieve a certain degree of independence from variable ordering. Thus, this approach can be an alternative to dynamic re-ordering. Experimental results on Boolean function representation, and exact and approximate forward symbolic traversal of FSMs, demonstrate the benefits both in terms of memory requirements and of CPU time.

This paper presents a solution to the problem of reducing the power dissipated by a digital system containing an intellectual proprietary core processor which repeatedly executes a special-purpose program. The proposed method relies on a novel, application-dependent low-power address bus encoding scheme. The analysis of the execution traces of a given program allows an accurate computation of the correlations that may exist between blocks of bits in consecutive patterns; this information can be successfully exploited to determine an encoding which sensibly reduces the bus transition activity. Experimental results, obtained on a set of special-purpose applications, are very satisfactory; reductions of the bus activity up to 64.8% (41.8% on average) have been achieved over the original address streams. In addition, data concerning the quality and the performance of the automatically synthesized encoding/decoding circuits, as well as the results obtained for a realistic core-based design, indicate the practical usefulness of the proposed power optimization strategy.

Extending the applicability of reachability analysis to large andreal circuits is a key issue.In fact they are still limited forthe following reasons: peak BDD size during image computation,BDD explosion for representing state sets and very highsequential depth.Following the promising trend of partitioning and problem decomposition,we present a new approach based on a disjunctivepartitioned transition relation and on an improved iterativesquaring.In this approach a Finite State Machine is decomposedand traversed one "functioning-mode" at a time bymeans of the "disjunctive" partitioned approach.The overall algorithm aims at lowering the intermediate peakBDD size pushing further reachability analysis.Experimentson a few industrial circuits containing counters and on somelarge benchmarks show the feasibility of the approach.

Article Free Access Share on System-level power optimization of special purpose applications: the beach solution Authors: Luca Benini Stanford University, Computer Systems Laboratory, Stanford, CA Stanford University, Computer Systems Laboratory, Stanford, CAView Profile , Giovanni De Micheli Stanford University, Computer Systems Laboratory, Stanford, CA Stanford University, Computer Systems Laboratory, Stanford, CAView Profile , Enrico Macii Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy 10129 Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy 10129View Profile , Massimo Poncino Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy 10129 Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy 10129View Profile , Stefano Quer Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy 10129 Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy 10129View Profile Authors Info & Claims ISLPED '97: Proceedings of the 1997 international symposium on Low power electronics and designAugust 1997 Pages 24–29https://doi.org/10.1145/263272.263277Published:01 August 1997Publication History 33citation259DownloadsMetricsTotal Citations33Total Downloads259Last 12 Months17Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

BDD-based symbolic traversals are the state-of-the-art technique for reachability analysis of finite state machines. They are currently limited to medium-small circuits for two reasons: peak BDD size during image computation and BDD explosion for representing state sets. Starting from these limits, this paper presents can optimized traversal technique particularly oriented to the exact exploration of the state space of large machines. This is possible thanks to: temporary simplification of a finite state machine by removing some of its state elements; and a "divide-and-conquer" approach based on state set decomposition. An effective use of secondary memory allows us to store relevant portions of BDDs and to regularize access to memory, resulting in less page faults. Experimental results show that this approach is particularly effective on the larger ISCAS'89 and ISCAS'89-addendum'93 circuits.

Synthesis and optimization of large finite-state machines has improved dramatically over the last few years with the introduction and rapid improvement of symbolic-state manipulation techniques. The algorithms efficiently visit each reachable state in the machine while computing and storing information about these states. We propose a new technique for improving the efficacy of traversal algorithms: re-encoding the states of the machine to more efficiently represent state sets or state transitions, or to more efficiently compute the next set of states. Our technique can be embedded in existing traversal algorithms. Experiments reveal that re-encoding can indeed reduce the time and/or space required for traversal.

Article Free Access Share on Auxiliary variables for extending symbolic traversal techniques to data paths Authors: Gianpiero Cabodi Politecnico di Torino, Dipartimento di Automatica e Informatica, Turin, Italy Politecnico di Torino, Dipartimento di Automatica e Informatica, Turin, ItalyView Profile , Paolo Camurati Politecnico di Torino, Dipartimento di Automatica e Informatica, Turin, Italy Politecnico di Torino, Dipartimento di Automatica e Informatica, Turin, ItalyView Profile , Stefano Quer Politecnico di Torino, Dipartimento di Automatica e Informatica, Turin, Italy Politecnico di Torino, Dipartimento di Automatica e Informatica, Turin, ItalyView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 289–293https://doi.org/10.1145/196244.196380Published:06 June 1994Publication History 5citation122DownloadsMetricsTotal Citations5Total Downloads122Last 12 Months4Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Symbolic state space traversal techniques are best on control-dominated circuits, not on data paths. This paper extends their applicability to regular structures commonly found in data paths by using auxiliary variables to decompose and to manipulate Boolean functions in decomposed form. Experimental results demonstrate the gain both in terms of binary decision diagram (BDD) size and CPU time.>

Most symbolic state space exploration techniques for finite state machines (FSMs) are exact and based on forward traversal, but limited to medium-size circuits. Approximate forward traversal deals with bigger circuits at the expense of exactness. Backward traversal focuses the search process on the property under scrutiny, but it also takes into account many unreachable states. For this reason, it works mainly on small circuits. This paper presents novel techniques that make exact symbolic backward traversal feasible also for large circuits. The key point is an efficient pruning of the search space, exploiting information coming from an approximate forward reachability analysis. Experimental evidence shows that, for the first time, the larger ISCAS'89 and MCNC circuits are symbolically manipulated in an exact way and the test patterns for them are generated.>

Symbolic state space exploration techniques proved to be useful not only in formal verification and synthesis, but also in testing. Most of them are based on exact forward or backward traversal. As an alternative, approximate forward traversal algorithms have been proposed, but they are not immediately applicable to test pattern generation. This paper presents strategies for approximate forward traversal, then it combines approximate forward traversal and backward traversal for generating test patterns for hard to detect faults. Efficient search space pruning is obtained by means of cofactoring. Experimental results show that the speed up ranges from 2 to more than 50.>

Until now, symbolic FSM state space exploration techniques were limited to small circuits. This paper presents a combination of approximate forward and exact backward traversal that handles larger circuits. For the first time, we have been able to generate test patterns for or to tag as undetectable the faults of some ISCAS'89 and MCNC benchmarks never considered before.