Sriram, S. ; Tandon, R. ; Dasgupta, P. ; Chakrabarti, P. P. (2001) Symbolic verification of Boolean constraints over partially specified functions In: The 2001 IEEE International Symposium on Circuits and Systems, 2001. ISCAS 2001, 6-9 May 2001, Sydney, NSW, Australia.
Full text not available from this repository.
Official URL: http://ieeexplore.ieee.org/document/921998/
Related URL: http://dx.doi.org/10.1109/ISCAS.2001.921998
Abstract
Incomplete or partial specifications arise out of mistakes in design or purposefully to avoid loss of generality in application. When designing a system with several partially specified functions, we often impose constraints on the global behavior of the system. In this paper we study the problem of verifying whether a set of partially specified functions meets such constraints. We show that the problem is /spl Pi//sub 2//sup P/ complete. While symbolic BDD-based algorithms have been widely used for propositional satifiability (/spl Sigma//sub 1//sup P/ complete) and validity (/spl Pi//sub 1//sup P/ complete) problems, the structure of BDDs is not natural for solving /spl Pi//sub 2//sup P/ complete problems. We present a two-step BDD-based method for solving the above /spl Pi//sub 2//sup P/ complete problem and show that the method is effective when the number of functions is small.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Source: | Copyright of this article belongs to Institute of Electrical and Electronics Engineers. |
| ID Code: | 101720 |
| Deposited On: | 09 Mar 2018 10:18 |
| Last Modified: | 09 Mar 2018 10:18 |
Repository Staff Only: item control page
