题名: a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol
作者: Li Yongjian
; Hung William N.N.
; Song Xiaoyu
关键词: Semantics
; Trajectories
刊名: Theoretical Computer Science
发表日期: 2011
卷: 412, 期: 25, 页: 2746-2765 收录类别: EI
部门归属: (1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (2) Synopsys Inc., Mountain View, CA 94043, United States; (3) Department of ECE, Portland State University, Portland, OR 97207, United States
英文摘要: This paper presents a formal symbolic trajectory evaluation (STE) theory based on a structural netlist circuit model, instead of an abstract next state function. We introduce an inductive definition for netlists, which gives an accurate and formal definition for netlist structures. A closure state function of netlists is formally introduced in terms of the formal netlist model. We refine the definition of the defining trajectory and the STE implementation to deal with the closure state function. The close correspondence between netlist structures and properties is discussed. We present a set of novel algebraic laws to characterize the relation between the structures and properties of netlists. Finally, the application of the new laws is demonstrated by parameterized verification of the properties of content-addressable memories. © 2010 Elsevier B.V. All rights reserved. WOS记录号: WOS:000291087100004
Citation statistics:
内容类型: 期刊论文
URI标识: http://ir.iscas.ac.cn/handle/311060/14087
Appears in Collections: 计算机科学国家重点实验室 _期刊论文
File Name/ File Size
Content Type
Version
Access
License
A novel formalization of symbolic trajectory evaluation semantics in Isabelle.pdf （408KB） -- -- 限制开放 -- 联系获取全文
Recommended Citation:
Li Yongjian,Hung William N.N.,Song Xiaoyu. a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol[J]. Theoretical Computer Science,2011-01-01,412(25):2746-2765.
