```// -----------------------------------------------------------------------------
// 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
// -----------------------------------------------------------------------------

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[i]
for(i=0..l-1)
if(P[P[i]]==i) // i and P[i] are connected in depth 0
if(i<=P[i])
// C[i] is min of input[i] and input[P[i]]
C[i] = input[i] & input[P[i]];
else
// C[i] is max of input[i] and input[P[i]]
C[i] = input[i] | input[P[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;
P = 2;
P = 1;
P = 4;
P = 3;
// depth 1
P = 1;
P = 0;
P = 4;
P = 3;
P = 2;
// depth 2
P = 0;
P = 4;
P = 3;
P = 2;
P = 1;
// depth 3
P = 2;
P = 3;
P = 0;
P = 1;
P = 4;
// depth 4
P = 3;
P = 2;
P = 1;
P = 0;
P = 4;
}
```