Weak precongruence, a new model of device compliance

摘要

Weak precongruence is a formal property that improves upon the previously-reported congruent weak conformance. Both properties capture the desired relationship between a specification model and its implementation, but congruent weak conformance required both models to be initially stable. Weak precongruence relaxes this requirement, allowing instabilities in either model as long as those instabilities are shared by the other. By treating instability more accurately, weak precongruence displays a greater similarity to Milner's classical property of observational equivalence. Like congruent weak conformance, weak precongruence tolerates unspecified behavior in the unreachable state space, provides greater flexibility in design than previous properties, and can be useful for validating transformational systems, such as logic synthesis and hardware description language translation systems. This paper presents weak precongruence in terms of six formal laws, and discusses the intuitive notions governing them.