// -----------------------------------------------------------------------------
// The module below checks whether a given permutation matrix P represents a
// correct sorting network. To this end, wires i and j are connected by a
// compare/exchange module at depth k iff P[k][i]=j and P[k][j]=i holds.
// If wire i should not be connected to a compare/exchange module at depth k,
// then P[k][i]=i must hold. Hence, each row of P must be a permutation of
// the numbers 0..L-1. Each of these permutation matrices represents a
// sorting network. By the 0/1-principle, it is sufficient to check the
// correctness for all 1-bit numbers, but this has to be done for all possible
// sequences. Thus, the module enumerates all possible input sequences and
// checks that these are correctly sorted by the sorting network encoded by
// P. For more information see Morgenstern's PhD thesis [Morg10].
// -----------------------------------------------------------------------------

macro d = 5;  // depth of sorting network
macro l = 5;  // size of sequence to be sorted

module SortingNetworks([d][l]nat{l} ?P,bool noperm,unsorted) {
    // enumerate all possible 2^l boolean input sequences
    // and assign them to the local boolean array input
    // that is sorted using the intermediate local values C[k][i]
    // with the same permutation matrix P
    for(x=0..exp(2,l)-1) {    // enumerate all inputs
        event [l]bool input;  // local input array obtained by bitvector x
        event [d][l]bool C; // intermediate value of wires for this input

        // generate local input sequence to be sorted
        for(i=0..l-1)
            input[i] = nat2bv(x,l){i};

        // compute values of wires C[0][i]
        for(i=0..l-1)
            if(P[0][P[0][i]]==i) // i and P[0][i] are connected in depth 0
                if(i<=P[0][i])
                    // C[0][i] is min of input[i] and input[P[0][i]]
                    C[0][i] = input[i] & input[P[0][i]];
                else
                    // C[0][i] is max of input[i] and input[P[0][i]]
                    C[0][i] = input[i] | input[P[0][i]];
            else emit(noperm);
    
        for(k=1..d-1)
            for(i=0..l-1)
                if(P[k][P[k][i]]==i) // i and P[k][i] are connected in depth k
                    if(i<=P[k][i])
                        // C[k][i] is min of C[k-1][i] and C[k-1][P[k][i]]
                        C[k][i] = C[k-1][i] & C[k-1][P[k][i]];
                    else
                        // C[k][i] is max of C[k-1][i] and C[k-1][P[k][i]]
                        C[k][i] = C[k-1][i] | C[k-1][P[k][i]];
                else emit(noperm);

        // check whether input x has been sorted by P
        if(!forall(i=0..l-2) (C[d-1][i] -> C[d-1][i+1]))
            emit(unsorted);
        }
}
satisfies {
    // specification to assure that P is a correct sorting network
    x : assert(!noperm -> unsorted);
}
drivenby {
    // depth 0
    P[0][0] = 0;
    P[0][1] = 2;
    P[0][2] = 1;
    P[0][3] = 4;
    P[0][4] = 3;
    // depth 1
    P[1][0] = 1;
    P[1][1] = 0;
    P[1][2] = 4;
    P[1][3] = 3;
    P[1][4] = 2;
    // depth 2
    P[2][0] = 0;
    P[2][1] = 4;
    P[2][2] = 3;
    P[2][3] = 2;
    P[2][4] = 1;
    // depth 3
    P[3][0] = 2;
    P[3][1] = 3;
    P[3][2] = 0;
    P[3][3] = 1;
    P[3][4] = 4;
    // depth 4
    P[4][0] = 3;
    P[4][1] = 2;
    P[4][2] = 1;
    P[4][3] = 0;
    P[4][4] = 4;
}