15-398 Bug Catching: Automated ProgramVerification and TestingHomework AssignmentOctober 18, 20021. The following SMV code models a simple in-order pipeline stage. Such apipeline stage is part of all modern microprocessors. The instructions of aprogram are processed as a car in an assembly line.The signal that indicates that an instruction moves into the next stage iscalled update enable signal. The instruction in this next stage is overwritten,unless it also moves. This update enable signal is used as clock signal forthe registers of the next stage.The module of the stage takes the following parameters: The parameterfirst is set if the stage is the first stage. This allows injection of new in-structions. The parameter prev ue is the update enable (i.e., clock) signalof the previous stage. The parameter next stall is the stall signal of thenext stage. The stall signals allow stopping the execution in arbitrary stages.A reason for such a stall condition might be slow external memory (or, incase of the assembly line, that a worker dropped his screw driver).MODULE simple_stage(first, prev_ue, next_stall)VARfull : boolean;i_stall: boolean;ASSIGNinit(full):=first;next(full):=prev_ue | stall | first;DEFINE1ue:=full & !stall;stall:=(i_stall | next_stall) & full;The module has two state variables: the variable full indicates that thereis an instruction in the stage. If it is not set, the stage is empty. The vari-able i stall allows nondeterministic stalls within the stage, as describedabove.Describe - informally - the behavior of one stage.2. The stages can be composed to a five stage pipeline as follows:MODULE mainVARstage0: simple_stage(1, 0, stage1.stall);stage1: simple_stage(0, stage0.ue, stage2.stall);stage2: simple_stage(0, stage1.ue, stage3.stall);stage3: simple_stage(0, stage2.ue, stage4.stall);stage4: simple_stage(0, stage3.ue, 0);2stage1.fullstage2.fullstage3.fullstagen.fullstage0.fullFormalize and verify the following properties:• Liveness: Eventually, every stage will be clocked (i.e., the updateenable signal is active) infinitely often. In order to verify this claim,you have to make an assumption. What is the assumption? What goeswrong without it? How does this compare to the assembly line?• Nothing is overwritten: If the instruction in a given stage is over-written, it simultaneously moves into the next stage. For which stagesdoes this hold? Make the comparison with the assembly line!• Nothing is lost: If an instruction does not move into the next stage, itwill be in the same stage in the next cycle.• Nothing is duplicated: If an instruction in a given stage moves intothe next stage, and no instruction moves into the given stage, the givenstage will be empty in the next cycle.• No instruction appears without reason: Any stage - other than stage0 - is not full until an instruction moves into the stage.33. The model of the bus protocol presented in the class is available on the classhome page. Add a special node that is not communicating initially, but hasno power. Later on, after the node is powered on, it tries to synchronizewith the nodes that are already running. This process is called integration.• Extend the control automaton by a state no power and a state in-tegrating.• The automaton is initialized with the state no power.• If in the state no power, the node can stay there or go into the stateintegrating. This is chosen nondeterministically.• If in the state integrating, the node watches the bus. Upon activ-ity, the node goes into the busy state.• Formalize (and verify) the following property: If the node gets power,it will be in the busy state eventually.• This requires help from the other nodes. Why? How can you ensurethis help as part of the implementation, i.e., without a fairness