2

我用这段代码验证了一个 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
4

1 回答 1

1

空的主模块。如果您没有（直接或间接）在主模块中包含某些内容，那么它会被简单地忽略。你可以把它想象成在 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。

于 2017-05-08T09:00:41.427 回答