Model Checking with “X Value Based on PSL

摘要：

The foundation of hardware verification is that an implementation satisfies its specification. The specification described by a natural language may be ambiguous and inconsistence. The Acclellera Property Specification Language (PSL) is developed for the formal specification of hardware. It provides a standard means of specifying design properties using a concise syntax with clearly-defined formal semantics, particularly it offers an input method for dynamic(simulation) and static(formal verification method, such as model checking) verification tools. This paper proposes how to use model checking to verify a property with “X value, and gives a model checking algorithm based on 3-valued (true, false, X) logic formula of PSL. This algorithm has the same time complexity as 2-valued logic model checking. Finally, we present how to separate CTL formula from a PSL verification unit, and verify these properties from PSL under the given model.

作者: Guo Jian Han Jungang Yang Hongli Wang Bo

作者单位: Xidian University Shaanxi China 710071 Xian institute of posts and telecommunications Shaanxi China 710061

会议类型: 国际会议

会议名称: 第八届国际电子测量与仪器学术会议(Proceedings of 2007 8th International Conference on Electronic Measurement & Instruments)

会议地点: 西安

会议语种:英文

在线出版日期: 2007-08-16（万方平台首次上网日期，不代表论文的发表时间）