From 59948b3348964f4b16f408ffe690f2c78ca80959 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Mar 2019 17:41:27 +0100 Subject: Added double comparisons --- mppa_k1c/Asm.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'mppa_k1c/Asm.v') 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 -- cgit