| Formal Verification under Unknown Constraints |
| |
| 作者姓名： | LIXiao-weit |
| |
| 作者单位： | InstituteotComputingTechnology,ChineseAcademyofSciences,Ik,ijing100080,China／／GraduateSchooloftheChineseAcademyofSciences,Beijing100039,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). |
| |
| 摘 要： | 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 (BI)I)) 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.
|
| 关 键 词： | 计算机辅助设计 形式验证 末知约束条件 布尔可满足性 二元图表 |
| 收稿时间： | 14 May 2004 |
Formal verification under unknown constraints |
| |
| LIXiao-weit.Formal Verification under Unknown Constraints[J].Wuhan University Journal of Natural Sciences,2005,10(1):43-46. |
| |
| Authors: | Li Guang-hui Li Xiao-wei |
| |
| Institution: | (1) School of Information Engineering, Zhejiang Forestry College, 311300 Hangzhou Zhejiang, China;(2) Institute of Computing Technology, Chinese Academy of Sciences, 100080 Beijing, China;(3) Graduate School of the Chinese Academy of Sciences, 100039 Beijing, China |
| |
| Abstract: | 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. |
| |
| Keywords: | formal verification unknown constraints black box Boolean satisfiability Boolean comparison |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
|
