Parallel Bounded Property Checking with SymC
Pradeep Kumar Nalla, Roland J. Weiss, Jürgen Ruf, Thomas Kröpf, Wolfgang Rosenstiel · 2005
Abstract. Today, verification of industrial size designs like multi-million gate ASICs (Application Specific Integrated Circuit) and SoC (System-on-a-Chip) processors consumes up to 75 % of the design effort. The trend to augment functional verification with formal verification tries to alleviate this problem. Efficient property checking algorithms based on binary decision diagrams (BDDs) and satisfiability (SAT) solvers allow automatic verification of medium-sized designs. However, the steadily increasing design sizes still leave verification the major bottleneck, because formal methodologies do not yet scale to very large designs. To address these problems, we developed the bounded property checking tool SymC. SymC takes properties and a system description as inputs and translates them into a symbolically simulatable representation. SymC performs forward state space traversal for verifying the properties. However, for larger designs SymC cannot complete the traversal due to the state space explosion problem. Therefore, we propose a parallel version of SymC. The main idea of our approach is to split the state set into partitions and delegate traversal of these subsets to nodes on a cluster computer. Depending on the property and the quantification operator, detecting an accepting or rejecting state on one node can immediately abort computation on all other nodes and a witness/counterexample is produced. Otherwise, only the current search path is terminated and the remaining paths are traversed further. Parallel computation shows approximately linear speedups in execution time, enables faster verification of properties and we are able to handle larger designs. 1