Translation Validation: Matrix Multiplication (NuSMV, w/loops)¶

Description of the Case Study¶

We investigate a translation-validation benchmark for a C program that performs matrix multiplication (MM). When executed, the high-level C code is compiled into a low-level RTL (Register–Transfer Level) implementation that introduces explicit memory reads/writes. Specifications are triples \(\langle \mathit{Pre},\, \mathit{annot},\, \mathit{Post} \rangle\), where \(\mathit{Pre}\) and \(\mathit{Post}\) are assertions and \(\mathit{annot}\) is a partial function from labels to assertions.

We capture conformance via SIMAE and a HyperLTL constraint \(\varphi_{\mathrm{conf}}\), proving that the translated code satisfies the same specification as the source. We consider two variants:

a correct translation (expected SAT: a SIMAE witness exists), and
an incorrect translation (expected UNSAT).

The NuSMV model(s)¶

MODULE main
VAR
  s : 0..26;

ASSIGN
  init(s) := 0;

  next(s) :=
    case
      s = 0  : 1;
      s = 1  : {2, 26};
      s = 2  : 3;
      s = 3  : 4;
      s = 4  : 5;
      s = 5  : 6;
      s = 6  : {7, 24};
      s = 7  : 8;
      s = 8  : 9;
      s = 9  : 10;
      s = 10 : 11;
      s = 11 : {12, 21};
      s = 12 : 13;
      s = 13 : 14;
      s = 14 : 15;
      s = 15 : {16, 17, 18, 19};
      s = 16 : 20;
      s = 17 : 20;
      s = 18 : 20;
      s = 19 : 20;
      s = 20 : 11;   
      s = 21 : 22;
      s = 22 : 6;   
      s = 24 : 25;
      s = 25 : 1;
      s = 26 : 26;
      TRUE   : s;
    esac;

MODULE main
VAR
  s : 0..26;

ASSIGN
  init(s) := 0;

  next(s) :=
    case
      s = 0  : 1;
      s = 1  : {2, 26};
      s = 2  : 3;
      s = 3  : 4;
      s = 4  : 5;
      s = 5  : 6;
      s = 6  : {7, 24};
      s = 7  : 8;
      s = 8  : 9;
      s = 9  : 10;
      s = 10 : 11;
      s = 11 : {12, 21};
      s = 12 : 13;
      s = 13 : 14;
      s = 14 : 15;
      s = 15 : {16, 17, 18, 19};
      s = 16 : 20;
      s = 17 : 20;
      s = 18 : 20;
      s = 19 : 20;
      s = 20 : 20; 
      s = 21 : 22;
      s = 22 : 6;    
      s = 24 : 25;
      s = 25 : 1;
      s = 26 : 26;
      TRUE   : s;
    esac;

The HyperLTL formula(s)¶

The conformance constraint ties every source trace \(\pi_A\) to some target trace \(\pi_B\) such that their abstract control variable \(s\) remains aligned at all steps.

\[\begin{aligned} \varphi_{\mathrm{conf}} \;=\; \forall \pi_A.\ \exists \pi_B.\ \mathbf{G}\big(s_{\pi_A} = s_{\pi_B}\big). \end{aligned}\]

Forall A . Exists B . G(s[A] = s[B])

References¶

Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Kunz, César; and Pacalet, Anne. “Implementing a direct method for certificate translation.” In International Conference on Formal Engineering Methods (ICFEM 2009), pp. 541–560. Springer, 2009.