Build formal model of UART in NuSMV?

Question

I'm learning model-checking and NuSMV for my education. I can edit and run NuSMV code and I have a fair understanding of what UART is and does.

My task is to formally model UART with NuSMV but at this time I'm not sure how to do it. I understand that UART transmits one byte as eight sequential bits but how can I model that?

I have a mutex code as a starting point:

>NuSMV.exe mutex.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:37:51 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <[email protected]>.
*** Please report bugs to <Please report bugs to <[email protected]>>

*** Copyright (c) 2010-2014, Fondazione Bruno Kessler

*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado

*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson

-- specification EF (state1 = c1 & state2 = c2)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    state1 = n1
    state2 = n2
    turn = 1
-- specification AG (state1 = t1 -> AF state1 = c1)  is true
-- specification AG (state2 = t2 -> AF state2 = c2)  is true

The code

MODULE main


VAR

state1: {n1, t1, c1};

ASSIGN

init(state1) := n1;

next(state1) := 
case
   (state1 = n1) & (state2 = t2): t1;
   (state1 = n1) & (state2 = n2): t1;
   (state1 = n1) & (state2 = c2): t1;
   (state1 = t1) & (state2 = n2): c1;
   (state1 = t1) & (state2 = t2) & (turn = 1):  c1;
   (state1 = c1): n1;
   TRUE : state1;
esac;




VAR

state2: {n2, t2, c2};

ASSIGN

init(state2) := n2;

next(state2) := 
case
   (state2 = n2) & (state1 = t1): t2;
   (state2 = n2) & (state1 = n1): t2;
   (state2 = n2) & (state1 = c1): t2;
   (state2 = t2) & (state1 = n1): c2;
   (state2 = t2) & (state1 = t1) & (turn = 2):  c2;
   (state2 = c2): n2;
   TRUE : state2;
esac;


VAR

turn: {1, 2};

ASSIGN

init(turn) := 1;

next(turn) := 
case
   (state1 = n1) & (state2 = t2): 2;
   (state2 = n2) & (state1 = t1): 1;
   TRUE : turn;
esac;

SPEC

EF((state1 = c1) & (state2 = c2))

SPEC

AG((state1 = t1) -> AF (state1 = c1))

SPEC

AG((state2 = t2) -> AF (state2 = c2))

Answer 1

Before jumping into the smv model, you need to understand at what level of detail you are interested in modeling the UART component. It can be helpful to first model the component in a different formalism, so that you do not get stuck with syntactical issues. What are the inputs of the component? What are the outputs? Is there internal state? How does the internal state change over time and, in particular, in one step?

If you are familiar with hardware description languages (e.g., Verilog and VHDL), this would be a very good starting point, since a transition in SMV can be seen as a clock tick. If you do not know those languages, you can try to write a piece of software instead; this will help you understand input/outputs of the system, but the translation into SMV will not be so immediate.

For components that are very stateful, manually drawing the corresponding automata might help.