Institutional Repository
| a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol | |
| Li Yongjian; Hung William N.N.; Song Xiaoyu | |
| 2011 | |
| Source | Theoretical Computer Science
 |
| ISSN | 3043975 |
| Volume | 412Issue:25Pages:2746-2765 |
| 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. |
| Indexed Type | EI |
| Keyword | Semantics Trajectories |
| 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 |
| WOS ID | WOS:000291087100004 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/14087 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | Li Yongjian,Hung William N.N.,Song Xiaoyu. a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol[J]. Theoretical Computer Science,2011,412(25):2746-2765. |
| APA | Li Yongjian,Hung William N.N.,&Song Xiaoyu.(2011).a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol.Theoretical Computer Science,412(25),2746-2765. |
| MLA | Li Yongjian,et al."a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol".Theoretical Computer Science 412.25(2011):2746-2765. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| A novel formalizatio（408KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment