engleski

Symbolic Boolean Function Representation and Handling on Distributed Computing Systems

Binary decision diagrams (BDDs) are data structures that enable efficient representation and formal verification of digital systems. There are different heuristics that can be employed in order to optimize BDD based formal verification process. In particular, distributed BDD construction and manipulation can be used to make formal verification of digital systems more efficient. The paper describes distributed algorithms for BDD manipulation based on combined breadth-first and depth-first BDD construction techniques. The algorithms are targeted for execution on network of workstations. The measurement of the distributed BDD creation performance is accomplished by building BDD representation of digital multiplier circuit. The multiplier is used because of the specific characteristics of its BDD representations. Performance of distributed algorithms is measured using two processor system and a computer cluster. Special analysis on performance impact of distributed computed cache is also given.

Digital System Design; System Verification; Symbolic Methods

nije evidentirano