CODEWITHSUNDEEP
hardwareformal-verificationmodel-checkingnusmv
Niklas Rosencrantz
Niklas Rosencrantz

Reputation: 26647

Reason for difference in number of reachable states

I verify an 8-bit adder with this code. When I print the number of reachable states are 1 if the main module is empty and 2^32 if the entire main module is included. What makes this difference in reported number of reachable states? For a 4-bit adder the reported number of reachable states were 2^16. It seems logical that the input states are 2^n if n is the number of bits. Where do all the other states come from? I noticed it is when I add the line a : adder (in1, in2); that the states increase, but that was only experimentally verified that this is what increasese the number of states and not the adder module itself. Why?

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

Upvotes: 2

Views: 127

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

Empty Main Module. If you don't include (directly or indirectly) something in the main module, then it is simply ignored. You can think of it like defining a class in C++ and never instantiating/using it anywhere else: it can be optimised away by the compiler without affecting the execution of the system.

8-bit adder.

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

This is my take on the example:

  • Module bit-adder has two boolean variables, both of these are free to take any legal value in the domain of a boolean variable, depending on the specific inputs of the Module (i.e. the values in in1, in2 and cin).

  • Module adder has eight bit-adder sub-modules and a number of defined fields, which don't really count when the purpose is to estimate the state space. This module does not add any particular constraint on the possible states assumed by the variables in the bit-adders, so the only thing that matters is that by combining eight bit-adders together it has a potential space of 2^16 states.

  • Module main has one adder module and two 8-bit arrays which model the inputs. These inputs are arbitrarily chosen in the first state and remain fixed forever, so they add 2^16 possible initial states to the system. The adder itself overall has 2^16 reachable states. The combination of both things yields a space of 2^32 states.

Addendum. In the above output, nuXmv warns you that the system diameter is only 1. This is due to the fact that both sum and cout can assume an arbitrary value in the initial state, so for any choice of in1 and in2, there exists at least one initial state in which the values of sum and cout of each bit-adder in the system coincide with the correct sum, without any computation being necessary. This is obviously an unrealistic stretch. A better approach would be to force both sum and cout being initialised to FALSE:

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

You can see that this time around the system diameter has increased to 9. This is obviously due to the fact that in this very simple encoding of a circuit adder the carry-bit is propagated along the diagonal, and each propagation step takes one transition. The number of reachable states has also been reduced thanks to the fact we have discarded some configurations by fixing the values of cout and sum.

Upvotes: 1

Related Questions