My full proposal document is here. The title and the abstract are as follows. Here is my talk.
However, all verification algorithms based on characteristic function representation are inherently limited. Symbolic simulation overcomes this limitation by implicitly representing the set of states as a vector of functions in parametric form, one function for each state variable. Techniques like bounded model checking (BMC) and various symbolic trajectory evaluation (STE) algorithms use this implicit representation. The image computation step is simple in symbolic simulation, as it just amounts to unwinding the transition relation of the system. Moreover, the size of the representation of the set of states is linear in the number of simulation steps. There are two main problems with existing algorithms: First, even a linear growth in the sizes of the formulae can be prohibitive for large circuits, thus limiting the simulation depth. BDD based symbolic simulation tries to address this issue by reparameterization, i.e., converting a parametric form into another another smaller parametric form. However, this is not applicable to BMC. More seriously, BDD based reparameterization algorithms are ineffective at handling all but small designs as the large number of variables that need to be quantified during reparameterization adversely affect the performance. The number of variables to be quantified grows linearly with the the simulation depth and the circuit size. I propose a novel SAT based reparameterization algorithm that solves these problems. The algorithm uses the SAT based enumeration procedure described earlier for quantification. First, the SAT based reparameterization algorithm builds Boolean expressions, which do not suffer from variable ordering problems, and can be used in BMC equally well. Next, the reparameterization algorithm is largely unaffected by the number of variables that are existentially quantified in the enumeration, thus enabling the simulation to go much deeper than existing techniques. I demonstrated a 3x improvement in the runtime and space requirement over existing BMC algorithm and BDD based symbolic simulator on large industrial circuits. The symbolic simulator using SAT based reparameterization algorithm forms the central part of my thesis. The reparameterization algorithm benefits from improvements in the SAT based enumeration procedure presented earlier. I will investigate nonclausal representations for the enumeration algorithm as there are known functions for which no concise clausal representations are possible. The size of a parametric representation is affected by the relative ordering of the state variables. I propose to investigate variable ordering techniques used in BDD based image computation [CHARME'01,ICCAD'01] for this purpose.
The integration of the reparameterization algorithm in a SAT based abstraction-refinement framework concludes my proposal. My algorithm can simulate much longer abstract counterexamples than currently possible. I propose to extract refinement information from the simulation, as was done in my earlier work [FMCAD'02]. Using the reparameterization algorithm in the SAT based abstraction-refinement framework will make the algorithm complete for safety properties. When the property is true, abstract model checking is used to infer that fact, and if the property is false, the symbolic simulator will provide a counterexample. Recently, Biere et al. have demonstrated how a liveness property can be reduced to safety property by a semantic translation and introduction of auxiliary variables in the transition system. Using reparameterization algorithm in the abstraction-refinement framework thus allows us to prove of both safety and liveness properties.