In this work we advocate the adoption of Binary Decision Diagrams (BDDs) for storing and manipulating Time-Series datasets. We first propose a generic BDD transformation which identifies and removes 50% of all BDD edges without any loss of information. Following, we optimize the core operation for adding samples to a dataset and characterize its complexity. We identify time-range queries as one of the core operations executed on time-series datasets, and describe explicit Boolean function constructions that aid in efficiently executing them directly on BDDs. We exhibit significant space and performance gains when applying our algorithms on synthetic and real-life biosensor time-series datasets collected from field trials.

We present the architecture of a new Ordered Binary Decision Diagram library that is designed from the ground up to be space efficient. The main novelty lies in the library's node structure, which is modified at run-time to closely follow the variations in size of the stored OBDDs. We compare the new library with existing OBDD libraries on ACM/SIGDA and industrial circuits and report significant performance and space gains.

State-space-partitioning-based approaches have been proposed in the literature to address the state-explosion problem in model checking. These approaches, whether sequential or distributed, perform a large amount of work in the form of interpartition (crossover) image computations, which can be expensive. A model-checking algorithm that aggregates these expensive crossover images by localizing computation to individual partitions is presented. It reduces the number of crossover images and drastically outperforms extant approaches in terms of crossover image computation cost as well as total model-checking time, often by two orders of magnitude.

Formal verification, especially error detection, is rapidly increasing in importance with the rising complexity of designs. The main constraint in verification is the total amount of resources available - both time as well as memory. Most attempts at verification only use a single processor. Recently, various attempts have been made to use parallel and distributed methods for verification. However, verification in a Grid-based environment has not yet been very widely adopted. As personal computers gain in computing capacity, the concept of computation grids is gaining acceptance. Here, a grid is a network of machines that may not be dedicated to a specific computational use, but may only be available some of the time. This is a unique environment where massive parallelism is possible by using otherwise idle CPU cycles from a large number of computers. Such processors may even be in geographically diverse locations. We describe a Grid-based verifi- cation environment for detecting errors in a design. We verify user-written assertions as well as properties, e.g. unreachable code, index-out-of-range, that are extracted automatically from the design using a state-of-the-art HDL parser. Such an approach can help the user to quickly find RTL level bugs earlier in the design cycle.

Partitioned BDD-based algorithms have been proposed in the literature to solve the memory explosion problem in BDD-based verification. Such algorithms can be at times ineffective as they suffer from the problem of scheduling the relative order in which the partitions are processed. In this paper we present a novel multi-threaded reachability algorithm that avoids this scheduling problem while increasing the latent parallelism in partitioned state space traversal. We show that in most cases our method is significantly faster than both the standard reachability algorithm as well as the existing partitioned approaches. The gains are further magnified when our threaded implementation is evaluated in the context of a parallel framework.

We describe a complete method for the latch mapping problem that is based on the efficient integration of previously proposed tech-niques for latch mapping as well as novel optimizations for further improvement. The highlights of the proposed approach include a new method of integrating complete methods and incomplete meth-ods for latch mapping, the use of incremental reasoning to optimize the overall algorithm and the use of a conventional combinational equivalence checking tool as the core engine. Experiments con-firm that the proposed method retains much of the efficiency and capacity of incomplete methods while providing the completeness of complete methods and derives significant performance improve-ments from the proposed optimizations.

We discuss an open problem with constructing an OBDD using composition and prove that the worst case complexity of the construction is truly cubic. Using this insight, we show compactness of partitioned-OBDD over monolithic OBDD.

Article Free Access Share on Automatic partitioning for efficient combinatorial verification Authors: Rajarshi Mukherjee Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CA Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CAView Profile , Jawahar Jain Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CA Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CAView Profile , Koichiro Takayama Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CA Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CAView Profile , Masahiro Fujita Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CA Fujitsu Laboratories of America, 595 Lawrence Expressway, Sunnyvale, CAView Profile Authors Info & Claims ASP-DAC '00: Proceedings of the 2000 Asia and South Pacific Design Automation ConferenceJanuary 2000 Pages 67–72https://doi.org/10.1145/368434.368521Published:28 January 2000Publication History 0citation161DownloadsMetricsTotal Citations0Total Downloads161Last 12 Months10Last 6 weeks0 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

We discuss an open problem in ROBDD construction using composition and prove that the worst case complexity of the construction is truly cubic. With this insight we show that the process of composition naturally leads to construction of (even exponentially) compact partitioned-OBDDs (POBDDs)[17]. Our algorithm which incorporates dynamic partitioning, leads to the most general (and compact) form of POBDDs - graphs with multiple root variables. To show our algorithm is robust and practical, we have analyzed some well known problems in Boolean function representation, verification and finite state machine analysis where our approach generates graphs which are even orders of magnitude smaller.

