Efficient Verification of the PCI Local Bus using Boolean Satisfiability
Fadi Aloul, Karem A. Sakallah · 2000
Abstract: The purpose of this paper is to study the application of Boolean Satisfiability to the verification of the PCI Local Bus. The novel feature of this approach is the generation of several propositional formulas that describe the specification of the bus system. The formulas are tested using a powerful SAT solver and the bus is verified for errors. The SAT-based approach has several important advantages over conventional BDD-based approaches such as achieving high speed testing. To demonstrate how our method works, we have modeled the PCI Local Bus and verified several properties.