|
1 (* Title: HOL/Datatype_Benchmark/Verilog.thy |
|
2 |
|
3 Example from Daryl: a Verilog grammar. |
|
4 *) |
|
5 |
|
6 theory Verilog imports Main begin |
|
7 |
|
8 datatype |
|
9 Source_text |
|
10 = module string "string list" "Module_item list" |
|
11 | Source_textMeta string |
|
12 and |
|
13 Module_item |
|
14 = "declaration" Declaration |
|
15 | initial Statement |
|
16 | always Statement |
|
17 | assign Lvalue Expression |
|
18 | Module_itemMeta string |
|
19 and |
|
20 Declaration |
|
21 = reg_declaration "Range option" "string list" |
|
22 | net_declaration "Range option" "string list" |
|
23 | input_declaration "Range option" "string list" |
|
24 | output_declaration "Range option" "string list" |
|
25 | DeclarationMeta string |
|
26 and |
|
27 Range = range Expression Expression | RangeMeta string |
|
28 and |
|
29 Statement |
|
30 = clock_statement Clock Statement_or_null |
|
31 | blocking_assignment Lvalue Expression |
|
32 | non_blocking_assignment Lvalue Expression |
|
33 | conditional_statement |
|
34 Expression Statement_or_null "Statement_or_null option" |
|
35 | case_statement Expression "Case_item list" |
|
36 | while_loop Expression Statement |
|
37 | repeat_loop Expression Statement |
|
38 | for_loop |
|
39 Lvalue Expression Expression Lvalue Expression Statement |
|
40 | forever_loop Statement |
|
41 | disable string |
|
42 | seq_block "string option" "Statement list" |
|
43 | StatementMeta string |
|
44 and |
|
45 Statement_or_null |
|
46 = statement Statement | null_statement | Statement_or_nullMeta string |
|
47 and |
|
48 Clock |
|
49 = posedge string |
|
50 | negedge string |
|
51 | clock string |
|
52 | ClockMeta string |
|
53 and |
|
54 Case_item |
|
55 = case_item "Expression list" Statement_or_null |
|
56 | default_case_item Statement_or_null |
|
57 | Case_itemMeta string |
|
58 and |
|
59 Expression |
|
60 = plus Expression Expression |
|
61 | minus Expression Expression |
|
62 | lshift Expression Expression |
|
63 | rshift Expression Expression |
|
64 | lt Expression Expression |
|
65 | leq Expression Expression |
|
66 | gt Expression Expression |
|
67 | geq Expression Expression |
|
68 | logeq Expression Expression |
|
69 | logneq Expression Expression |
|
70 | caseeq Expression Expression |
|
71 | caseneq Expression Expression |
|
72 | bitand Expression Expression |
|
73 | bitxor Expression Expression |
|
74 | bitor Expression Expression |
|
75 | logand Expression Expression |
|
76 | logor Expression Expression |
|
77 | conditional Expression Expression Expression |
|
78 | positive Primary |
|
79 | negative Primary |
|
80 | lognot Primary |
|
81 | bitnot Primary |
|
82 | reducand Primary |
|
83 | reducxor Primary |
|
84 | reducor Primary |
|
85 | reducnand Primary |
|
86 | reducxnor Primary |
|
87 | reducnor Primary |
|
88 | primary Primary |
|
89 | ExpressionMeta string |
|
90 and |
|
91 Primary |
|
92 = primary_number Number |
|
93 | primary_IDENTIFIER string |
|
94 | primary_bit_select string Expression |
|
95 | primary_part_select string Expression Expression |
|
96 | primary_gen_bit_select Expression Expression |
|
97 | primary_gen_part_select Expression Expression Expression |
|
98 | primary_concatenation Concatenation |
|
99 | primary_multiple_concatenation Multiple_concatenation |
|
100 | brackets Expression |
|
101 | PrimaryMeta string |
|
102 and |
|
103 Lvalue |
|
104 = lvalue string |
|
105 | lvalue_bit_select string Expression |
|
106 | lvalue_part_select string Expression Expression |
|
107 | lvalue_concatenation Concatenation |
|
108 | LvalueMeta string |
|
109 and |
|
110 Number |
|
111 = decimal string |
|
112 | based "string option" string |
|
113 | NumberMeta string |
|
114 and |
|
115 Concatenation |
|
116 = concatenation "Expression list" | ConcatenationMeta string |
|
117 and |
|
118 Multiple_concatenation |
|
119 = multiple_concatenation Expression "Expression list" |
|
120 | Multiple_concatenationMeta string |
|
121 and |
|
122 meta |
|
123 = Meta_Source_text Source_text |
|
124 | Meta_Module_item Module_item |
|
125 | Meta_Declaration Declaration |
|
126 | Meta_Range Range |
|
127 | Meta_Statement Statement |
|
128 | Meta_Statement_or_null Statement_or_null |
|
129 | Meta_Clock Clock |
|
130 | Meta_Case_item Case_item |
|
131 | Meta_Expression Expression |
|
132 | Meta_Primary Primary |
|
133 | Meta_Lvalue Lvalue |
|
134 | Meta_Number Number |
|
135 | Meta_Concatenation Concatenation |
|
136 | Meta_Multiple_concatenation Multiple_concatenation |
|
137 |
|
138 end |