| a novel formalization of symbolic trajectory evaluation semantics in isabelle/hol | |
| Li Yongjian; Hung William N.N.; Song Xiaoyu | |
| 2011 | |
| 发表期刊 | Theoretical Computer Science
 |
| ISSN | 3043975 |
| 卷号 | 412期号:25页码:2746-2765 |
| 摘要 | 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. |
| 收录类别 | EI |
| 关键词 | Semantics Trajectories |
| 部门归属 | (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记录号 | WOS:000291087100004 |
| 引用统计 | |
| 内容类型 | 期刊论文 |
| URI标识 | http://ir.iscas.ac.cn/handle/311060/14087 |
| 专题 | 基础软件与系统重点实验室 |
| 推荐引用方式 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. |
| 条目包含的文件 | ||||||
| 文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 | ||
| A novel formalizatio（408KB） | 开放获取 | -- | 请求全文 | |||
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论