Variable ordering for BDDs has been extensively investigated. Recently, sampling based ordering techniques have been proposed to overcome problems with structure based static ordering methods and sifting based dynamic reordering techniques. However, existing sampling techniques can lead to an unacceptably large deviation in the size of the final BDD. In this paper, we propose a new sampling technique based on abstract BDDs (aBDDs) that does not suffer from this problem. This new technique, easy to implement and automate, consistently creates high quality variable orderings for both combinational as well as sequential functions. Experimental results show that for many applications our approach is significantly superior to existing techniques.

Improvement of the accuracy of error and fault diagnosis as well as ATPG for IP-based designs are important problems in industry. In this paper we address these problems when portions of the design may be unspecified. Two approaches to solve these problems have been presented: (1) solving Boolean satisfiability under unknown constraints, and (2) a network modification-based solution. Experimental results on constrained equivalence checking, enhancement of error diagnosis resolution for combinational circuits, and ATPG for IP-based designs have been presented on the ISCAS 85 benchmark and industrial circuits.

In this paper, we present multiple error diagnosis algorithms to overcome two significant problems associated with current error diagnosis techniques targeting large circuits: their use of limited error models and a lack of solutions that scale well for multiple errors.Our solution is based on a nonenumerative analysis technique, based on logic simulation (3-valued and symbolic), for simultaneously analyzing all possible errors at sets of nodes in the circuit.Error models are introduced in order to address the "locality" aspect of error location and to identify sets of nodes that are "local" with respect to each other.Theoretical results are provided to guarantee the diagnosis of modeled errors and robust diagnosis approaches are shown to address the cases when errors do not correspond to the modeled types.Experimental results on benchmark circuits demonstrate accurate and extremely rapid location of errors of large multiplicity.

We have developed a filter-based framework where several fundamentally different techniques can be combined to provide fully automated and efficient heuristic solutions to verification and possibly other NP-complete problems. Such an integrated methodology is far more robust and efficient than any single existing technique on a wide variety of circuits. Our methodology has been applied to verify the ISCAS 85 benchmark circuits and efficient verification results have been presented on a large set of industrial circuits which could not be verified using several published techniques and commercial verification tools available to us.

Combinational verification is a co-NP complete problem. However, in reality, several techniques exist which perform reasonably well on many practical circuits. Also, it is often found that while one technique efficiently verifies a given circuit it fails badly on another circuit, whereas a certain other technique is efficient on the latter circuit but cannot handle the former circuit. Therefore, clearly, a robust verification methodology cannot depend on any single technique. Our goal in this research is to build a verification methodology whose performance is more immune to circuit variations. We have developed a methodology where several fundamentally different techniques can be combined to provide efficient heuristic solutions to combinational verification, and possibly other intractable problems as well. Such an integrated methodology is far more robust and efficient on a majority of combinational verification problems than any single existing technique. In this paper, we discuss the methodology in detail and present verification results using a fully automated prototype of the proposed methodology. Using this methodology, we can verify many circuits which could not be efficiently verified using any published techniques available to us, and even by some popular commercial combinational verification programs.

: We suggest some novel variable ordering techniques based upon the notion of sampling. Such techniques can produce highly e#ective static variable orders, and can thus be employed in numerous problems where current static variable ordering techniques prove totally inadequate. They can also augmentvarious reordering techniques thereby helping to produce far superior variable orders in a comparable, or lesser, amount of time. Importantly,wehave been able to build BDDs of circuits which could not be represented previously using numerous other reordering packages. 1 Introduction Ordered Binary Decision Diagrams #3# have found extensive use in various algorithms for analyzing Boolean functions, and thus play an important role in numerous CAD related applications. Unfortunately, in many applications, very large sized BDDs can be generated which can render a BDD based analysis scheme impractical or ine#cient. In particular, OBDD sizes are very sensitive to the order chosen on input variabl...

We address the problem of finite state machine (FSM) traversal, a key step in most sequential verification and synthesis algorithms. We propose the use of partitioned ROBDDs to reduce the memory explosion problem associated with symbolic state space exploration techniques. In our technique, the reachable state set is represented as a partitioned ROBDD (A. Narayan et al., 1996). Different partitions of the Boolean space are allowed to have different variable orderings and only one partition needs to be in memory at any given time. We show the effectiveness of our approach on a set of ISCAS89 benchmark circuits. Our techniques result in a significant reduction in total memory utilization. For a given memory limit, partitioned ROBDD based method can complete traversal for many circuits for which monolithic ROBDDs fail. For circuits where both partitioned ROBDDs as well as monolithic ROBDDs cannot complete traversal, partitioned ROBDDs can reach a significantly larger set of states.

