Ternary Simulation: Refinement of Binary Functions or Abstraction of Real-Time Behaviour?

We prove the equivalence between the ternary circuit model and a notion of intuitionistic stabilization bounds. This formalizes in a mathematically precise way the intuitive understanding of the ternary model as a level intermediate between the static Boolean model and the (discrete) real-time behaviour of circuits. We show that if one takes an intensional view of the ternary model then the delays that have been abstracted away can be completely recovered. Our intensional soundness and completeness theorems imply that the extracted delays are both correct and exact; thus we have developed a framework which unifies ternary simulation and functional timing analysis. Our focus is on the combinational behaviour of gate-level circuits with feedback.