nand is implemented

7 files changed, 39 insertions, 2 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 5ed54a2b..ee3fd198 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -138,6 +138,7 @@ Inductive instruction : Type :=
   | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

   | Pmulw               (rd rs1 rs2: ireg)          (**r mul word *)

   | Pandw               (rd rs1 rs2: ireg)          (**r and word *)

+  | Pnandw              (rd rs1 rs2: ireg)          (**r and word *)

   | Porw                (rd rs1 rs2: ireg)          (**r or word *)

   | Pxorw               (rd rs1 rs2: ireg)          (**r xor word *)

   | Psraw               (rd rs1 rs2: ireg)          (**r shift right arithmetic word *)

@@ -166,6 +167,7 @@ Inductive instruction : Type :=
 

   | Paddiw              (rd rs: ireg) (imm: int)    (**r add imm word *)

   | Pandiw              (rd rs: ireg) (imm: int)    (**r and imm word *)

+  | Pnandiw             (rd rs: ireg) (imm: int)    (**r and imm word *)

   | Poriw               (rd rs: ireg) (imm: int)    (**r or imm word *)

   | Pxoriw              (rd rs: ireg) (imm: int)    (**r xor imm word *)

   | Psraiw              (rd rs: ireg) (imm: int)    (**r shift right arithmetic imm word *)

@@ -259,6 +261,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Psubw rd rs1 rs2       => Psubw rd rs1 rs2

   | PArithRRR Asmblock.Pmulw rd rs1 rs2       => Pmulw rd rs1 rs2

   | PArithRRR Asmblock.Pandw rd rs1 rs2       => Pandw rd rs1 rs2

+  | PArithRRR Asmblock.Pnandw rd rs1 rs2      => Pnandw rd rs1 rs2

   | PArithRRR Asmblock.Porw rd rs1 rs2        => Porw rd rs1 rs2

   | PArithRRR Asmblock.Pxorw rd rs1 rs2       => Pxorw rd rs1 rs2

   | PArithRRR Asmblock.Psraw rd rs1 rs2       => Psraw rd rs1 rs2

@@ -286,6 +289,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm

   | PArithRRI32 Asmblock.Paddiw rd rs imm       => Paddiw rd rs imm

   | PArithRRI32 Asmblock.Pandiw rd rs imm       => Pandiw rd rs imm

+  | PArithRRI32 Asmblock.Pnandiw rd rs imm      => Pnandiw rd rs imm

   | PArithRRI32 Asmblock.Poriw rd rs imm        => Poriw rd rs imm

   | PArithRRI32 Asmblock.Pxoriw rd rs imm       => Pxoriw rd rs imm

   | PArithRRI32 Asmblock.Psraiw rd rs imm       => Psraiw rd rs imm

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 883cfb94..ca9a96a5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -338,6 +338,7 @@ Inductive arith_name_rrr : Type :=
   | Psubw                                           (**r sub word *)
   | Pmulw                                           (**r mul word *)
   | Pandw                                           (**r and word *)
+  | Pnandw                                          (**r and word *)
   | Porw                                            (**r or word *)
   | Pxorw                                           (**r xor word *)
   | Psraw                                           (**r shift right arithmetic word *)
@@ -367,6 +368,7 @@ Inductive arith_name_rri32 : Type :=
 
   | Paddiw                                          (**r add imm word *)
   | Pandiw                                          (**r and imm word *)
+  | Pnandiw                                         (**r and imm word *)
   | Poriw                                           (**r or imm word *)
   | Pxoriw                                          (**r xor imm word *)
   | Psraiw                                          (**r shift right arithmetic imm word *)
@@ -1091,6 +1093,7 @@ Definition arith_eval_rrr n v1 v2 :=
   | Psubw  => Val.sub  v1 v2
   | Pmulw  => Val.mul  v1 v2
   | Pandw  => Val.and  v1 v2
+  | Pnandw => Val.notint (Val.and v1 v2)
   | Porw   => Val.or   v1 v2
   | Pxorw  => Val.xor  v1 v2
   | Psrlw  => Val.shru v1 v2
@@ -1120,6 +1123,7 @@ Definition arith_eval_rri32 n v i :=
   | Pcompiw c => compare_int c v (Vint i)
   | Paddiw  => Val.add   v (Vint i)
   | Pandiw  => Val.and   v (Vint i)
+  | Pnandiw => Val.notint(Val.and   v (Vint i))
   | Poriw   => Val.or    v (Vint i)
   | Pxoriw  => Val.xor   v (Vint i)
   | Psraiw  => Val.shr   v (Vint i)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 19fca6c1..499b0d66 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1300,6 +1300,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Psubw => "Psubw"
   | Pmulw => "Pmulw"
   | Pandw => "Pandw"