With the increase in the complexity of present day systems, proving the correctness of a design has become a major concern. Simulation based methodologies are generally inadequate to validate the correctness of a design with a reasonable confidence. More and more designers are moving towards formal methods to guarantee the correctness of their designs. The authors survey some state-of-the-art techniques used to perform automatic verification of combinational circuits. They classify the current approaches for combinational verification into two categories: functional and structural. The functional methods consist of representing a circuit as a canonical decision diagram. Two circuits are equivalent if and only if their decision diagrams are equal. The structural methods consist of identifying related nodes in the circuit and using them to simplify the problem of verification. They briefly describe some of the methods in both the categories and discuss their merits and drawbacks.

A new Boolean function representation scheme, the Indexed Binary Decision Diagram (IBDD), is proposed to provide a compact representation for functions whose Ordered Binary Decision Diagram (OBDD) representation is intractably large. We explain properties of IBDDs and present algorithms for constructing IBDDs from a given circuit. Practical and effective algorithms for satisfiability testing and equivalence checking of IBDDs, as well as their implementation results, are also presented. The results show that many functions, such as multipliers and the hidden-weighted-bit function, whose analysis is intractable using OBDDs, can be efficiently accomplished using IBDDs. We report efficient verification of Booth multipliers, as well as a practical strategy for polynomial time verification of some classes of unsigned array multipliers.

We present a new representation for Boolean functions called Partitioned ROBDDs. In this representation we divide the Boolean space into 'k' partitions and represent a function over each partition as a separate ROBDD. We show that partitioned-ROBDDs are canonical and can be efficiently manipulated. Further they can be exponentially more compact than monolithic ROBDDs and even free BDDs. Moreover, at any given time, only one partition needs to be manipulated which further increases the space efficiency. In addition to showing the utility of partitioned-ROBDDs on special classes of functions, we provide automatic techniques for their construction. We show that for large circuits our techniques are more efficient in space as well as time over monolithic ROBDDs. Using these techniques, some complex industrial circuits could be verified for the first time.

Article Advanced verification techniques based on learning Share on Authors: Jawahar Jain Fujitsu Laboratories of America, 77 Rio Robles, San Jose CA Fujitsu Laboratories of America, 77 Rio Robles, San Jose CAView Profile , Rajarshi Mukherjee Fujitsu Laboratories of America, 77 Rio Robles, San Jose CA and Dept. of Electrical and Computer Engineering, University of Texas at Austin, Austin TX Fujitsu Laboratories of America, 77 Rio Robles, San Jose CA and Dept. of Electrical and Computer Engineering, University of Texas at Austin, Austin TXView Profile , Masahiro Fujita Fujitsu Laboratories of America, 77 Rio Robles, San Jose CA Fujitsu Laboratories of America, 77 Rio Robles, San Jose CAView Profile Authors Info & Claims DAC '95: Proceedings of the 32nd annual ACM/IEEE Design Automation ConferenceJanuary 1995 Pages 420–426https://doi.org/10.1145/217474.217564Published:01 January 1995 57citation243DownloadsMetricsTotal Citations57Total Downloads243Last 12 Months2Last 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 SiteGet Access

Introduces some new methods for estimating the "importance" of a variable in a Boolean function, and uses them to compute variable orders for OBDD construction. These measures are based on information theoretic criteria, and require the computation of the entropy of a variable in a given function. These entropy measures prove quite effective in distinguishing the importance of variables. Experimental results show this to be a very encouraging approach to help in the solution of this well known problem.>

Recently, learning-based techniques, which are extremely effective in finding test vectors for hard to detect faults and in detecting redundancies, have been proposed as an efficient alternative to the traditional branch-and-bound techniques for test generation. This paper presents functional learning, a new OBDD-based learning technique, that uses implication procedures. Functional learning is complete given enough time; it will determine all the uniquely implied values in the circuit from the current situation of value assignments. The most attractive feature of functional learning is its ability to extract, maintain and manipulate novel information regarding the circuit in compact OBDD representations for Boolean functions.>

The authors present a novel method for verifying the equivalence of two Boolean functions. Each function is hashed to an integer code by assigning random integer values to the input variables and evaluating its integer-valued representation. The equivalence of two functions can be verified with a very low probability of error. The probability of error can be exponentially decreased by making multiple runs. Results indicate significant time and space advantages for this method over deterministic techniques. Some functions known to require space (and time) exponential in the number of input variables for deterministic verification require only polynomial resources using the proposed technique.>