Define semantics for vadd.

1 files changed, 39 insertions, 0 deletions

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
new file mode 100644
index 0000000..0d21322
--- /dev/null
+++ b/src/Helium/Instructions.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Instructions where
+
+open import Data.Fin
+open import Data.Nat
+open import Data.Sum
+open import Relation.Binary.PropositionalEquality
+
+GenReg : Set
+GenReg = Fin 16
+
+VecReg : Set
+VecReg = Fin 8
+
+module VAdd
+  where
+
+  record VAdd : Set where
+    field
+      size : Fin 3
+      dest : VecReg
+      src₁ : VecReg
+      src₂ : GenReg ⊎ VecReg
+
+  esize : VAdd → Fin 33
+  esize record { size = zero }             = # 8
+  esize record { size = (suc zero) }       = # 16
+  esize record { size = (suc (suc zero)) } = # 32
+
+  elements : VAdd → 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