Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1016/j.tcs.2011.01.032 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
defining trajectory,netlist structure,formal symbolic trajectory evaluation,STE implementation,formal netlist model,Closure semantics,formal definition,Formal semantics,novel formalization,Symbolic trajectory evaluation,inductive definition,Netlist,Isabelle/HOL,closure state function,symbolic trajectory evaluation semantics,structural netlist circuit model,abstract next state function | Journal | 412 |
Issue | ISSN | Citations |
25 | Theoretical Computer Science | 2 |
PageRank | References | Authors |
0.43 | 12 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yongjian Li | 1 | 37 | 12.27 |
| William N. N. Hung | 2 | 304 | 34.98 |
| Xiaoyu Song | 3 | 57 | 11.26 |