Formal Model of MOS Clocking Disciples

Abstract

This paper presents a formalization of clocking disciplines used to prevent race conditions in VLSI circuits. A signal-labeling scheme for the two-phase clocking discipline informally described in Mead and Conway [MC] is presented. Rules are given for checking the correct labeling of a circuit consisting of combinatorial logic and memory elements. The signal-labeling conventions are based in part on those of Noice, Mathews, and Newkirk [NMN]. A formal basis is presented for constructing signal-labeling schemes for multi-phase clocks (both overlapping and non-overlapping) from a definition of the master timing signals. The two-phase scheme is shown to be a special case of this general method. The method is also illustrated for four-phase overlapping clocks.