diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 2 |
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
|