Here is a formal specification of the requested circuit. (I hope I got it right). Notation: Signals vary in time, so we denote by A[t] the value of signal A in clock cycle t. For the sake of specification, we assume that all the propagation delays are zero. This assumption implies that *all* signals are stable during a clock cycle (provided that the inputs are stable during each clock cycle) Definitions: Define FP'[t] to be the derivative of FP[t], namely: FP'[t]=1 if and only if FP[t]=1 and FP[t-1]=0. Define the synchronization events: syn1[t]=1 iff FP'[t]=1 and FD[t:t+3]=1010 and syn2[t]=1 iff FD[t:t+3]=1010 and syn1[t-64]=1 (syn1 means that the frame pulse and the synchronization word are properly aligned. syn2 means that a frame pulse is missing, but only one such pulse is missing - not 2 consecutive pulses.) define: syn[t] = syn1[t] or syn2[t] Specification: Now the lock signal is specified as follows: lock[t+1]=1 if and only if exists t' such that 1. 3 < t-t' < 64+3 and 2. syn[t']=1 Remarks: 1. no initialization or reset signal is required. The circuit may initially output lock=1 by mistake, but this will fix itself after at most 64 cycles. If you find this terribly unaesthetic, you may add a reset signal. This will complicate your design a bit. 2. a somewhat more aggressive approach is to reset lock (i.e. set it to zero) as soon as possible if the synchronization word is wrong. What I mean is that if you can prove in cycle t that lock should be zero in cycle t+1, t+2, t+3, or t+4, then you already set lock to zero. No need to worry about this point. 3. The specification refers to lock[t+1] because we want lock to be an output of a register. That means that the circuit will function as if the propagation delays are zero (if the clock period is long enough) without having to rely on the properties of the circuit that uses the lock signal.