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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
;; GENERATED BY `isaspec`. DO NOT EDIT!!!
(attr MInst.VecRRR (tag isaspec_generated))
(spec
(MInst.VecRRR alu_op rd rn rm size)
(provide
(match
size
((Size8x16)
(match
alu_op
((Addp)
(=
rd
(concat
(bvadd (extract 119 112 rm) (extract 127 120 rm))
(concat
(bvadd (extract 103 96 rm) (extract 111 104 rm))
(concat
(bvadd (extract 87 80 rm) (extract 95 88 rm))
(concat
(bvadd (extract 71 64 rm) (extract 79 72 rm))
(concat
(bvadd (extract 55 48 rm) (extract 63 56 rm))
(concat
(bvadd (extract 39 32 rm) (extract 47 40 rm))
(concat
(bvadd (extract 23 16 rm) (extract 31 24 rm))
(concat
(bvadd (extract 7 0 rm) (extract 15 8 rm))
(concat
(bvadd (extract 119 112 rn) (extract 127 120 rn))
(concat
(bvadd (extract 103 96 rn) (extract 111 104 rn))
(concat
(bvadd (extract 87 80 rn) (extract 95 88 rn))
(concat
(bvadd (extract 71 64 rn) (extract 79 72 rn))
(concat
(bvadd (extract 55 48 rn) (extract 63 56 rn))
(concat
(bvadd (extract 39 32 rn) (extract 47 40 rn))
(concat (bvadd (extract 23 16 rn) (extract 31 24 rn)) (bvadd (extract 7 0 rn) (extract 15 8 rn)))
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
((Size8x8)
(match
alu_op
((Addp)
(=
rd
(zero_ext
128
(concat
(bvadd (extract 55 48 rm) (extract 63 56 rm))
(concat
(bvadd (extract 39 32 rm) (extract 47 40 rm))
(concat
(bvadd (extract 23 16 rm) (extract 31 24 rm))
(concat
(bvadd (extract 7 0 rm) (extract 15 8 rm))
(concat
(bvadd (extract 55 48 rn) (extract 63 56 rn))
(concat
(bvadd (extract 39 32 rn) (extract 47 40 rn))
(concat (bvadd (extract 23 16 rn) (extract 31 24 rn)) (bvadd (extract 7 0 rn) (extract 15 8 rn)))
)
)
)
)
)
)
)
)
)
)
)
)
)
(require (match size ((Size8x16) (match alu_op ((Addp) true))) ((Size8x8) (match alu_op ((Addp) true)))))
)