From ef9f0202c1acae915f02ee2b39ab92981f800297 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 21 Dec 2021 11:37:20 +0000
Subject: Define semantics for vmulh.

---
 src/Helium/Instructions.agda           | 30 +++++++++++++++++++++---------
 src/Helium/Semantics/Denotational.agda | 12 ++++++++++++
 2 files changed, 33 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 1fa2829..1ff17a0 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -4,7 +4,7 @@ module Helium.Instructions where
 
 open import Data.Bool
 open import Data.Fin
-open import Data.Nat
+open import Data.Nat hiding (pred)
 open import Data.Product using (∃; _,_)
 open import Data.Sum
 open import Relation.Binary.PropositionalEquality
@@ -22,19 +22,23 @@ record VecOp₂ : Set where
     src₁ : VecReg
     src₂ : GenReg ⊎ VecReg
 
-  split32 : ∃ λ (elements : Fin 5) → ∃ λ (esize : Fin 33) → toℕ elements * toℕ esize ≡ 32
-  split32 = helper size
-    where
-    helper : _ → _
-    helper zero             = # 4 , # 8 , refl
-    helper (suc zero)       = # 2 , # 16 , refl
-    helper (suc (suc zero)) = # 1 , # 32 , refl
+  private
+    split32 : ∃ λ (elements : Fin 5) → ∃ λ (esize-1 : Fin 32) → toℕ elements * toℕ (suc esize-1) ≡ 32
+    split32 = helper size
+      where
+      helper : _ → _
+      helper zero             = # 4 , # 7 , refl
+      helper (suc zero)       = # 2 , # 15 , refl
+      helper (suc (suc zero)) = # 1 , # 31 , refl
 
   elements : Fin 5
   elements with (elmt , _ , _) ← split32 = elmt
 
+  esize-1 : Fin 32
+  esize-1 with (_ , esize-1 , _) ← split32 = esize-1
+
   esize : Fin 33
-  esize with (_ , esize , _) ← split32 = esize
+  esize = suc esize-1
 
   e*e≡32 : toℕ elements * toℕ esize ≡ 32
   e*e≡32 with (_ , _ , eq) ← split32 = eq
@@ -51,3 +55,11 @@ record VHSub : Set where
   open VecOp₂ op₂ public
 
 VMul = VecOp₂
+
+record VMulH : Set where
+  field
+    op₂ : VecOp₂
+    unsigned : Bool
+    rounding : Bool
+
+  open VecOp₂ op₂ public
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 93c784c..2cf1607 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -161,3 +161,15 @@ module _
 
   vmul : VMul → Procedure 2 (Beat , ElmtMask , _)
   vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x *ᶻ sint y))
+
+  vmulh : VMulH → Procedure 2 (Beat , ElmtMask , _)
+  vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x *ᶻ int y +ᶻ rval)))
+    where
+    open VMulH d
+    int = Bool.if unsigned then uint else sint
+    rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
+    2esize = toℕ esize + toℕ esize
+    esize′ = inject+ _ (strengthen esize)
+    eq : ∀ {n} m (i : Fin n) → toℕ i + m ℕ-ℕ inject+ m (strengthen i) ≡ m
+    eq m zero    = refl
+    eq m (suc i) = eq m i
-- 
cgit v1.2.3