diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Helium/Instructions/Base.agda | 10 | ||||
| -rw-r--r-- | src/Helium/Instructions/Core.agda | 10 |
2 files changed, 19 insertions, 1 deletions
diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda index 4ea8973..8473d65 100644 --- a/src/Helium/Instructions/Base.agda +++ b/src/Helium/Instructions/Base.agda @@ -12,7 +12,7 @@ open import Data.Bool as Bool using (true; false) open import Data.Fin as Fin using (Fin; Fin′; zero; suc; toℕ) open import Data.Nat as ℕ using (ℕ; zero; suc) import Data.Nat.Properties as ℕₚ -open import Data.Sum using ([_,_]′) +open import Data.Sum using ([_,_]′; inj₂) open import Data.Vec as Vec using (Vec; []; _∷_) open import Data.Vec.Relation.Unary.All using (All; []; _∷_) open import Function using (_$_) @@ -269,6 +269,14 @@ vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) where open Instr.VRMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ [])) +vmla : Instr.VMlA → Procedure [] +vmla d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * element₂ + toInt (var 1))) + where + open Instr.VMlA d + op₂ = record { size = size ; dest = acc ; src₁ = src₁ ; src₂ = inj₂ acc } + toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ [])) + element₂ = toInt (index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f))) + private vqr?dmulh : Instr.VQDMulH → Function (int ∷ int ∷ []) int → Procedure [] vqr?dmulh d f = vec-op₂′ d ( diff --git a/src/Helium/Instructions/Core.agda b/src/Helium/Instructions/Core.agda index 466a396..6c9363d 100644 --- a/src/Helium/Instructions/Core.agda +++ b/src/Helium/Instructions/Core.agda @@ -85,6 +85,16 @@ record VRMulH : Set where open VecOp₂ op₂ public +record VMlA : Set where + field + size : VecOpSize + unsigned : Bool + acc : VecReg + src₁ : VecReg + src₂ : GenReg + + open Size size public + VQDMulH = VecOp₂ VQRDMulH = VecOp₂ |