From 0b581ec922b40284291d6814578bd2e68049c8b7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 21 Dec 2021 15:14:54 +0000
Subject: Define execBeats, a wrapper to execute beat-wise instructions.

---
 src/Helium/Data/Pseudocode.agda             |  6 ++-
 src/Helium/Semantics/Denotational.agda      | 65 +++++++++++++++++++++++++++--
 src/Helium/Semantics/Denotational/Core.agda |  5 ++-
 3 files changed, 70 insertions(+), 6 deletions(-)

(limited to 'src/Helium')

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 3f82cf0..9982501 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -23,7 +23,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
   infix 8 _⁻¹
   infixr 7 _*ᶻ_ _*ʳ_
   infix 6 -ᶻ_ -ʳ_
-  infixr 5 _+ᶻ_ _+ʳ_
+  infixr 5 _+ᶻ_ _+ʳ_ _∶_
   infix 4 _≈ᵇ_ _≟ᵇ_ _≈ᶻ_ _≟ᶻ_ _<ᶻ_ _<?ᶻ_ _≈ʳ_ _≟ʳ_ _<ʳ_ _<?ʳ_
 
   field
@@ -83,6 +83,10 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
   zeros {zero}  = []
   zeros {suc n} = 0b ∶ zeros
 
+  ones : ∀ {n} → Bits n
+  ones {zero}  = []
+  ones {suc n} = 1b ∶ ones
+
   _eor_ : ∀ {n} → Op₂ (Bits n)
   x eor y = (x or y) and not (x and y)
 
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index bbe69d2..fc93a26 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -37,13 +37,27 @@ record State : Set ℓ where
   field
     S : Vector (Bits 32) 32
     R : Vector (Bits 32) 16
+    P0 : Bits 16
+    mask : Bits 8
     QC : Bits 1
+    advanceVPT : Bool
 
 open Core State
 
 Beat : Set
 Beat = Fin 4
 
+hilow : Beat → Fin 2
+hilow zero          = zero
+hilow (suc zero)    = zero
+hilow (suc (suc _)) = suc zero
+
+oddeven : Beat → Fin 2
+oddeven zero                   = zero
+oddeven (suc zero)             = suc zero
+oddeven (suc (suc zero))       = zero
+oddeven (suc (suc (suc zero))) = suc zero
+
 ElmtMask : Set b₁
 ElmtMask = Bits 4
 
@@ -70,6 +84,24 @@ ElmtMask = Bits 4
   ; set = λ σ ρ x → just (record σ { QC = x } , ρ)
   }
 
+&VPR-P0 : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 16)
+&VPR-P0 = record
+  { get = λ σ ρ → just (σ , State.P0 σ)
+  ; set = λ σ ρ x → just (record σ { P0 = x } , ρ)
+  }
+
+&VPR-mask : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 8)
+&VPR-mask = record
+  { get = λ σ ρ → just (σ , State.mask σ)
+  ; set = λ σ ρ x → just (record σ { mask = x } , ρ)
+  }
+
+&AdvanceVPT : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ Bool
+&AdvanceVPT = record
+  { get = λ σ ρ → just (σ , State.advanceVPT σ)
+  ; set = λ σ ρ x → just (record σ { advanceVPT = x } , ρ)
+  }
+
 -- Reference properties
 
 &cast : ∀ {k m n ls} {Γ : Sets n ls} → .(eq : k ≡ m) → Reference n Γ (Bits k) → Reference n Γ (Bits m)
@@ -115,8 +147,8 @@ elem m &v idx = slice &v λ σ ρ → idx σ ρ >>= λ (σ , i) → just (σ , h
 
 -- General functions
 
-copy-masked : VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _)
-copy-masked dest = for 4 (lift (
+copyMasked : VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _)
+copyMasked dest = for 4 (lift (
   -- e result beat elmtMask
   if ⦇ (λ x y → does (getᵇ y x ≟ᵇ 1b)) (!# 3) (!# 0) ⦈
   then
@@ -148,6 +180,31 @@ module fun-sliceᶻ
       var (# 0) ≔ ⦇ false ⦈) ∙
     return ⦇ ⦇ (sliceᶻ (suc n) zero) (!# 1) ⦈ , !# 0 ⦈
 
+advanceVPT : Procedure 1 (Beat , _)
+advanceVPT = declare (! elem 4 &VPR-mask ⦇ hilow (!# 0) ⦈)  $
+  if ⦇ (λ x → does (x ≟ᵇ 1b ∶ 0b ∶ 0b ∶ 0b)) (!# 0) ⦈
+  then
+    var (# 0) ≔ ⦇ zeros ⦈
+  else if ⦇ (λ x → does (x ≟ᵇ zeros {4})) (!# 0) ⦈
+  then skip
+  else
+    (if ⦇ (hasBit (# 3)) (!# 0) ⦈ then
+       elem 4 &VPR-P0 (!# 1) ⟵ not
+     else skip ∙
+     var (# 0) ⟵ λ x → sliceᵇ (# 3) zero x ∶ 0b) ∙
+  if ⦇ (λ x → does (oddeven x Finₚ.≟ # 1)) (!# 1) ⦈
+  then
+    elem 4 &VPR-mask ⦇ hilow (!# 1) ⦈ ≔ !# 0
+  else skip
+
+execBeats : Procedure 2 (Beat , ElmtMask , _) → Procedure 0 _
+execBeats inst = for 4 (lift (
+  declare ⦇ ones ⦈ $
+  if ⦇ (λ x → does (x ≟ᵇ zeros {4})) (! elem 4 &VPR-mask ⦇ hilow (!# 1) ⦈) ⦈ then skip else var (# 0) ≔ ! elem 4 &VPR-P0 (!# 1) ∙
+  &AdvanceVPT ≔ ⦇ true ⦈ ∙
+  ignore (call inst (⦇ !# 1 , !# 0 ⦈)) ∙
+  if ! &AdvanceVPT then ignore (call advanceVPT (!# 1)) else skip))
+
 module _
   (d : VecOp₂)
   where
@@ -166,7 +223,7 @@ module _
          , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0))
          ]′ src₂) ⦈
     )) ∙
-    ignore (call (copy-masked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
+    ignore (call (copyMasked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈)))
 
 -- Instruction semantics
 
@@ -224,7 +281,7 @@ module _
         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 ⦈ ⦈)))
+    ignore (call (copyMasked 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 bbddc57..54f0375 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -104,7 +104,7 @@ _,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ
 -- Statements
 
 infixr 1 _∙_
-infix 4 _≔_
+infix 4 _≔_ _⟵_
 infixl 2 if_then_else_
 
 skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ
@@ -119,6 +119,9 @@ return e _ = e
 _≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Statement n Γ τ′
 (ref ≔ e) cont σ ρ = e σ ρ >>= λ (σ , v) → Reference.set ref σ ρ v >>= λ (σ , v) → cont σ v
 
+_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Statement n Γ τ′
+ref ⟵ e = ref ≔ ⦇ e (! ref) ⦈
+
 label : ∀ {n ls} {Γ : Sets n ls} → smap _ (Reference n Γ) n Γ ⇉ Statement n Γ τ → Statement n Γ τ
 label {n = n} s = uncurry⊤ₙ n s vars
   where
-- 
cgit v1.2.3