+  | Pnandw => "Pnandw"
   | Porw => "Porw"
   | Pxorw => "Pxorw"
   | Psraw => "Psraw"
@@ -1327,6 +1328,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
     Pcompiw _ => "Pcompiw"
   | Paddiw => "Paddiw"
   | Pandiw => "Pandiw"
+  | Pnandiw => "Pnandiw"
   | Poriw => "Poriw"
   | Pxoriw => "Pxoriw"
   | Psraiw => "Psraiw"
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 26b1c6c1..12dabd88 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -86,6 +86,7 @@ Definition opimm32 (op: arith_name_rrr)
 
 Definition addimm32 := opimm32 Paddw Paddiw.
 Definition andimm32 := opimm32 Pandw Pandiw.
+Definition nandimm32 := opimm32 Pnandw Pnandiw.
 Definition orimm32  := opimm32 Porw Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
 (*
@@ -434,6 +435,12 @@ Definition transl_op
   | Oandimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (andimm32 rd rs n ::i k)
+  | Onand, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pnandw rd rs1 rs2 ::i k)
+  | Onandimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (nandimm32 rd rs n ::i k)
   | Oor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porw rd rs1 rs2 ::i k)
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 4627dd09..791936f3 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -61,6 +61,7 @@ let arith_rrr_str = function
   | Psubw -> "Psubw"
   | Pmulw -> "Pmulw"
   | Pandw -> "Pandw"
+  | Pnandw -> "Pnandw"
   | Porw -> "Porw"
   | Pxorw -> "Pxorw"
   | Psraw -> "Psraw"
@@ -86,6 +87,7 @@ let arith_rri32_str = function
   | Pcompiw it -> "Pcompiw"
   | Paddiw -> "Paddiw"
   | Pandiw -> "Pandiw"
+  | Pnandiw -> "Pnandiw"
   | Poriw -> "Poriw"
   | Pxoriw -> "Pxoriw"
   | Psraiw -> "Psraiw"
@@ -378,6 +380,7 @@ type real_instruction =
   (* ALU *) 
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
+  | Nandw                                                                 
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -394,6 +397,7 @@ let ab_inst_to_real = function
   | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
   | "Paddl" | "Paddil" | "Pmv" | "Pmvw2l" -> Addd
   | "Pandw" | "Pandiw" -> Andw
+  | "Pnandw" | "Pnandiw" -> Nandw
   | "Pandl" | "Pandil" -> Andd
   | "Pcompw" | "Pcompiw" -> Compw
   | "Pcompl" | "Pcompil" -> Compd
@@ -475,7 +479,7 @@ let rec_to_usage r =
                                   (* I do not know yet in which context Ofslow can be used by CompCert *)
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
-  | Addw | Andw | Orw | Sbfw | Xorw -> 
+  | Addw | Andw | Nandw | Orw | Sbfw | Xorw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
@@ -527,7 +531,8 @@ let rec_to_usage r =
 
 let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
-  | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw | Rorw
+  | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
+  | Rorw | Nandw
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
   | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 810808c2..9ab09866 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -370,6 +370,8 @@ module Target (*: TARGET*) =
          fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pandw (rd, rs1, rs2) ->
          fprintf oc "	andw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pnandw (rd, rs1, rs2) ->
+         fprintf oc "	nandw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Porw (rd, rs1, rs2) -> 
          fprintf oc "	orw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pxorw (rd, rs1, rs2) -> 
@@ -420,6 +422,8 @@ module Target (*: TARGET*) =
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pandiw (rd, rs, imm) ->
          fprintf oc "	andw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Pnandiw (rd, rs, imm) ->
+         fprintf oc "	nandw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Poriw (rd, rs, imm) -> 
          fprintf oc "	orw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pxoriw (rd, rs, imm) -> 
diff --git a/test/monniaux/nand/nand.c b/test/monniaux/nand/nand.c
index 002c2368..bcd30396 100644
--- a/test/monniaux/nand/nand.c
+++ b/test/monniaux/nand/nand.c
@@ -1,3 +1,14 @@
+#include <stdio.h>
+
 unsigned not(unsigned x) {
   return ~x;
 }
+
+unsigned nand(unsigned x, unsigned y) {
+  return ~(x & y);
+}
+
+int main() {
+  unsigned x = 0xF4, y = 0x33;
+  printf("%X\n", nand(x, y));
+}