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.
展开▼
