可达状态数不同的原因

Question

我用这段代码验证了一个 8 位加法器。当我打印时，如果主模块为空，则可达状态数为 1，如果包含整个主模块，则为 2^32。报告的可达状态数量有何不同？对于 4 位加法器，报告的可达状态数为 2^16。如果 n 是位数，则输入状态为 2^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

Answer 1

空主模块。 如果您没有（直接或间接）在主模块中包含某些内容，那么它将被忽略。你可以把它想象成在 C++ 中定义一个 class 而永远不会在其他任何地方定义它：它可以被编译器 optimised 掉而不影响执行系统.

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子模块和一些定义的字段，当目的是估计状态时这些字段不算数space.该模块不会对 bit-adders 中变量假定的可能状态添加任何特定约束，因此唯一重要的是通过将八个 bit-adders 组合在一起，它具有潜在的 space 2^16 个州。
模块 main 有一个 adder 模块和两个对输入建模的 8-bit 数组。这些输入在第一个状态是任意选择的，并且永远保持固定，因此它们向系统添加 2^16 个可能的初始状态。 adder 本身总体上有 2^16 个可达状态。两者结合产生 space 个 2^32 状态。

附录。 在上面的输出中，nuXmv 警告您 系统直径 是只有 1。这是因为 sum 和 cout 在初始状态下都可以取任意值，所以对于 in1 和 in2 的任意选择，至少存在一种初始状态，其中系统中每个 bit-adder 的 sum 和 cout 的值与正确的和一致，无需任何计算。这显然是不切实际的延伸。更好的方法是强制将 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.

的值丢弃了一些配置，因此可到达状态的数量也减少了

可达状态数不同的原因

Reason for difference in number of reachable states

hardware

model-checking

formal-verification

nusmv