摘要
We present a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT). This method is based on a new encoding scheme of unknown constraints, and solves the corresponding conjunctive normal form (CNF) formulas.Furthermore,this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs. Experimental results demonstrate the efficiency and feasibility of the proposed method.
We present a formal method of verifying designs with unknown constraints (e.g., black boxes) using Boolean satisfiability (SAT). This method is based on a new encoding scheme of unknown constraints, and solves the corresponding conjunctive normal form (CNF) formulas.Furthermore,this method can avoid the potential memory explosion, which the binary decision diagram (BDD) based techniques maybe suffer from, thus it has the capacity of verifying large designs. Experimental results demonstrate the efficiency and feasibility of the proposed method.
作者
LI Guang-hui 1,2,3 , LI Xiao-wei 2,31. School of Information Engineering, Zhejiang Forestry College, Hangzhou 311300, Zhejiang, China
2. Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100080, China
3. Graduate School of the Chinese Academy of Sciences, Beijing 100039, China
基金
Supported by the National Natural Science Foun dation of China (90207002),the Science and Technology Project ofBeijing (H020120120130),and in part by the Zhejiang ProvincialNatural Science Foundation of China (M603097).
