in p2 hw6:
we have to verify EFGout
that is EFEGEX(-reset).
i tried to verify EGEX(-reset) first.
^^^^^^^^^^
P
In BMC induction step:
i have to proof unSAT(TR0 & P0 & -P1)
however, P0, P1 can not translate into clause directly.
So,i need to find the set of states that satisfies P0 first.
that is:
SAT((S0==reset)&(TR0)&(S1!=reset))
SAT((S0==idle)&(TR0)&(S1!=reset))
...
after check every state seperately
i found all states satisfied P0.
then i can do unSAT(TR0 & P0 & -P1)
in hw6 this is unSAT so the property has been proofed.
but if it is SAT, i should try unSAT(TR0 & TR1 & P0 & P1 & -P2) in next step.
i found this is similar to greatest fixed point
while P0=R0,
(R0 & (TR0 & P1))=R1 if SAT(R0 & TR0 & -P1) means R1!=R0
^^^^^^^^^^
constraint make next state should still satisfy P
(R1 & (TR1 & P2))=R2
....
what the difference between BMC and greatest fixed point?
or why we don't need a simple path constraint in finding greatest fixed point?