scholarly journals BDD-based verification of scalable designs

2007 ◽  
Vol 20 (3) ◽  
pp. 367-379
Author(s):  
Daniel Große ◽  
Rolf Drechsler
Keyword(s):  
Data Structure ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Verification Algorithm ◽  
Word Level ◽  
Variable Ordering ◽  
Level Data ◽  
Level Information ◽  
Speed Up ◽  
Verification Techniques

Many formal verification techniques make use of Binary Decision Diagrams (BDDs). In most applications the choice of the variable ordering is crucial for the performance of the verification algorithm. Usually BDDs operate on the Boolean level, i.e. BDDs are a bit-level data structure. In this paper we present a method to speed-up BDD-based verification of scalable designs that makes use of a learning process for word-level information. In a pre-processing a scalable ordering is extracted from the RTL that is used as a static ordering for large designs. Experimental results show that significant improvements can be achieved.

scholarly journals DenseZDD: A Compact and Fast Index for Families of Sets

Algorithms ◽  
2018 ◽  
Vol 11 (8) ◽  
pp. 128 ◽  
Author(s):  
Shuhei Denzumi ◽  
Jun Kawahara ◽  
Koji Tsuda ◽  
Hiroki Arimura ◽  
Shin-ichi Minato ◽  
...  
Keyword(s):  
Data Structure ◽  
Data Structures ◽  
Information Integration ◽  
Decision Diagrams ◽  
Web Information Retrieval ◽  
Binary Decision ◽  
Web Information ◽  
Set Operations ◽  
Succinct Data Structure ◽  
The Family

In this article, we propose a succinct data structure of zero-suppressed binary decision diagrams (ZDDs). A ZDD represents sets of combinations efficiently and we can perform various set operations on the ZDD without explicitly extracting combinations. Thanks to these features, ZDDs have been applied to web information retrieval, information integration, and data mining. However, to support rich manipulation of sets of combinations and update ZDDs in the future, ZDDs need too much space, which means that there is still room to be compressed. The paper introduces a new succinct data structure, called DenseZDD, for further compressing a ZDD when we do not need to conduct set operations on the ZDD but want to examine whether a given set is included in the family represented by the ZDD, and count the number of elements in the family. We also propose a hybrid method, which combines DenseZDDs with ordinary ZDDs. By numerical experiments, we show that the sizes of our data structures are three times smaller than those of ordinary ZDDs, and membership operations and random sampling on DenseZDDs are about ten times and three times faster than those on ordinary ZDDs for some datasets, respectively.

scholarly journals Compressing Exact Cover Problems with Zero-suppressed Binary Decision Diagrams

2021 ◽  
Author(s):  
Masaaki Nishino ◽  
Norihito Yasuda ◽  
Kengo Nakamura
Keyword(s):  
Data Structure ◽  
State Of The Art ◽  
Linear Time ◽  
Binary Decision Diagrams ◽  
Experimental Results ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Running Time ◽  
Order Of Magnitude ◽  
Exact Cover

Exact cover refers to the problem of finding subfamily F of a given family of sets S whose universe is D, where F forms a partition of D. Knuth’s Algorithm DLX is a state-of-the-art method for solving exact cover problems. Since DLX’s running time depends on the cardinality of input S, it can be slow if S is large. Our proposal can improve DLX by exploiting a novel data structure, DanceDD, which extends the zero-suppressed binary decision diagram (ZDD) by adding links to enable efficient modifications of the data structure. With DanceDD, we can represent S in a compressed way and perform search in linear time with the size of the structure by using link operations. The experimental results show that our method is an order of magnitude faster when the problem is highly compressed.

A Variable Ordering Heuristic Based on Zero-Suppressed Binary Decision Diagrams

2010 ◽  
Author(s):  
Ya-zhou Li ◽  
Jin Wang ◽  
Li-qin Hu ◽  
Yi-can Wu
Keyword(s):  
Nuclear Power ◽  
Safety Assessment ◽  
Large Scale ◽  
Binary Decision Diagrams ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Minimal Cut Sets ◽  
Variable Ordering ◽  
Safety And Reliability ◽  
Event Trees

Two approaches have been proposed to solve the large-scale fault trees or event trees for Probabilistic Safety Assessment in a nuclear power plant. The first one consists in MCS/ZBDD, which uses ZBDDs (Zero-suppressed Binary Decision Diagrams) to implement classical MCS (Minimal Cut Sets) algorithm. The second consists in designing heuristics and strategies to reduce the complexity of the BDDs (Binary Decision Diagrams) construction. This paper was motivated to combine the MCS/ZBDD and designing heuristics for ZBDDs together. A heuristic, which took the failure rate of basic event into account and utilized that truncation could be implemented on ZBDDs during the calculating process, was proposed. This heuristic accelerated the analysis progress by bringing forward the truncation and reducing the complexity of the intermediate ZBDDs. RiskA, a Zero-suppressed Binary Decision Diagram package extended to safety and reliability analysis, has adopted this heuristic. RiskA’s truncation strategies, which had some relations with the ordering scheme, were also introduced. The correctness and efficiency of this new heuristic were verified by some practical models’ analyses.

Sign in / Sign up

Export Citation Format

Share Document