diff options
Diffstat (limited to 'src/Helium')
| -rw-r--r-- | src/Helium/Instructions.agda | 94 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational.agda | 85 |
2 files changed, 55 insertions, 124 deletions
diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda index 9560cc2..256f9c4 100644 --- a/src/Helium/Instructions.agda +++ b/src/Helium/Instructions.agda @@ -5,6 +5,7 @@ module Helium.Instructions where open import Data.Bool open import Data.Fin open import Data.Nat +open import Data.Product using (∃; _,_) open import Data.Sum open import Relation.Binary.PropositionalEquality @@ -14,78 +15,37 @@ GenReg = Fin 16 VecReg : Set VecReg = Fin 8 -module VAdd - where +record VecOp₂ : Set where + field + size : Fin 3 + dest : VecReg + src₁ : VecReg + src₂ : GenReg ⊎ VecReg - record VAdd : Set where - field - size : Fin 3 - dest : VecReg - 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 - esize : VAdd → Fin 33 - esize record { size = zero } = # 8 - esize record { size = (suc zero) } = # 16 - esize record { size = (suc (suc zero)) } = # 32 + elements : Fin 5 + elements with (elmt , _ , _) ← split32 = elmt - elements : VAdd → Fin 5 - elements record { size = zero } = # 4 - elements record { size = (suc zero) } = # 2 - elements record { size = (suc (suc zero)) } = # 1 + esize : Fin 33 + esize with (_ , esize , _) ← split32 = esize - 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 + e*e≡32 : toℕ elements * toℕ esize ≡ 32 + e*e≡32 with (_ , _ , eq) ← split32 = eq -module VHSub - where +VAdd = VecOp₂ - record VHSub : Set where - field - unsigned : Bool - size : Fin 3 - dest : VecReg - src₁ : VecReg - src₂ : GenReg ⊎ VecReg +record VHSub : Set where + field + op₂ : VecOp₂ + unsigned : Bool - esize : VHSub → Fin 33 - esize record { size = zero } = # 8 - esize record { size = (suc zero) } = # 16 - esize record { size = (suc (suc zero)) } = # 32 + open VecOp₂ op₂ public - elements : VHSub → 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 - -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 +VMul = VecOp₂ diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index eaaad62..0739d28 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -7,6 +7,7 @@ module Helium.Semantics.Denotational (pseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) where +open import Algebra.Core using (Op₂) open import Data.Bool as Bool using (Bool) open import Data.Fin as Fin hiding (cast; lift; _+_) import Data.Fin.Properties as Finₚ @@ -115,75 +116,45 @@ copy-masked dest = for 4 (lift ( else skip)) --- vec-op₂ : VecReg → GenReg → Op₂ (Bits n) - --- Instruction semantics - module _ - (≈ᶻ-trans : Transitive _≈ᶻ_) - (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) - (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) - (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) - (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ)) - (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x) + (d : VecOp₂) where - open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ + open VecOp₂ d - vadd : VAdd.VAdd → Procedure 2 (Beat , ElmtMask , _) - vadd d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) ( + vec-op₂ : Op₂ (Bits (toℕ esize)) → Procedure 2 (Beat , ElmtMask , _) + vec-op₂ op = 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) ≔ - ⦇ _+ᵇ_ + ⦇ op (! 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 VAdd.VAdd d - esize = VAdd.esize d - elements = VAdd.elements d - e*e≡32 = VAdd.elem*esize≡32 d - vhsub : VHSub.VHSub → Procedure 2 (Beat , ElmtMask , _) - vhsub 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ᶻ (suc (toℕ esize)) (suc zero) (int x +ᶻ -ᶻ int 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 VHSub.VHSub d - esize = VHSub.esize d - 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 +-- Instruction semantics + +module _ + (≈ᶻ-trans : Transitive _≈ᶻ_) + (round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧) + (round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y) + (0#-homo-round : round 0ℝ ≈ᶻ 0ℤ) + (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ)) + (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x) + where + + open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ + + vadd : VAdd → Procedure 2 (Beat , ElmtMask , _) + vadd d = vec-op₂ d _+ᵇ_ + + vhsub : VHSub → Procedure 2 (Beat , ElmtMask , _) + vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ (suc (toℕ esize)) (suc zero) (int x +ᶻ -ᶻ int y)) + where open VHSub d ; int = Bool.if unsigned then uint else sint + + vmul : VMul → Procedure 2 (Beat , ElmtMask , _) + vmul d = vec-op₂ d (λ x y → sliceᶻ (toℕ _) zero (sint x *ᶻ sint y)) |