ECE582 Project3-Project with NuSMV Solved

Description

 

Problem 1.

Follow the instructions and prepare yourself for using NuSMV.

 

• nuSMV 2.5.4 Download:

http://nusmv.fbk.eu/NuSMV/download/getting–v2.html ➢ Tutorial:

http://nusmv.fbk.eu/NuSMV/tutorial/

• Install the binary

Run NuSMV from the command line (NOTICE the -int option):

 

./NuSMV -int

NuSMV > help

NuSMV > read_model -h

usage: read_model [-h] [-i <file>] -h Prints the command usage.

-i <file> Reads the model from the specified <file>.

NuSMV > quit

 

Problem 2.

Consider the following example.

 

MODULE main VAR  request : boolean;  state : {ready,busy}; ASSIGN

init(state) := ready;

next(state) := case

state = ready & request : busy;              TRUE : {ready,busy};

esac;

SPEC

AG(request -> AF state = busy)

 

Copy the code above in a text file and call it short.smv. Then, call NuSMV and load this file:

 

NuSMV -int

NuSMV > read_model -i short.smv

NuSMV > flatten_hierarchy

NuSMV > encode_variables

NuSMV > build_model

 

At this point NuSMV is ready to perform simulation and verification. You can verify the formula above with the command check_ctlspec. You can verify more CTL formulas with the command check_ctlspec -p “CTL-formula”. For instance, check whether or not the formula AG(request -> AX(state=busy)) is true.

 

Tasks: 

1) Read the tutorial of Nusmv 2.5 and learn the syntax, draw the state diagram of above code. 2) Come up with 3 more CTL properties and check against the model.

 

Problem 3.

Consider the following 3-bit counter.

 

MODULE counter_cell(carry_in)

VAR

value : boolean;

ASSIGN

init(value) := FALSE;

next(value) := value xor carry_in;

DEFINE

carry_out := value & carry_in;

MODULE main

VAR

bit0 : counter_cell(TRUE); bit1 : counter_cell(bit0.carry_out); bit2 : counter_cell(bit1.carry_out);

 

Without using NuSMV, try to uderstand what the code does (see tutorial).

Copy the code above in a text file and call it counter.smv. Then, call NuSMV and load this file:

./NuSMV -int

NuSMV > read_model -i counter.smv

NuSMV > flatten_hierarchy

NuSMV > encode_variables

NuSMV > build_model

 

At this point NuSMV is ready to perform simulation and verification.

 

Simulation: 

At this point you verify that your understanding of the code was correct. To perform simulation, first you have to select a state from the set of initial states:

 

NuSMV > pick_state -i

(with this command you select a state interactively (-i). As there is only one initial state, you just have to confirm the only option available). The command simulates -i <number> is used to perform simulation. <number> specifies the number of steps you want to simulate, e.g.,

NuSMV > simulate -i 1

The evolution of the system is deterministic. Try a few steps and check that your guess was correct.

 

Verification: 

You can verify CTL formulas with the command check_spec -p “CTL-formula”. For instance, check whether or not the formula AX(bit0.value=0) is true.

 

Tasks:

• Draw state diagram for this model
• Come up with 3 more CTL property and check against above model.

 

Problem 4.  Model checking VS Simulation

Consider the following microwave oven controller design written in Verilog.

 

// Microwave oven

module microwave(clk, sys_reset, reset, closeDoor, starOven, done, States);     input     clk, sys_reset;     input     reset, closeDoor, starOven, done;     reg       Start, Close, Heat, Error;     output    reg [3:0] States;

 

always @ (posedge clk)      begin

if (sys_reset == 1’b1)

begin

{Start, Close, Heat, Error} <= 4’b0000;         end         else         begin             case ({Start, Close, Heat, Error})                 4’b0000:

if      (closeDoor) {Start, Close, Heat, Error} <= 4’b0100;                     else if (starOven)  {Start, Close, Heat, Error} <= 4’b1001;

4’b1001:

if      (closeDoor) {Start, Close, Heat, Error} <= 4’b1101;                  4’b1101:

if      (~closeDoor){Start, Close, Heat, Error} <= 4’b1001;                      else if (reset)     {Start, Close, Heat, Error} <= 4’b0100;                  4’b0100:

if      (~closeDoor){Start, Close, Heat, Error} <= 4’b0000;                      else if (starOven)  {Start, Close, Heat, Error} <= 4’b1100;

4’b1100:                {Start, Close, Heat, Error} <= 4’b1110;

4’b1110:                {Start, Close, Heat, Error} <= 4’b0110;                                      4’b0110:

if      (~closeDoor){Start, Close, Heat, Error} <= 4’b0000;                     else if (done)      {Start, Close, Heat, Error} <= 4’b0100;                 default:                {Start, Close, Heat, Error} <= 4’b0000;             endcase         end

end

 

always @ (*)     begin

States = {Start, Close, Heat, Error};     end

endmodule // microwave

 

Tasks: 

• Understand the design and draw the transition diagram for the design
• Propose 5 new CTL properties. Describe them in English first, then in CTL forms. Your properties should be different from those proposed by other students.
• Create Verilog test benches and run simulation to verify your properties, justify your test result.

(show the test result in script form instead of wave form)

• Model the design in NuSMV
• Prove/disprove them by the NuSMV package.
• Explain why the property is true or false and if the test result meets your expectation.
• Compare the model checking to simulation, and discuss the advantages and disadvantages of the above two verification methods.

 

Sample properties:

• If an error condition occurs, it must be reset before the oven may heat.
• G((Close=0 * Start=1) -> (Error=0 R Heat=0));

 

• The oven can’t be heated if the door is not closed.
• Heat=0 U Close=1;