2 files changed, 44 insertions, 0 deletions
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
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 5f83fdf..eaaad62 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -168,3 +168,22 @@ module _
     elements = VHSub.elements d
     e*e≡32 = VHSub.elem*esize≡32 d
     int = Bool.if unsigned then uint else sint
+
+  vmul : VMul.VMul → Procedure 2 (Beat , ElmtMask , _)
+  vmul d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (
+    -- op₁ result beat elmtMask
+    for (toℕ elements) (lift (
+      -- e op₁ result beat elmtMask
+      elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔
+      ⦇ (λ x y → sliceᶻ (toℕ esize) zero (sint x *ᶻ sint y))
+        (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0))
+        ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈)
+         , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
+         ]′ src₂) ⦈
+    )) ∙
+    ignore (call (copy-masked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
+    where
+    open VMul.VMul d
+    esize = VMul.esize d
+    elements = VMul.elements d
+    e*e≡32 = VMul.elem*esize≡32 d