Research on Efficient Manipulation of Boolean Functions Using Shared Binary Decision Diagrams and Its Application to Computer Aided Logic Design

我们对布尔函数的高效表示和操作进行了研究，并将其应用于计算机辅助逻辑设计。布尔函数的高效表示和操作我们利用共享二进制决策图（sdd）对布尔函数的高效表示进行了研究。为了有效地操作sddds，我们提出了属性边。我们已经开发了一个矢量算法来操纵sdd。我们还研究了最小化sbdd的变量排序方法。基于共享二值决策图的计算机辅助逻辑设计我们将布尔函数操作应用于逻辑电路的故障诊断和时序验证。在故障诊断方面，我们开发了高效的多故障模拟方法和生成紧凑测试集的新方法。在时序验证方面，我们开发了具有不确定性延迟的逻辑电路仿真方法。基于共享二元决策图的逻辑设计形式化验证我们提出了一种使用sdd来表示状态转换图的方法。在此基础上，提出了分支时间规则时间逻辑的形式化验证算法，并实现了序列机的形式化验证系统。布尔函数运算的计算复杂度我们已经阐明了用bdd有效表示的一类函数。我们还开发了一种操纵bdd的并行化方法，并澄清了计算复杂性。为了便于在计算机辅助逻辑设计工具上操作sdd，我们开发了一个软件包。

We have carried out researches on efficient representation and manipulation of Boolean functions, and applied them to computer aided logic design.1. Efficient Representation and Manipulation of Boolean FunctionsWe have carried out researches on the efficient representation of Boolean functions using Shared Binary Decision Diagrams (SBDDs). For efficient manipulation of SBDDS, we have proposed attributed edges. We have developed a vector algorithm for manipulating SBDDs. We have also investigated variables ordering methods for minimizing SBDDs.2. Computer Aided Logic Design Using Shared Binary Decision DiagramsWe have applied Boolean function manipulation to fault diagnosis and timing verification of logic circuits. On fault diagnosis, we have developed efficient fault simulation methods for multiple faults and novel methods of generating compact test sets. On timing verification, we have developed methods for simulating logic circuits with nondeterministic delays.3. Formal Verification of Logic Design Using Shared Binary Decision DiagramsWe have proposed a method to represent state transition diagrams using SBDDs. Based on the method, we have developed a formal verification algorithm on branching time regular temporal logic, and implemented a formal verification system for sequential machines.4. Computational Complexity of Boolean Function ManipulationWe have clarified the class of functions efficiently expressed by BDDs. We have also developed a paranelization methods for manipulating BDDs and clarified the computational complexity.5. Systems for Computer Aided Logic DesignWe have developed a package software so as to make it easy to manipulate SBDDs on tools for computer aided logic design.