aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/Asm.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-12-07 15:35:20 +0100
committerCyril SIX <cyril.six@kalray.eu>2020-12-07 15:35:20 +0100
commit23da7b35d0edf98f271401ac93a1fa06adb062a2 (patch)
tree036672f28d72d8d583886b2503607ce661825e9b /kvx/Asm.v
parent60ff1e39bac5ab35c46698cbc1ed7a76fc936cab (diff)
downloadcompcert-kvx-23da7b35d0edf98f271401ac93a1fa06adb062a2.tar.gz
compcert-kvx-23da7b35d0edf98f271401ac93a1fa06adb062a2.zip
Fixing test/regression for KVXv3.8_kvx
Diffstat (limited to 'kvx/Asm.v')
-rw-r--r--kvx/Asm.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/kvx/Asm.v b/kvx/Asm.v
index 6d8736af..fd20316c 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -104,6 +104,9 @@ Inductive instruction : Type :=
| Palclrd (dst: ireg) (addr: ireg)
| Palclrw (dst: ireg) (addr: ireg)
| Pclzll (rd rs: ireg)
+ | Pclzw (rd rs: ireg)
+ | Pctzll (rd rs: ireg)
+ | Pctzw (rd rs: ireg)
| Pstsud (rd rs1 rs2: ireg)
(** Loads *)