Symmetry reduction for STE model checking using structured models
Ashish Darbari · ePrints Soton (University of Southampton) · 2006
Symbolic trajectory evaluation (STE) is not sufficient to handle verification of circuits with large number of state holding elements such as memories.It is also the case that memory based circuits have plenty of symmetry, which can be exploited for computing reductions for STE model checking.This dissertation addresses the problem of symmetry reduction for STE model checking.There are two main challenges involved in achieving an efficient solution to the problem of symmetry reduction.First is the discovery of symmetry in the circuit, and second, a methodology of computing reductions in the size of the STE model checking run.To address the problem of finding symmetries in circuits, we propose a method of designing circuit models, so that symmetries in the structure of the circuit, can be recorded at the time of design.We propose a framework that allows us to model circuits using special functions, and a type system is provided to enforce discipline on the usage of these functions.A type soundness theorem then guarantees that circuits constructed using these functions have symmetry.The other main contribution of our work is the design of a reduction methodology.This is centered around the use of novel STE inference rules, and a symmetry soundness theorem.Inference rules are used to decompose the original property into a set of smaller properties, which is then clustered into several equivalence classes based on the symmetry of circuit model.One representative property is chosen from each equivalence class and verified using an STE simulator, and then using the symmetry soundness theorem correctness of the entire class of equivalent properties is deduced.Inference rules are then used to compose the overall statement of correctness given by the original property.We demonstrate the strength of our approach on several examples and case studies.