For instance, an inverter with input A and output B, expressed declaratively as predicates of time, can be specified as \[ \forall t . A(t) ~~ \leftrightarrow ~~ \neg B(t) \]
Here the logic levels of the circuit have the same notation as the logic values in the proof system, but an approach where this is not done is not significantly more complicated: \[ \forall t . A(t)==1 ~~ \leftrightarrow ~~ B(t)==0 \]
When time is quantised in units equal to a tick of the global clock then a D-type flip-flop can be expressed: \[ Q(t+1)==x ~~ \leftrightarrow ~~ D(t)==x \] Here we have dropped the implied, leading $\forall t$.
A complex formal specification does not necessarily describe the algorithm and hence logic structure that will be used in the implementation. Therefore, synthesis from formal specification involves a measure of inventiveness on the part of the tool.