Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean cir...Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean circuit specifications and logic designs, but these methods require a large amount of memory and time. Due to these limitations, several models of Decision Diagrams have been studied and other verification techniques have been proposed. In this paper, we have used probabilistic verification with Galois (or finite) field GF(2m) modifying the CUDD package for the computation of signatures in classical OBDDs, and for the construction of Mod2-OBDDs (also known as ?-OBDDs). Mod2-OBDDs have been constructed with a two-level layer of ?-nodes using a positive Davio expansion (pDE) for a given variable. The sizes of the Mod2-OBDDs obtained with our method are lower than the Mod2-OBDDs sizes obtained with other similar methods.展开更多
A short-time scaling criterion of variable ordering of OBDDs is proposed. By this criterion it is easy and fast to determine which one is better when several. variable orders are given, especially when they differ 10%...A short-time scaling criterion of variable ordering of OBDDs is proposed. By this criterion it is easy and fast to determine which one is better when several. variable orders are given, especially when they differ 10% or more in resulted BDD size from each other. An adaptive variable order selection method, based on the short-time scaling criterion, is also presented. The experimental results show that this method is efficient and it makes the heuristic variable ordering methods more practical.展开更多
An efficient heuristic algorithm for variable ordering of OBDDs, the WDHA (Weight and Distance based Heuristic Algorithm), is presented. The algorithm is based on the heuristics implied in the circuit structure grap...An efficient heuristic algorithm for variable ordering of OBDDs, the WDHA (Weight and Distance based Heuristic Algorithm), is presented. The algorithm is based on the heuristics implied in the circuit structure graph. To scale the heuristics, pi -weight , node -weight , average -weight and pi -distance in the circuit structure graph are defined. As any of the heuristics is not a panacea for all circuits, several sub algorithms are proposed to cope with various cases. One is a direct method that uses pi -weight and pi -distance . The others are based on the depth first search (DFS) traversal of the circuit structure graph, with each focusing on one of the heuristics. An adaptive order selection strategy is adopted in WDHA. Experimental results show that WDHA is efficient in terms of BDD size and run time, and the dynamic OBDD variable ordering is more attractive if combined with WDHA.展开更多
根据机械装配序列推理的特点,对PADL-2提供的CAD模型数据进行简化处理,再结合有序二叉决策图(OBDD-O rdered B inary D ec is ion D iagram),建立了一种新的装配体模型。基于此模型,可以通过一系列的OBDD符号运算完成装配操作的可行性判...根据机械装配序列推理的特点,对PADL-2提供的CAD模型数据进行简化处理,再结合有序二叉决策图(OBDD-O rdered B inary D ec is ion D iagram),建立了一种新的装配体模型。基于此模型,可以通过一系列的OBDD符号运算完成装配操作的可行性判断,从而实现了装配序列的推理。这种推理方法容易实现计算机化和自动化,是对文献[6]中推理方法的一种改进。通过对实例的实现和分析证明了该方法是切实可行的。展开更多
文摘Formal verification is fundamental in many phases of digital systems design. The most successful verification procedures employ Ordered Binary Decision Diagrams (OBDDs) as canonical representation for both Boolean circuit specifications and logic designs, but these methods require a large amount of memory and time. Due to these limitations, several models of Decision Diagrams have been studied and other verification techniques have been proposed. In this paper, we have used probabilistic verification with Galois (or finite) field GF(2m) modifying the CUDD package for the computation of signatures in classical OBDDs, and for the construction of Mod2-OBDDs (also known as ?-OBDDs). Mod2-OBDDs have been constructed with a two-level layer of ?-nodes using a positive Davio expansion (pDE) for a given variable. The sizes of the Mod2-OBDDs obtained with our method are lower than the Mod2-OBDDs sizes obtained with other similar methods.
文摘A short-time scaling criterion of variable ordering of OBDDs is proposed. By this criterion it is easy and fast to determine which one is better when several. variable orders are given, especially when they differ 10% or more in resulted BDD size from each other. An adaptive variable order selection method, based on the short-time scaling criterion, is also presented. The experimental results show that this method is efficient and it makes the heuristic variable ordering methods more practical.
基金the National Natural Science Foundationof China! ( No.69873 0 2 6)the Post-doctoral ScienceFoundation of China
文摘An efficient heuristic algorithm for variable ordering of OBDDs, the WDHA (Weight and Distance based Heuristic Algorithm), is presented. The algorithm is based on the heuristics implied in the circuit structure graph. To scale the heuristics, pi -weight , node -weight , average -weight and pi -distance in the circuit structure graph are defined. As any of the heuristics is not a panacea for all circuits, several sub algorithms are proposed to cope with various cases. One is a direct method that uses pi -weight and pi -distance . The others are based on the depth first search (DFS) traversal of the circuit structure graph, with each focusing on one of the heuristics. An adaptive order selection strategy is adopted in WDHA. Experimental results show that WDHA is efficient in terms of BDD size and run time, and the dynamic OBDD variable ordering is more attractive if combined with WDHA.
文摘根据机械装配序列推理的特点,对PADL-2提供的CAD模型数据进行简化处理,再结合有序二叉决策图(OBDD-O rdered B inary D ec is ion D iagram),建立了一种新的装配体模型。基于此模型,可以通过一系列的OBDD符号运算完成装配操作的可行性判断,从而实现了装配序列的推理。这种推理方法容易实现计算机化和自动化,是对文献[6]中推理方法的一种改进。通过对实例的实现和分析证明了该方法是切实可行的。
