diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-19 11:42:30 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:08 +0200 |
| commit | 1c1dd8c9cfcc98f183f6844b6c2f4ae60edd165d (patch) | |
| tree | fa2c37098369a22ec7e6150ea7e4ed5fd4e529d3 /mppa_k1c/Asm.v | |
| parent | 734ef70ef9edcd69d822d573628d5f0ca282ddcb (diff) | |
| download | compcert-kvx-1c1dd8c9cfcc98f183f6844b6c2f4ae60edd165d.tar.gz compcert-kvx-1c1dd8c9cfcc98f183f6844b6c2f4ae60edd165d.zip | |
MPPA - Activated Paddw and Paddiw + ops
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 4693975b..42b5f85f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -144,8 +144,8 @@ Inductive instruction : Type := | Pmv (rd: ireg) (rs: ireg) (**r integer move *) (** 32-bit integer register-immediate instructions *) -(*| Paddiw (rd: ireg) (rs: ireg) (imm: int) (**r add immediate *) - | Psltiw (rd: ireg) (rs: ireg) (imm: int) (**r set-less-than immediate *) + | Paddiw (rd: ireg) (rs: ireg) (imm: int) (**r add immediate *) +(*| Psltiw (rd: ireg) (rs: ireg) (imm: int) (**r set-less-than immediate *) | Psltiuw (rd: ireg) (rs: ireg) (imm: int) (**r set-less-than unsigned immediate *) | Pandiw (rd: ireg) (rs: ireg) (imm: int) (**r and immediate *) | Poriw (rd: ireg) (rs: ireg) (imm: int) (**r or immediate *) @@ -155,8 +155,8 @@ Inductive instruction : Type := | Psraiw (rd: ireg) (rs: ireg) (imm: int) (**r shift-right-arith immediate *) | Pluiw (rd: ireg) (imm: int) (**r load upper-immediate *) (** 32-bit integer register-register instructions *) - | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) - | Psubw (rd: ireg) (rs1 rs2: ireg) (**r integer subtraction *) +*)| Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) +(*| Psubw (rd: ireg) (rs1 rs2: ireg) (**r integer subtraction *) | Pmulw (rd: ireg) (rs1 rs2: ireg) (**r integer multiply low *) | Pmulhw (rd: ireg) (rs1 rs2: ireg) (**r integer multiply high signed *) @@ -629,9 +629,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (rs#s))) m (** 32-bit integer register-immediate instructions *) -(*| Paddiw d s i => + | Paddiw d s i => Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m - | Psltiw d s i => +(*| Psltiw d s i => Next (nextinstr (rs#d <- (Val.cmp Clt rs##s (Vint i)))) m | Psltiuw d s i => Next (nextinstr (rs#d <- (Val.cmpu (Mem.valid_pointer m) Clt rs##s (Vint i)))) m @@ -651,9 +651,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Vint (Int.shl i (Int.repr 12))))) m (** 32-bit integer register-register instructions *) - | Paddw d s1 s2 => +*)| Paddw d s1 s2 => Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m - | Psubw d s1 s2 => +(*| Psubw d s1 s2 => Next (nextinstr (rs#d <- (Val.sub rs##s1 rs##s2))) m | Pmulw d s1 s2 => Next (nextinstr (rs#d <- (Val.mul rs##s1 rs##s2))) m |