Consider a clocked device with one input and output. These I$/$O bits are low initially,

until the input is found to be high at the beginning of a clock cycle. After that the output

stays high. Using bounded model checking, prove that the output does not go high at any

time within $5$ clock cycles unless the input goes high. A couple of hints:

a$)$ Construct Q$,$ a proposition which expresses the transitions in a system and $P,$

some property that we want to check.

b$)$ Show that the statement, $"$If Q is true, then P must be false" is false.

c$)$ Review slides related to SBSAT models and state machines

Submit an SBSAT file for the above, and your state machine.