Issue No.06 - June (2013 vol.62)
T. Nopper , Dept. of Comput. Sci., Univ. of Freiburg, Freiburg, Germany
C. Scholl , Dept. of Comput. Sci., Univ. of Freiburg, Freiburg, Germany
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TC.2012.53
We consider the problem of checking whether an incomplete design (i.e., a design containing "unknown parts", so-called Black Boxes) can still be extended to a complete design satisfying a given property or whether the property is satisfied for all possible extensions. There are many applications of property checking for incomplete designs, such as early verification checks for unfinished designs, error localization in faulty designs and the abstraction of complex parts of a design in order to simplify the property checking task. To process incomplete designs we present an approximate, yet sound algorithm. The algorithm is flexible in the sense that for every Black Box a different approximation method can be chosen. This permits us to handle less relevant Black Boxes (in terms of the property) with larger approximation and thus faster, whereas we do not lose important information when the possible effect of more relevant Black Boxes is modeled by more exact methods. Additionally, we present a concept to decide exactly whether Black Boxes with bounded memory can be implemented so that they satisfy a given property. This question is reduced to conventional symbolic model checking. The effectiveness and feasibility of the methods is demonstrated by a series of experimental results.
Computational modeling, Boolean functions, Approximation methods, Logic gates, Data structures, Integrated circuit modeling, Algorithm design and analysis,BDDs, Symbolic model checking, verification, Black Boxes, incomplete designs, abstraction, approximation
T. Nopper, C. Scholl, "Symbolic Model Checking for Incomplete Designs with Flexible Modeling of Unknowns", IEEE Transactions on Computers, vol.62, no. 6, pp. 1234-1254, June 2013, doi:10.1109/TC.2012.53