Carl Pixley提出了时序电路等价性的有关理论和若干概念。包括门级模型（Gate Level Model, GLM）的概念，硬件有限状态机（Hardware Finite State Machine, HFSM），商机（quotient machine），状态等价（state equivalence），alignability，resetability，essential resetability，同形，以及时序电路的等价性。该理论考虑了下面两点：1）在给电路加电时，有限状态机的初始状态是无法控制的；2）只能根据两个设计的网表和逻辑设备模型来判别是否等价，而不能设定初始状态。C.Pixley还提出了一种基于BDD的方法来计算上面所定义的各种性质。
　　如果两个电路都具有外加reset状态s₁和s₂，则两个电路的等价当且仅当s₁和s₂等价。这种等价称为reset等价（reset equivalence）。
　　对于没有外加reset状态的电路而言，如何定义两个电路等价是一个值得研究的问题。对于某些电路而言，必须要用一个同步时序（synchronizing sequence）来驱动电路达到一个预定状态，然后才能正常工作。C.Pixley的等价性定义是只考虑同步后的电路行为是否等价。如果两个电路在同步化之后的行为相同，则认为这两个电路是等价的，至于它们的到达同步的同步时序是否相同则无关紧要。这种等价我们称为同步后等价（post-synchronization equivalence）。因此，只要给定了同步时序，则同步后等价的验证就简化为reset等价验证。
　　此后，C.Pixley等又提出了一种新的等价定义，称为可安全替换（safe replaceability）的等价。对于任意的输入序列，该定义要求替换电路中的每个状态在原电路中都存在一个一致的状态，使得对于这个特定的输入序列，具有相同的输出响应。对于嵌入式电路而言，当无法得到同步时序时，这种等价性定义就比较安全和比较严格。由于要对电路的每个状态进行检查，因此要判别这种等价性是比较困难的。但如果可以表示为BDD方式的话，则仍是可行的。
　　S.Y.Huang等对于没有reset状态的电路，提出了电路覆盖（circuit covering）的时序电路等价定义。在这种定义中，每个触发器的初始值都设定为不确定(u)。对于外加的任意输入时序，采用三值的逻辑模拟得到原始输出的响应，如果替换电路的输出响应均覆盖原电路的输出响应，则认为替换电路覆盖了原电路。