|
| This Article | ||
| | ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
Formal Methods in Computer Aided Design (FMCAD'06)
San Jose, California, USA
November 12-November 16
ISBN: 0-7695-2707-8
| ASCII Text | x | ||
| Julien Schmaltz, "A Formal Model of Lower System Layers," Formal Methods in Computer Aided Design, pp. 191-192, Formal Methods in Computer Aided Design (FMCAD'06), 2006. | |||
| BibTex | x | ||
| @article{ 10.1109/FMCAD.2006.1, author = {Julien Schmaltz}, title = {A Formal Model of Lower System Layers}, journal ={Formal Methods in Computer Aided Design}, volume = {0}, year = {2006}, isbn = {0-7695-2707-8}, pages = {191-192}, doi = {http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.1}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Formal Methods in Computer Aided Design TI - A Formal Model of Lower System Layers SN - 0-7695-2707-8 SP191 EP192 A1 - Julien Schmaltz, PY - 2006 KW - null VL - 0 JA - Formal Methods in Computer Aided Design ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.1
We present a formal model of the bit transmission between registers with arbitrary clock periods. Our model considers precise timing parameters, as well as metastability. We formally define the behavior of registers over time. From that definition, we prove, under certain conditions, that data are properly transmitted. We discuss how to incorporate the model in a purely digital model. The hypotheses of our main theorem define conditions that must be satisfied by the purely digital part of the system to preserve correctness.
Citation:
Julien Schmaltz, "A Formal Model of Lower System Layers," fmcad, pp.191-192, Formal Methods in Computer Aided Design (FMCAD'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.