Причина разницы в количестве достижимых состояний

Я проверяю 8-битный сумматор с помощью этого кода. Когда я печатаю, число доступных состояний равно 1, если основной модуль пуст, и 2^32, если включен весь основной модуль. Что делает эту разницу в сообщаемом количестве достижимых состояний? Для 4-битного сумматора заявленное количество достижимых состояний было 2 ^ 16. Кажется логичным, что входные состояния равны 2^n, если n — количество битов. Откуда берутся все остальные государства? Я заметил, что когда я добавляю строку a : adder (in1, in2);, состояния увеличиваются, но это было только экспериментально проверено, что это то, что увеличивает количество состояний, а не сам модуль сумматора. Почему?

MODULE bit-adder (in1, in2, cin)
VAR
    sum : boolean;
    cout : boolean;
ASSIGN
    next (sum) := (in1 xor in2) xor cin;
    next (cout) := (in1 & in2) | ((in1 | in2) & cin);
MODULE adder (in1, in2)
VAR
    bit0 : bit-adder (in1[0], in2[0], FALSE);
    bit1 : bit-adder (in1[1], in2[1], bit0.cout);
    bit2 : bit-adder (in1[2], in2[2], bit1.cout);
    bit3 : bit-adder (in1[3], in2[3], bit2.cout);
    bit4 : bit-adder (in1[4], in2[4], bit3.cout);
    bit5 : bit-adder (in1[5], in2[5], bit4.cout);
    bit6 : bit-adder (in1[6], in2[6], bit5.cout);
    bit7 : bit-adder (in1[7], in2[7], bit6.cout);
DEFINE
    sum0 := bit0.sum;
    sum1 := bit1.sum;
    sum2 := bit2.sum;
    sum3 := bit3.sum;
    sum4 := bit4.sum;
    sum5 := bit5.sum;
    sum6 := bit6.sum;
    sum7 := bit7.sum;   
    overflow := bit7.cout;
MODULE main
VAR
    in1 : array 0 .. 7 of boolean;
    in2 : array 0 .. 7 of boolean;
    a : adder (in1, in2);
ASSIGN
    next (in1[0]) := in1[0];
    next (in1[1]) := in1[1];
    next (in1[2]) := in1[2];
    next (in1[3]) := in1[3];

    next (in1[4]) := in1[4];
    next (in1[5]) := in1[5];
    next (in1[6]) := in1[6];
    next (in1[7]) := in1[7];


    next (in2[0]) := in2[0];
    next (in2[1]) := in2[1];
    next (in2[2]) := in2[2];
    next (in2[3]) := in2[3];

    next (in2[4]) := in2[4];
    next (in2[5]) := in2[5];
    next (in2[6]) := in2[6];
    next (in2[7]) := in2[7];


DEFINE
    op1 := toint (in1[0]) + 2 * toint (in1[1]) + 4 * toint (in1[2]) + 8 * toint
    (in1[3]) + 16 * toint (in1[4]) + 32 * toint (in1[5]) + 64 * toint (in1[6]) + 128 * toint
    (in1[7]);
    op2 := toint (in2[0]) + 2 * toint (in2[1]) + 4 * toint (in2[2]) + 8 * toint
    (in2[3]) + 16* toint (in2[4]) + 32 * toint (in2[5]) + 64 * toint (in2[6]) + 128 * toint
    (in2[7]);
    sum := toint (a.sum0) + 2 * toint (a.sum1) + 4 * toint (a.sum2) + 8 * toint
    (a.sum3) +16 * toint (a.sum4) + 32 * toint (a.sum5) + 64 * toint (a.sum6) + 128 * toint
    (a.sum7) + 256 * toint (a.overflow);


    LTLSPEC F op1 + op2 = sum

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

Ответы (1)


arrow_upward
1
arrow_downward

Пустой основной модуль. Если вы не включаете (прямо или косвенно) что-то в основной модуль, то это просто игнорируется. Вы можете думать об этом как об определении класса в C++ и никогда не создавать/использовать его где-либо еще: он может быть оптимизирован компилятором, не влияя на выполнение системы.

8-битный сумматор.

nuXmv > print_reachable_states
######################################################################
system diameter: 1
reachable states: 4.29497e+09 (2^32) out of 4.29497e+09 (2^32)
######################################################################

Это мой взгляд на пример:

  • Модуль bit-adder имеет две переменные boolean, обе они свободны и могут принимать любое допустимое значение в домене переменной boolean в зависимости от конкретных входных данных модуля (т. е. значений в in1, in2 и cin). ).

  • Модуль adder имеет восемь подмодулей bit-adder и ряд определенных полей, которые на самом деле не учитываются, когда целью является оценка пространства состояний. Этот модуль не добавляет каких-либо конкретных ограничений на возможные состояния, принимаемые переменными в bit-adders, поэтому единственное, что имеет значение, это то, что объединение восьми bit-adders вместе дает потенциальное пространство 2^16 состояний.

  • Модуль main состоит из одного модуля adder и двух массивов 8-bit, которые моделируют входные данные. Эти входы выбираются произвольно в первом состоянии и навсегда остаются фиксированными, поэтому они добавляют в систему 2^16 возможных начальных состояний. Сам adder всего имеет 2^16 достижимых состояний. Комбинация обоих вещей дает пространство 2^32 состояний.

Дополнение. В приведенном выше выводе nuXmv предупреждает, что диаметр системы составляет всего 1. Это связано с тем, что и sum, и cout могут принимать произвольное значение в начальном состоянии, поэтому для любого выбора in1 и in2 существует по крайней мере одно начальное состояние, в котором значения sum и cout каждого bit-adder в системы совпадают с правильной суммой без каких-либо вычислений. Это явно нереальная натяжка. Лучшим подходом было бы принудительно инициализировать sum и cout значением FALSE:

nuXmv > print_reachable_states 
######################################################################
system diameter: 9
reachable states: 259539 (2^17.9856) out of 4.29497e+09 (2^32)
######################################################################

Вы можете видеть, что на этот раз диаметр системы увеличился до 9. Очевидно, это связано с тем, что в этом очень простом кодировании сумматора цепей carry-bit распространяется вдоль диагонали, и каждый шаг распространения занимает один переход. Количество достижимых состояний также было уменьшено благодаря тому, что мы отказались от некоторых конфигураций, зафиксировав значения cout и sum.

person Patrick Trentin    schedule 08.05.2017