aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v8
-rw-r--r--mppa_k1c/Asmblock.v10
-rw-r--r--mppa_k1c/Asmblockdeps.v2
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml11
-rw-r--r--mppa_k1c/TargetPrinter.ml4
5 files changed, 26 insertions, 9 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index ee3fd198..3e4e4db7 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -138,8 +138,9 @@ 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 *)
+ | Pnandw (rd rs1 rs2: ireg) (**r nand word *)
| Porw (rd rs1 rs2: ireg) (**r or word *)
+ | Pnorw (rd rs1 rs2: ireg) (**r nor word *)
| Pxorw (rd rs1 rs2: ireg) (**r xor word *)
| Psraw (rd rs1 rs2: ireg) (**r shift right arithmetic word *)
| Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
@@ -167,8 +168,9 @@ 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 *)
+ | Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *)
| Poriw (rd rs: ireg) (imm: int) (**r or imm word *)
+ | Pnoriw (rd rs: ireg) (imm: int) (**r nor imm word *)
| Pxoriw (rd rs: ireg) (imm: int) (**r xor imm word *)
| Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
@@ -263,6 +265,7 @@ Definition basic_to_instruction (b: basic) :=
| 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.Pnorw rd rs1 rs2 => Pnorw rd rs1 rs2
| PArithRRR Asmblock.Pxorw rd rs1 rs2 => Pxorw rd rs1 rs2
| PArithRRR Asmblock.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
| PArithRRR Asmblock.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
@@ -291,6 +294,7 @@ Definition basic_to_instruction (b: basic) :=
| 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.Pnoriw rd rs imm => Pnoriw rd rs imm
| PArithRRI32 Asmblock.Pxoriw rd rs imm => Pxoriw rd rs imm
| PArithRRI32 Asmblock.Psraiw rd rs imm => Psraiw rd rs imm
| PArithRRI32 Asmblock.Psrliw rd rs imm => Psrliw rd rs imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index ca9a96a5..66878a94 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -338,8 +338,9 @@ Inductive arith_name_rrr : Type :=
| Psubw (**r sub word *)
| Pmulw (**r mul word *)
| Pandw (**r and word *)
- | Pnandw (**r and word *)
+ | Pnandw (**r nand word *)
| Porw (**r or word *)
+ | Pnorw (**r nor word *)
| Pxorw (**r xor word *)
| Psraw (**r shift right arithmetic word *)
| Psrlw (**r shift right logical word *)
@@ -368,8 +369,9 @@ Inductive arith_name_rri32 : Type :=
| Paddiw (**r add imm word *)
| Pandiw (**r and imm word *)
- | Pnandiw (**r and imm word *)
+ | Pnandiw (**r nand imm word *)
| Poriw (**r or imm word *)
+ | Pnoriw (**r nor imm word *)
| Pxoriw (**r xor imm word *)
| Psraiw (**r shift right arithmetic imm word *)
| Psrliw (**r shift right logical imm word *)
@@ -1095,6 +1097,7 @@ Definition arith_eval_rrr n v1 v2 :=
| Pandw => Val.and v1 v2
| Pnandw => Val.notint (Val.and v1 v2)
| Porw => Val.or v1 v2
+ | Pnorw => Val.notint (Val.or v1 v2)
| Pxorw => Val.xor v1 v2
| Psrlw => Val.shru v1 v2
| Psraw => Val.shr v1 v2
@@ -1123,8 +1126,9 @@ 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))
+ | Pnandiw => Val.notint (Val.and v (Vint i))
| Poriw => Val.or v (Vint i)
+ | Pnoriw => Val.notint (Val.or v (Vint i))
| Pxoriw => Val.xor v (Vint i)
| Psraiw => Val.shr v (Vint i)
| Psrliw => Val.shru v (Vint i)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 499b0d66..0694c22f 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1302,6 +1302,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
| Pandw => "Pandw"
| Pnandw => "Pnandw"
| Porw => "Porw"
+ | Pnorw => "Pnorw"
| Pxorw => "Pxorw"
| Psraw => "Psraw"
| Psrlw => "Psrlw"
@@ -1330,6 +1331,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
| Pandiw => "Pandiw"
| Pnandiw => "Pnandiw"
| Poriw => "Poriw"
+ | Pnoriw => "Pnoriw"
| Pxoriw => "Pxoriw"
| Psraiw => "Psraiw"
| Psrliw => "Psrliw"
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 791936f3..c674bf3e 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -63,6 +63,7 @@ let arith_rrr_str = function
| Pandw -> "Pandw"
| Pnandw -> "Pnandw"
| Porw -> "Porw"
+ | Pnorw -> "Pnorw"
| Pxorw -> "Pxorw"
| Psraw -> "Psraw"
| Psrlw -> "Psrlw"
@@ -89,6 +90,7 @@ let arith_rri32_str = function
| Pandiw -> "Pandiw"
| Pnandiw -> "Pnandiw"
| Poriw -> "Poriw"
+ | Pnoriw -> "Pnoriw"
| Pxoriw -> "Pxoriw"
| Psraiw -> "Psraiw"
| Psrliw -> "Psrliw"
@@ -380,7 +382,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
+ | Nandw | Norw
| Make | Nop | Sxwd | Zxwd
(* LSU *)
| Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -406,6 +408,7 @@ let ab_inst_to_real = function
| "Pmulw" -> Mulw
| "Pmull" -> Muld
| "Porw" | "Poriw" -> Orw
+ | "Pnorw" | "Pnoriw" -> Norw
| "Porl" | "Poril" -> Ord
| "Psubw" | "Pnegw" -> Sbfw
| "Psubl" | "Pnegl" -> Sbfd
@@ -469,7 +472,7 @@ let ab_inst_to_real = function
| "Pfmuld" -> Fmuld
| "Pfmulw" -> Fmulw
| s -> failwith @@ sprintf "ab_inst_to_real: unrecognized instruction: %s" s
-
+
exception InvalidEncoding
let rec_to_usage r =
@@ -479,7 +482,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 | Nandw | Orw | Sbfw | Xorw ->
+ | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw ->
(match encoding with None | Some U6 | Some S10 -> alu_tiny
| Some U27L5 | Some U27L10 -> alu_tiny_x
| _ -> raise InvalidEncoding)
@@ -532,7 +535,7 @@ 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 | Nandw
+ | Rorw | Nandw | Norw
| 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 9ab09866..07663074 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -374,6 +374,8 @@ module Target (*: TARGET*) =
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
+ | Pnorw (rd, rs1, rs2) ->
+ fprintf oc " norw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Pxorw (rd, rs1, rs2) ->
fprintf oc " xorw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
| Psraw (rd, rs1, rs2) ->
@@ -426,6 +428,8 @@ module Target (*: TARGET*) =
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
+ | Pnoriw (rd, rs, imm) ->
+ fprintf oc " norw %a = %a, %a\n" ireg rd ireg rs coqint imm
| Pxoriw (rd, rs, imm) ->
fprintf oc " xorw %a = %a, %a\n" ireg rd ireg rs coqint imm
| Psraiw (rd, rs, imm) ->
generated by cgit (git 2.34.1) at 2024-07-04 14:10:05 +0000