Title: a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol
Author: Li Yongjian
; Hung William N.N.
; Song Xiaoyu
Keyword: Semantics
; Trajectories
Source: Theoretical Computer Science
Issued Date: 2011
Volume: 412, Issue: 25, Pages: 2746-2765 Indexed Type: EI
Department: (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
English Abstract: 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 ID: WOS:000291087100004
Citation statistics:
Content Type: 期刊论文
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.
