From bfcbca52a117ec207addf629f1cada93e0f12e02 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 13 Feb 2022 14:01:44 +0000 Subject: Refactor to group instruction definitions together --- src/Helium/Data/Pseudocode.agda | 317 -------------------------------------- src/Helium/Instructions.agda | 96 ------------ src/Helium/Instructions/Base.agda | 317 ++++++++++++++++++++++++++++++++++++++ src/Helium/Instructions/Core.agda | 96 ++++++++++++ 4 files changed, 413 insertions(+), 413 deletions(-) delete mode 100644 src/Helium/Data/Pseudocode.agda delete mode 100644 src/Helium/Instructions.agda create mode 100644 src/Helium/Instructions/Base.agda create mode 100644 src/Helium/Instructions/Core.agda (limited to 'src') diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda deleted file mode 100644 index 9f936f2..0000000 --- a/src/Helium/Data/Pseudocode.agda +++ /dev/null @@ -1,317 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Definition of instructions using the Armv8-M pseudocode. ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -module Helium.Data.Pseudocode where - -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.Vec as Vec using (Vec; []; _∷_) -open import Data.Vec.Relation.Unary.All using (All; []; _∷_) -open import Function using (_$_) -open import Helium.Data.Pseudocode.Core as Core public - hiding (module Code) -import Helium.Instructions as Instr -import Relation.Binary.PropositionalEquality as P -open import Relation.Nullary.Decidable.Core using (True) - ---- Types - -beat : Type -beat = fin 4 - -elmtMask : Type -elmtMask = bits 4 - ---- State - -State : Vec Type _ -State = array (bits 32) 32 -- S - ∷ array (bits 32) 16 -- R - ∷ bits 16 -- VPR-P0 - ∷ bits 8 -- VPR-mask - ∷ bit -- FPSCR-QC - ∷ bool -- _AdvanceVPTState - ∷ beat -- _BeatId - ∷ [] - -open Core.Code State public - ---- References - --- Direct from State - -S : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 32) -S = state 0 - -R : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 16) -R = state 1 - -VPR-P0 : ∀ {n Γ} → Expression {n} Γ (bits 16) -VPR-P0 = state 2 - -VPR-mask : ∀ {n Γ} → Expression {n} Γ (bits 8) -VPR-mask = state 3 - -FPSCR-QC : ∀ {n Γ} → Expression {n} Γ bit -FPSCR-QC = state 4 - -AdvanceVPTState : ∀ {n Γ} → Expression {n} Γ bool -AdvanceVPTState = state 5 - -BeatId : ∀ {n Γ} → Expression {n} Γ beat -BeatId = state 6 - --- Indirect - -group : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* suc m)) → Expression Γ (array (asType t k) (suc m)) -group {k = k} zero x = [ cast (P.trans (ℕₚ.*-comm k 1) (ℕₚ.+-comm k 0)) x ] -group {k = k} (suc m) x = group m (slice x′ (lit (Fin.fromℕ k ′f))) ∶ [ slice (cast (ℕₚ.+-comm k _) x′) (lit (zero ′f)) ] - where - x′ = cast (P.trans (ℕₚ.*-comm k _) (P.cong (k ℕ.+_) (ℕₚ.*-comm _ k))) x - -join : ∀ {n Γ t k m} → Expression {n} Γ (array (asType t k) (suc m)) → Expression Γ (asType t (k ℕ.* suc m)) -join {k = k} {zero} x = cast (P.trans (ℕₚ.+-comm 0 k) (ℕₚ.*-comm 1 k)) (unbox x) -join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶ unbox (slice {i = suc m} (cast (ℕₚ.+-comm 1 _) x) (lit (zero ′f)))) - where - eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k) - -index : ∀ {n Γ t m} → Expression {n} Γ (asType t (suc m)) → Expression Γ (fin (suc m)) → Expression Γ (elemType t) -index {t = bits} {m} x i = slice (cast (ℕₚ.+-comm 1 m) x) i -index {t = array _} {m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i) - -Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8) -Q = group 7 S - -elem : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* m)) → Expression Γ (fin k) → Expression Γ (asType t m) -elem {k = zero} m x i = abort i -elem {k = suc k} zero x i = cast (ℕₚ.*-comm k 0) x -elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc m)) x)) i - ---- Other utiliies - -hasBit : ∀ {n Γ m} → Expression {n} Γ (bits (suc m)) → Expression Γ (fin (suc m)) → Expression Γ bool -hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x) - -sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m) -sliceⁱ {m = zero} n i = lit ([] ′x) -sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i - ---- Functions - -Int : ∀ {n} → Function (bits n ∷ bool ∷ []) int -Int = skip ∙return (if var 1 then uint (var 0) else sint (var 0)) - --- arguments swapped, pred n -SignedSatQ : ∀ n → Function (int ∷ []) (tuple 2 (bits (suc n) ∷ bool ∷ [])) -SignedSatQ n = declare (lit (true ′b)) ( - if max >3 (tup (var 3 ∷ []))) - then - FPSCR-QC ≔ lit ((true ∷ []) ′x) - else skip)))) ∙ - -- 0:op₁ 1:result 2:elmtMask 3:curBeat - invoke copyMasked (tup (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ [])))) - ∙end)) - where - open Instr.VecOp₂ d - -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat - op₂ = - [ (λ src₂ → index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f))) - , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4))) (var 0)) - ]′ src₂ - - e*esize>>3 : All Fin (toℕ elements ∷ []) → Fin 4 - e*esize>>3 (x ∷ []) = helper size x - where - helper : ∀ size → Fin′ (Instr.Size.elements size) → Fin 4 - helper Instr.8bit i = Fin.combine i (zero {0}) - helper Instr.16bit i = Fin.combine i (zero {1}) - helper Instr.32bit i = Fin.combine i zero - -vqdmulh : Instr.VQDMulH → Procedure [] -vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> toℕ esize) - where open Instr.VecOp₂ d using (esize) - -vqrdmulh : Instr.VQRDMulH → Procedure [] -vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize) - where open Instr.VecOp₂ d using (esize; esize-1) diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda deleted file mode 100644 index ebe3f32..0000000 --- a/src/Helium/Instructions.agda +++ /dev/null @@ -1,96 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Definitions of a subset of Armv8-M instructions. ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -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.Sum -open import Relation.Binary.PropositionalEquality - -GenReg : Set -GenReg = Fin 16 - -VecReg : Set -VecReg = Fin 8 - -data VecOpSize : Set where - 8bit : VecOpSize - 16bit : VecOpSize - 32bit : VecOpSize - -module Size (size : VecOpSize) where - elements-1 : Fin 4 - elements-1 = helper size - where - helper : VecOpSize → Fin 4 - helper 8bit = # 3 - helper 16bit = # 1 - helper 32bit = # 0 - - elements : Fin 5 - elements = suc elements-1 - - esize-1 : Fin 32 - esize-1 = helper size - where - helper : VecOpSize → Fin 32 - helper 8bit = # 7 - helper 16bit = # 15 - helper 32bit = # 31 - - esize : Fin 33 - esize = suc esize-1 - -record VecOp₂ : Set where - field - size : VecOpSize - dest : VecReg - src₁ : VecReg - src₂ : GenReg ⊎ VecReg - - open Size size public - -VAdd = VecOp₂ - -VSub = VecOp₂ - -record VHSub : Set where - field - op₂ : VecOp₂ - unsigned : Bool - - open VecOp₂ op₂ public - -VMul = VecOp₂ - -record VMulH : Set where - field - op₂ : VecOp₂ - unsigned : Bool - - open VecOp₂ op₂ public - -record VRMulH : Set where - field - op₂ : VecOp₂ - unsigned : Bool - - open VecOp₂ op₂ public - -VQDMulH = VecOp₂ -VQRDMulH = VecOp₂ - -data Instruction : Set where - vadd : VAdd → Instruction - vsub : VSub → Instruction - vmul : VMul → Instruction - vmulh : VMulH → Instruction - vqdmulh : VQDMulH → Instruction diff --git a/src/Helium/Instructions/Base.agda b/src/Helium/Instructions/Base.agda new file mode 100644 index 0000000..8ec4073 --- /dev/null +++ b/src/Helium/Instructions/Base.agda @@ -0,0 +1,317 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definition of instructions using the Armv8-M pseudocode. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Instructions.Base where + +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.Vec as Vec using (Vec; []; _∷_) +open import Data.Vec.Relation.Unary.All using (All; []; _∷_) +open import Function using (_$_) +open import Helium.Data.Pseudocode.Core as Core public + hiding (module Code) +import Helium.Instructions.Core as Instr +import Relation.Binary.PropositionalEquality as P +open import Relation.Nullary.Decidable.Core using (True) + +--- Types + +beat : Type +beat = fin 4 + +elmtMask : Type +elmtMask = bits 4 + +--- State + +State : Vec Type _ +State = array (bits 32) 32 -- S + ∷ array (bits 32) 16 -- R + ∷ bits 16 -- VPR-P0 + ∷ bits 8 -- VPR-mask + ∷ bit -- FPSCR-QC + ∷ bool -- _AdvanceVPTState + ∷ beat -- _BeatId + ∷ [] + +open Core.Code State public + +--- References + +-- Direct from State + +S : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 32) +S = state 0 + +R : ∀ {n Γ} → Expression {n} Γ (array (bits 32) 16) +R = state 1 + +VPR-P0 : ∀ {n Γ} → Expression {n} Γ (bits 16) +VPR-P0 = state 2 + +VPR-mask : ∀ {n Γ} → Expression {n} Γ (bits 8) +VPR-mask = state 3 + +FPSCR-QC : ∀ {n Γ} → Expression {n} Γ bit +FPSCR-QC = state 4 + +AdvanceVPTState : ∀ {n Γ} → Expression {n} Γ bool +AdvanceVPTState = state 5 + +BeatId : ∀ {n Γ} → Expression {n} Γ beat +BeatId = state 6 + +-- Indirect + +group : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* suc m)) → Expression Γ (array (asType t k) (suc m)) +group {k = k} zero x = [ cast (P.trans (ℕₚ.*-comm k 1) (ℕₚ.+-comm k 0)) x ] +group {k = k} (suc m) x = group m (slice x′ (lit (Fin.fromℕ k ′f))) ∶ [ slice (cast (ℕₚ.+-comm k _) x′) (lit (zero ′f)) ] + where + x′ = cast (P.trans (ℕₚ.*-comm k _) (P.cong (k ℕ.+_) (ℕₚ.*-comm _ k))) x + +join : ∀ {n Γ t k m} → Expression {n} Γ (array (asType t k) (suc m)) → Expression Γ (asType t (k ℕ.* suc m)) +join {k = k} {zero} x = cast (P.trans (ℕₚ.+-comm 0 k) (ℕₚ.*-comm 1 k)) (unbox x) +join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶ unbox (slice {i = suc m} (cast (ℕₚ.+-comm 1 _) x) (lit (zero ′f)))) + where + eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k) + +index : ∀ {n Γ t m} → Expression {n} Γ (asType t (suc m)) → Expression Γ (fin (suc m)) → Expression Γ (elemType t) +index {t = bits} {m} x i = slice (cast (ℕₚ.+-comm 1 m) x) i +index {t = array _} {m} x i = unbox (slice (cast (ℕₚ.+-comm 1 m) x) i) + +Q : ∀ {n Γ} → Expression {n} Γ (array (array (bits 32) 4) 8) +Q = group 7 S + +elem : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* m)) → Expression Γ (fin k) → Expression Γ (asType t m) +elem {k = zero} m x i = abort i +elem {k = suc k} zero x i = cast (ℕₚ.*-comm k 0) x +elem {k = suc k} (suc m) x i = index (group k (cast (ℕₚ.*-comm (suc k) (suc m)) x)) i + +--- Other utiliies + +hasBit : ∀ {n Γ m} → Expression {n} Γ (bits (suc m)) → Expression Γ (fin (suc m)) → Expression Γ bool +hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x) + +sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m) +sliceⁱ {m = zero} n i = lit ([] ′x) +sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i + +--- Functions + +Int : ∀ {n} → Function (bits n ∷ bool ∷ []) int +Int = skip ∙return (if var 1 then uint (var 0) else sint (var 0)) + +-- arguments swapped, pred n +SignedSatQ : ∀ n → Function (int ∷ []) (tuple 2 (bits (suc n) ∷ bool ∷ [])) +SignedSatQ n = declare (lit (true ′b)) ( + if max >3 (tup (var 3 ∷ []))) + then + FPSCR-QC ≔ lit ((true ∷ []) ′x) + else skip)))) ∙ + -- 0:op₁ 1:result 2:elmtMask 3:curBeat + invoke copyMasked (tup (lit (dest ′f) ∷ to32 size (var 1) ∷ var 3 ∷ var 2 ∷ [])))) + ∙end)) + where + open Instr.VecOp₂ d + -- 0:e 1:op₁ 2:result 3:elmtMask 4:curBeat + op₂ = + [ (λ src₂ → index (from32 size (index R (lit (src₂ ′f)))) (lit (zero ′f))) + , (λ src₂ → index (from32 size (index (index Q (lit (src₂ ′f))) (var 4))) (var 0)) + ]′ src₂ + + e*esize>>3 : All Fin (toℕ elements ∷ []) → Fin 4 + e*esize>>3 (x ∷ []) = helper size x + where + helper : ∀ size → Fin′ (Instr.Size.elements size) → Fin 4 + helper Instr.8bit i = Fin.combine i (zero {0}) + helper Instr.16bit i = Fin.combine i (zero {1}) + helper Instr.32bit i = Fin.combine i zero + +vqdmulh : Instr.VQDMulH → Procedure [] +vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> toℕ esize) + where open Instr.VecOp₂ d using (esize) + +vqrdmulh : Instr.VQRDMulH → Procedure [] +vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize) + where open Instr.VecOp₂ d using (esize; esize-1) diff --git a/src/Helium/Instructions/Core.agda b/src/Helium/Instructions/Core.agda new file mode 100644 index 0000000..466a396 --- /dev/null +++ b/src/Helium/Instructions/Core.agda @@ -0,0 +1,96 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definitions of the data for a subset of Armv8-M instructions. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Instructions.Core where + +open import Data.Bool +open import Data.Fin +open import Data.Nat hiding (pred) +open import Data.Product using (∃; _×_; _,_) +open import Data.Sum +open import Relation.Binary.PropositionalEquality + +GenReg : Set +GenReg = Fin 16 + +VecReg : Set +VecReg = Fin 8 + +data VecOpSize : Set where + 8bit : VecOpSize + 16bit : VecOpSize + 32bit : VecOpSize + +module Size (size : VecOpSize) where + elements-1 : Fin 4 + elements-1 = helper size + where + helper : VecOpSize → Fin 4 + helper 8bit = # 3 + helper 16bit = # 1 + helper 32bit = # 0 + + elements : Fin 5 + elements = suc elements-1 + + esize-1 : Fin 32 + esize-1 = helper size + where + helper : VecOpSize → Fin 32 + helper 8bit = # 7 + helper 16bit = # 15 + helper 32bit = # 31 + + esize : Fin 33 + esize = suc esize-1 + +record VecOp₂ : Set where + field + size : VecOpSize + dest : VecReg + src₁ : VecReg + src₂ : GenReg ⊎ VecReg + + open Size size public + +VAdd = VecOp₂ + +VSub = VecOp₂ + +record VHSub : Set where + field + op₂ : VecOp₂ + unsigned : Bool + + open VecOp₂ op₂ public + +VMul = VecOp₂ + +record VMulH : Set where + field + op₂ : VecOp₂ + unsigned : Bool + + open VecOp₂ op₂ public + +record VRMulH : Set where + field + op₂ : VecOp₂ + unsigned : Bool + + open VecOp₂ op₂ public + +VQDMulH = VecOp₂ +VQRDMulH = VecOp₂ + +data Instruction : Set where + vadd : VAdd → Instruction + vsub : VSub → Instruction + vmul : VMul → Instruction + vmulh : VMulH → Instruction + vqdmulh : VQDMulH → Instruction -- cgit v1.2.3