blob: 2baf39df377e22a370a164537c0fc3238d5ef274 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
{-# OPTIONS --safe --without-K #-}
module Helium.Instructions where
open import Data.Bool
open import Data.Fin
open import Data.Nat
open import Data.Sum
open import Relation.Binary.PropositionalEquality
GenReg : Set
GenReg = Fin 16
VecReg : Set
VecReg = Fin 8
module VAdd
where
record VAdd : Set where
field
size : Fin 3
dest : VecReg
src₁ : VecReg
src₂ : GenReg ⊎ VecReg
esize : VAdd → Fin 33
esize record { size = zero } = # 8
esize record { size = (suc zero) } = # 16
esize record { size = (suc (suc zero)) } = # 32
elements : VAdd → 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 VHSub
where
record VHSub : Set where
field
unsigned : Bool
size : Fin 3
dest : VecReg
src₁ : VecReg
src₂ : GenReg ⊎ VecReg
esize : VHSub → Fin 33
esize record { size = zero } = # 8
esize record { size = (suc zero) } = # 16
esize record { size = (suc (suc zero)) } = # 32
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
|
