Counterexample-guided choice of projections in approximate symbolic model checking

BDD-based symbolic techniques of approximate reachability analysis based on decomposing the circuit into a collection of overlapping sub-machines (also referred to as overlapping projections) have been recently proposed posed. Computing a superset of the reachable states in this fashion is susceptible to false negatives. Searching for real counterexamples in such an approximate space is liable to failure. In this paper, the "hybridization effect" induced by the choice of projections is identified as the cause for the failure. A heuristic based on Hamming Distance is proposed to improve the choice of projections, that reduces the hybridization effect and facilitates either a genuine counterexample or proof of the property. The ideas are evaluated on a real large design example from the PCI Interface unit in the MAGIC chip of the Stanford FLASH Multiprocessor.