Define semantics of vhsub.

1 files changed, 27 insertions, 0 deletions

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 0d21322..2baf39d 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -2,6 +2,7 @@
 
 module Helium.Instructions where
 
+open import Data.Bool
 open import Data.Fin
 open import Data.Nat
 open import Data.Sum
@@ -37,3 +38,29 @@ module VAdd
   elem*esize≡32 record { size = zero }             = refl
   elem*esize≡32 record { size = (suc zero) }       = refl
   elem*esize≡32 record { size = (suc (suc zero)) } = refl
+
+module VHSub
+  where
+
+  record VHSub : Set where
+    field
+      unsigned : Bool
+      size : Fin 3
+      dest : VecReg
+      src₁ : VecReg
+      src₂ : GenReg ⊎ VecReg
+
+  esize : VHSub → Fin 33
+  esize record { size = zero }             = # 8
+  esize record { size = (suc zero) }       = # 16
+  esize record { size = (suc (suc zero)) } = # 32
+
+  elements : VHSub → Fin 5
+  elements record { size = zero }             = # 4
+  elements record { size = (suc zero) }       = # 2
+  elements record { size = (suc (suc zero)) } = # 1
+
+  elem*esize≡32 : ∀ d → toℕ (elements d) * toℕ (esize d) ≡ 32
+  elem*esize≡32 record { size = zero }             = refl
+  elem*esize≡32 record { size = (suc zero) }       = refl
+  elem*esize≡32 record { size = (suc (suc zero)) } = refl