Paper Info
Title
Input Elimination and Abstraction in Model Checking
Abstract
Symbolic model checking, while gaining success in the industry as a valuable tool for finding hardware design bugs, is still severely limited with respect to the size of the verifiable designs. This limitation is due to the nonlinear memory consumption of the data structure (namely, BDD and its variants) used to represent the model and the explored states. Input elimination is a known method that reduces the size of the model by existential quantification of the inputs. In this paper, we improve this technique in several dimensions: we present a novel re-encoding of the model that results in a much large set of quantifiable inputs, we introduce a new greedy algorithm for early quantification of the inputs during the transition relation build, and we suggest a new algorithm to reconstruct the input values in an error trace. Model abstraction is a semiautomatic method that requires the user to provide an abstraction mapping, and can dramatically reduce the size of models with large data-path. We show that data abstraction can be reduced to input elimination using few simple manipulations of the hardware netlist description. Model abstraction is a wellknown technique and our contribution is a novel technique that generates the minimal transition relation with respect to a given abstraction mapping.
Year
DOI
Venue
1998
10.1007/3-540-49519-3_20
FMCAD
Keywords
Field
DocType
input elimination,novel technique,abstraction mapping,wellknown technique,data abstraction,quantifiable input,model abstraction,model checking,symbolic model checking,input value,data structure,greedy algorithm
Transition system,Netlist,Abstraction model checking,Data structure,Model checking,Computer science,Algorithm,Greedy algorithm,Theoretical computer science,Finite-state machine,Abstraction inversion
Conference
ISBN
Citations 
PageRank 
3-540-65191-8
6
0.60
References 
Authors
10
2
Name
Order
Citations
PageRank
Sela Mador-Haim11746.87
Limor Fix2937118.11