summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Helium/Data/Pseudocode.agda9
-rw-r--r--src/Helium/Instructions.agda35
-rw-r--r--src/Helium/Semantics/Denotational.agda59
-rw-r--r--src/Helium/Semantics/Denotational/Core.agda10
4 files changed, 97 insertions, 16 deletions
diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 5027784..3f82cf0 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -21,9 +21,9 @@ private
record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
infix 9 _^ᶻ_ _^ʳ_
infix 8 _⁻¹
- infix 7 _*ᶻ_ _*ʳ_
+ infixr 7 _*ᶻ_ _*ʳ_
infix 6 -ᶻ_ -ʳ_
- infix 5 _+ᶻ_ _+ʳ_
+ infixr 5 _+ᶻ_ _+ʳ_
infix 4 _≈ᵇ_ _≟ᵇ_ _≈ᶻ_ _≟ᶻ_ _<ᶻ_ _<?ᶻ_ _≈ʳ_ _≟ʳ_ _<ʳ_ _<?ʳ_
field
@@ -150,7 +150,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
(2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ))
where
- open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round
+ open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round public
_>>_ : ℤ → ℕ → ℤ
x >> n = (x div (2ℤ ^ᶻ n)) {2^n≢0 n}
@@ -167,8 +167,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
(*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x)
where
- open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round
- open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0
+ open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 public
sliceᶻ : ∀ n i → ℤ → Bits (n ℕ-ℕ i)
sliceᶻ zero zero z = []
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
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index 2cf1607..bbe69d2 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -8,15 +8,16 @@ module Helium.Semantics.Denotational
where
open import Algebra.Core using (Op₂)
-open import Data.Bool as Bool using (Bool)
+open import Data.Bool as Bool using (Bool; true; false)
open import Data.Fin as Fin hiding (cast; lift; _+_)
import Data.Fin.Properties as Finₚ
open import Data.Maybe using (just; nothing; _>>=_)
open import Data.Nat hiding (_⊔_)
import Data.Nat.Properties as ℕₚ
-open import Data.Product using (∃; _,_; dmap)
+open import Data.Product using (∃; _×_; _,_; dmap)
open import Data.Sum using ([_,_]′)
open import Data.Vec.Functional as V using (Vector)
+open import Function using (_$_)
open import Function.Nary.NonDependent.Base
open import Helium.Instructions
import Helium.Semantics.Denotational.Core as Core
@@ -36,6 +37,7 @@ record State : Set ℓ where
field
S : Vector (Bits 32) 32
R : Vector (Bits 32) 16
+ QC : Bits 1
open Core State
@@ -62,6 +64,12 @@ ElmtMask = Bits 4
&Q : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ VecReg → Expr n Γ Beat → Reference n Γ (Bits 32)
&Q reg beat = &S (λ σ ρ → reg σ ρ >>= λ (σ , reg) → beat σ ρ >>= λ (σ , beat) → just (σ , combine reg beat))
+&FPSCR-QC : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 1)
+&FPSCR-QC = record
+ { get = λ σ ρ → just (σ , State.QC σ)
+ ; set = λ σ ρ x → just (record σ { QC = x } , ρ)
+ }
+
-- Reference properties
&cast : ∀ {k m n ls} {Γ : Sets n ls} → .(eq : k ≡ m) → Reference n Γ (Bits k) → Reference n Γ (Bits m)
@@ -116,6 +124,30 @@ copy-masked dest = for 4 (lift (
else
skip))
+module fun-sliceᶻ
+ (≈ᶻ-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ʳ
+
+ signedSatQ : ∀ n → Function 1 (ℤ , _) (Bits (suc n) × Bool)
+ signedSatQ n =
+ declare ⦇ true ⦈ $ (
+ if ⦇ (λ i → does (1ℤ << n +ᶻ -ᶻ 1ℤ <?ᶻ i)) (!# 1) ⦈
+ then
+ var (# 1) ≔ ⦇ (1ℤ << n +ᶻ -ᶻ 1ℤ) ⦈
+ else if ⦇ (λ i → does (-ᶻ 1ℤ << n <?ᶻ i)) (!# 1) ⦈
+ then
+ var (# 1) ≔ ⦇ (-ᶻ 1ℤ << n) ⦈
+ else
+ var (# 0) ≔ ⦇ false ⦈) ∙
+ return ⦇ ⦇ (sliceᶻ (suc n) zero) (!# 1) ⦈ , !# 0 ⦈
+
module _
(d : VecOp₂)
where
@@ -148,6 +180,7 @@ module _
where
open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
+ open fun-sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
vadd : VAdd → Procedure 2 (Beat , ElmtMask , _)
vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x +ᶻ uint y))
@@ -173,3 +206,25 @@ module _
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
+
+ vqdmulh : VQDMulH → Procedure 2 (Beat , ElmtMask , _)
+ vqdmulh d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (
+ -- op₁ result beat elmtMask
+ for (toℕ elements) (lift (
+ -- e op₁ result beat elmtMask
+ declare
+ ⦇ (λ x y → (2ℤ *ᶻ sint x *ᶻ sint y +ᶻ rval) >> toℕ esize)
+ (! 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₂) ⦈ $
+ declare ⦇ false ⦈ $
+ -- sat value e op₁ result beat elmtMask
+ elem (toℕ esize) (&cast (sym e*e≡32) (var (# 4))) (!# 2) ,′ var (# 0) ≔
+ call (signedSatQ (toℕ esize-1)) (!# 1) ∙
+ if !# 0 then if ⦇ (λ m e → hasBit (combine e zero) (cast (sym e*e>>3≡4) m)) (!# 6) (!# 2) ⦈ then &FPSCR-QC ≔ ⦇ 1b ⦈ else skip else skip
+ )) ∙
+ ignore (call (copy-masked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
+ where
+ open VQDMulH d
+ rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 8c1e231..bbddc57 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -95,9 +95,17 @@ wknRef &x = record
; set = λ σ (v , ρ) x → Reference.set &x σ ρ x >>= λ (σ , ρ) → just (σ , (v , ρ))
}
+_,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ′ → Reference n Γ (τ × τ′)
+&x ,′ &y = record
+ { get = λ σ ρ → Reference.get &x σ ρ >>= λ (σ , x) → Reference.get &y σ ρ >>= λ (σ , y) → just (σ , (x , y))
+ ; set = λ σ ρ (x , y) → Reference.set &x σ ρ x >>= λ (σ , ρ) → Reference.set &y σ ρ y
+ }
+
-- Statements
-infixr 9 _∙_
+infixr 1 _∙_
+infix 4 _≔_
+infixl 2 if_then_else_
skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ
skip cont = cont
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 05:50:32 +0000