Added double comparisons

1 files changed, 2 insertions, 0 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 49f2d23c..31bc855d 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -132,6 +132,7 @@ Inductive instruction : Type :=
   | Pcompw  (it: itest) (rd rs1 rs2: ireg)          (**r comparison word *)

   | Pcompl  (it: itest) (rd rs1 rs2: ireg)          (**r comparison long *)

   | Pfcompw (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float *)

+  | Pfcompl (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float64 *)

 

   | Paddw               (rd rs1 rs2: ireg)          (**r add word *)

   | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

@@ -253,6 +254,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2

   | PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2

   | PArithRRR (Asmblock.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2

+  | PArithRRR (Asmblock.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2

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

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

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