[SOLVED] ECE582 Project 3-Project with NuSMV

Project with NuSMV

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.

1

Tasks:

1. 1)  Read the tutorial of Nusmv 2.5 and learn the syntax, draw the state diagram of above code.
2. 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:

2

1. 1)  Draw state diagram for this model
2. 2)  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 input reg output

clk, sys_reset;

reset, closeDoor, starOven, done; Start, Close, Heat, Error;

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) default:

endcase end

end

always @ (*) begin

{Start, Close, Heat, Error} <= 4’b0100; {Start, Close, Heat, Error} <= 4’b0000;

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

endmodule // microwave

Tasks:

1) Understand the design and draw the transition diagram for the design 3

2. 2)  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.
3. 3)  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)
4. 4)  Model the design in NuSMV
5. 5)  Prove/disprove them by the NuSMV package.
6. 6)  Explain why the property is true or false and if the test result meets your expectation.
7. 7)  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;

4