From 63f9978f448574d4df1ebacec52125a957482260 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 21 Dec 2021 13:41:20 +0000
Subject: Define semantics of vqdmulh.

---
 src/Helium/Instructions.agda | 35 +++++++++++++++++++++++++++--------
 1 file changed, 27 insertions(+), 8 deletions(-)

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

diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 1ff17a0..5eba3f0 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -5,7 +5,7 @@ module Helium.Instructions where
 open import Data.Bool
 open import Data.Fin
 open import Data.Nat hiding (pred)
-open import Data.Product using (∃; _,_)
+open import Data.Product using (∃; _×_; _,_)
 open import Data.Sum
 open import Relation.Binary.PropositionalEquality
 
@@ -23,25 +23,37 @@ record VecOp₂ : Set where
     src₂ : GenReg ⊎ VecReg
 
   private
-    split32 : ∃ λ (elements : Fin 5) → ∃ λ (esize-1 : Fin 32) → toℕ elements * toℕ (suc esize-1) ≡ 32
+    split32 : ∃ λ (elements : Fin 5) → ∃ λ (esize>>3-1 : Fin 4) → ∃ λ (esize-1 : Fin 32) → (8 * toℕ (suc esize>>3-1) ≡ toℕ (suc esize-1)) × (toℕ elements * toℕ (suc esize-1) ≡ 32) × (toℕ elements * toℕ (suc esize>>3-1) ≡ 4)
     split32 = helper size
       where
       helper : _ → _
-      helper zero             = # 4 , # 7 , refl
-      helper (suc zero)       = # 2 , # 15 , refl
-      helper (suc (suc zero)) = # 1 , # 31 , refl
+      helper zero             = # 4 , # 0 , # 7 , refl , refl , refl
+      helper (suc zero)       = # 2 , # 1 , # 15 , refl , refl , refl
+      helper (suc (suc zero)) = # 1 , # 3 , # 31 , refl , refl , refl
 
   elements : Fin 5
-  elements with (elmt , _ , _) ← split32 = elmt
+  elements with (elmt , _ ) ← split32 = elmt
+
+  esize>>3-1 : Fin 4
+  esize>>3-1 with (_ , esize>>3-1 , _) ← split32 = esize>>3-1
+
+  esize>>3 : Fin 5
+  esize>>3 = suc esize>>3-1
 
   esize-1 : Fin 32
-  esize-1 with (_ , esize-1 , _) ← split32 = esize-1
+  esize-1 with (_ , _ , esize-1 , _) ← split32 = esize-1
 
   esize : Fin 33
   esize = suc esize-1
 
+  8*e>>3≡e : 8 * toℕ esize>>3 ≡ toℕ esize
+  8*e>>3≡e with (_ , _ , _ , eq , _) ← split32 = eq
+
   e*e≡32 : toℕ elements * toℕ esize ≡ 32
-  e*e≡32 with (_ , _ , eq) ← split32 = eq
+  e*e≡32 with (_ , _ , _ , _ , eq , _) ← split32 = eq
+
+  e*e>>3≡4 : toℕ elements * toℕ esize>>3 ≡ 4
+  e*e>>3≡4 with (_ , _ , _ , _ , _ , eq) ← split32 = eq
 
 VAdd = VecOp₂
 
@@ -63,3 +75,10 @@ record VMulH : Set where
     rounding : Bool
 
   open VecOp₂ op₂ public
+
+record VQDMulH : Set where
+  field
+    op₂ : VecOp₂
+    rounding : Bool
+
+  open VecOp₂ op₂ public
-- 
cgit v1.2.3