文章基本信息

标题：BDD Algortihms and Cache Misses
本地全文：下载
作者：Nils Klarlund ; Theis Rauhe
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1996
卷号：3
期号：26
出版社：Aarhus University
摘要：Within the last few years, CPU speed has greatly overtaken memory speed. For this reason, implementation of symbolic algorithms - with their extensive use of pointers and hashing - must be reexamined. In this paper, we introduce the concept of cache miss complexity as an analytical tool for evaluating algorithms depending on pointer chasing. Such algorithms are typical of symbolic computation found in verification. We show how this measure suggests new data structures and algorithms for multi-terminal BDDs. Our ideas have been implemented in a BDD package, which is used in a decision procedure for the Monadic Second-order Logic on strings. Experimental results show that on large examples involving e.g the verification of concurrent programs, our implementation runs 4 to 5 times faster than a widely used BDD implementation. We believe that the method of cache miss complexity is of general interest to any implementor of symbolic algorithms used in verification.