diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 17:13:41 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 17:13:41 +0200 |
| commit | 9fd4e33a6dd2c2dc88103711af62a7214dbd4109 (patch) | |
| tree | b39d6da151bd4c8d79a8009395afb2b54dbc6860 /mppa_k1c/Asm.v | |
| parent | d407e23fe62ce837082820f777564c0050cf66c1 (diff) | |
| download | compcert-kvx-9fd4e33a6dd2c2dc88103711af62a7214dbd4109.tar.gz compcert-kvx-9fd4e33a6dd2c2dc88103711af62a7214dbd4109.zip | |
Osub and Omul
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index c2f145aa..72bbff69 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -197,6 +197,8 @@ Inductive instruction : Type := (** 32-bit integer register-register instructions *) | Paddw (rd: ireg) (rs1 rs2: ireg) (**r integer addition *) + | Psubw (rd: ireg) (rs1 rs2: ireg) (**r integer subition *) + | Pmulw (rd: ireg) (rs1 rs2: ireg) (**r integer mulition *) | Pandw (rd: ireg) (rs1 rs2: ireg) (**r integer andition *) | Pnegw (rd: ireg) (rs: ireg) (**r negate word *) @@ -740,6 +742,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** 32-bit integer register-register instructions *) | Paddw d s1 s2 => Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m + | 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 | Pandw d s1 s2 => Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m | Pnegw d s => |