NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library multi_mul_prg

Require Import machine_int.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition multi_mul (k one a b c z t i j l atmp btmp ctmp : reg) :=
  addiu i r0 zero16;
  addiu t c zero16;
  while.while (bne i k) (
    addiu z t zero16;
    lwxs atmp i a;
    addiu j r0 zero16;
    while.while (bne j k) (
      lwxs btmp j b;
      maddu atmp btmp;
      addu l i j;
      lwxs ctmp l c;
      maddu ctmp one;
      mflhxu ctmp;
      sw ctmp zero16 z;
      addiu z z four16;
      addiu j j one16);
    mflhxu ctmp;
    sw ctmp zero16 z;
    addiu t t four16;
    addiu i i one16).