Построить формальную модель UART в NuSMV?

Я изучаю проверку моделей и NuSMV для своего образования. Я могу редактировать и запускать код NuSMV, и у меня есть четкое представление о том, что такое UART и что он делает.

Моя задача — формально смоделировать UART с помощью NuSMV, но пока я не уверен, как это сделать. Я понимаю, что UART передает один байт в виде восьми последовательных битов, но как мне это смоделировать?

У меня есть код мьютекса в качестве отправной точки:

>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

Код

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

uart formal-verification model-checking nusmv
person Niklas R.    schedule 26.02.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Перед тем, как перейти к модели smv, вам нужно понять, на каком уровне детализации вы заинтересованы в моделировании компонента UART. Может быть полезно сначала смоделировать компонент в другом формализме, чтобы не зацикливаться на синтаксических проблемах. Каковы входы компонента? Каковы результаты? Есть ли внутреннее состояние? Как меняется внутреннее состояние во времени и, в частности, за один шаг?

Если вы знакомы с языками описания оборудования (например, Verilog и VHDL), это будет очень хорошей отправной точкой, поскольку переход в SMV можно рассматривать как такт часов. Если вы не знаете этих языков, вы можете вместо этого попробовать написать программу; это поможет вам понять ввод/вывод системы, но перевод в SMV не будет таким быстрым.

Для компонентов, которые очень зависят от состояния, может помочь ручное рисование соответствующих автоматов.

person Marco    schedule 26.02.2017