1. 模型定义
　　根据同步时序电路的行为特点，可以定义一个模型M = (S, I, O, s₀, TF, OF, clk)，称之为同步有限状态模型。设B代表通常的布尔域，即B = {TRUE, FALSE}，其中：
　　S 是B的幂，表示状态机的所有状态，S = B^ns，其中 s₁, s₂, …, s_ns 是相应的状态变量。
　　I 是B的幂，表示状态机的输入，I = Bⁿⁱ，其中 i₁, i₂, …, i_ni 是相应的输入变量。
　　O 是B的幂，表示状态机的输出，O = Bno，其中 o₁, o₂, …, o_no 是相应的输出变量。
　　s₀ ∈ S， 表示状态机的初始状态。
　　TF: S×I → S: TF = {tf₁, tf₂, …, tf_ns}, TF 表示状态转换函数，其中tf_i: S×I → B 是状态变量 s_i 的转换函数。
　　OF: S×I → O: OF = {of₁, of₂, …, of_ns}, OF 表示输出函数，其中of_i: S×I → B 是输出变量 o_i 的输出函数。
　　clk 是同步有限状态机的全局时钟。
　　对于每一个 tf 和 of，都有一个显式的同步时钟 (clk)，表明状态或输出的改变只能发生在时钟跳变之时。本章限于只有一个同步时钟的情况，在不会混淆的情况下，下面模型的表达式中省略clk一项。
　　同步时序电路模型与一般时序电路模型的不同点在于：（1）同步模型中，时钟作为显示指定的特殊信号，在tf和of中不显式包含时钟信号。（2）同步模型中，只有与时钟有关的变量才形成状态变量，而与时钟无关的变量会消去，形成组合电路部分。