From 55e7c3cd0f2c3213bf36a2e6dadc1f26dcb877b5 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 20 Dec 2021 17:52:29 +0000
Subject: Define vmul.

---
 src/Helium/Instructions.agda | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'src/Helium/Instructions.agda')

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 2baf39d..9560cc2 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -64,3 +64,28 @@ module VHSub
   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 VMul
+  where
+
+  record VMul : Set where
+    field
+      size : Fin 3
+      dest : VecReg
+      src₁ : VecReg
+      src₂ : GenReg ⊎ VecReg
+
+  esize : VMul → Fin 33
+  esize record { size = zero }             = # 8
+  esize record { size = (suc zero) }       = # 16
+  esize record { size = (suc (suc zero)) } = # 32
+
+  elements : VMul → 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
-- 
cgit v1.2.3