diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:28:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-17 17:28:51 +0200 |
| commit | eb3fd167668695c33f776cbb381c7664c3ec1858 (patch) | |
| tree | e7bcfaa9fc18a8755d8fa983d3e8a8d18f1d89f1 /mppa_k1c/Asm.v | |
| parent | 139595171a98e6722503202a2a8fb7c000f267c2 (diff) | |
| download | compcert-kvx-eb3fd167668695c33f776cbb381c7664c3ec1858.tar.gz compcert-kvx-eb3fd167668695c33f776cbb381c7664c3ec1858.zip | |
MPPA - Added Pmull -> now able to run the sort test
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index b2272f7a..f8ab1e8d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -226,6 +226,7 @@ Inductive instruction : Type := | Pandl (rd: ireg) (rs1 rs2: ireg) (**r integer andition *) | Porl (rd: ireg) (rs1 rs2: ireg) (**r or long *) | Pnegl (rd: ireg) (rs: ireg) (**r negate long *) + | Pmull (rd: ireg) (rs1 rs2: ireg) (**r integer mulition long (low part) *) | Pslll (rd: ireg) (rs1 rs2: ireg) (**r shift left logical long *) | Psrll (rd: ireg) (rs1 rs2: ireg) (**r shift right logical long *) | Psral (rd: ireg) (rs1 rs2: ireg) (**r shift right arithmetic long *) @@ -807,6 +808,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.orl rs###s1 rs###s2))) m | Pnegl d s => Next (nextinstr (rs#d <- (Val.negl rs###s))) m + | Pmull d s1 s2 => + Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m | Pslll d s1 s2 => Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m | Psrll d s1 s2 => |