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.