author  wenzelm 
Tue, 24 Jul 2007 19:44:32 +0200  
changeset 23961  9e7e1e309ebd 
parent 22875  9b21fa38a3cf 
child 33695  bec342db1bf4 
permissions  rwrr 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

1 
(* Title: Admin/Benchmarks/HOLdatatype/Verilog.thy 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

3 
*) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

4 

16417  5 
theory Verilog imports Main begin 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

6 

8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

7 
(*  *) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

8 
(* Example from Daryl: a Verilog grammar. *) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

9 
(*  *) 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

10 

8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

11 
datatype 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

12 
Source_text 
7373  13 
= module string "string list" "Module_item list" 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

14 
 Source_textMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

15 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

16 
Module_item 
22875  17 
= "declaration" Declaration 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

18 
 initial Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

19 
 always Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

20 
 assign Lvalue Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

21 
 Module_itemMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

22 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

23 
Declaration 
7373  24 
= reg_declaration "Range option" "string list" 
25 
 net_declaration "Range option" "string list" 

26 
 input_declaration "Range option" "string list" 

27 
 output_declaration "Range option" "string list" 

7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

28 
 DeclarationMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

29 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

30 
Range = range Expression Expression  RangeMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

31 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

32 
Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

33 
= clock_statement Clock Statement_or_null 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

34 
 blocking_assignment Lvalue Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

35 
 non_blocking_assignment Lvalue Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

36 
 conditional_statement 
7373  37 
Expression Statement_or_null "Statement_or_null option" 
38 
 case_statement Expression "Case_item list" 

7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

39 
 while_loop Expression Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

40 
 repeat_loop Expression Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

41 
 for_loop 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

42 
Lvalue Expression Expression Lvalue Expression Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

43 
 forever_loop Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

44 
 disable string 
7373  45 
 seq_block "string option" "Statement list" 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

46 
 StatementMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

47 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

48 
Statement_or_null 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

49 
= statement Statement  null_statement  Statement_or_nullMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

50 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

51 
Clock 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

52 
= posedge string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

53 
 negedge string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

54 
 clock string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

55 
 ClockMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

56 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

57 
Case_item 
7373  58 
= case_item "Expression list" Statement_or_null 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

59 
 default_case_item Statement_or_null 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

60 
 Case_itemMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

61 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

62 
Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

63 
= plus Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

64 
 minus Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

65 
 lshift Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

66 
 rshift Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

67 
 lt Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

68 
 leq Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

69 
 gt Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

70 
 geq Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

71 
 logeq Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

72 
 logneq Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

73 
 caseeq Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

74 
 caseneq Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

75 
 bitand Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

76 
 bitxor Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

77 
 bitor Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

78 
 logand Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

79 
 logor Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

80 
 conditional Expression Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

81 
 positive Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

82 
 negative Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

83 
 lognot Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

84 
 bitnot Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

85 
 reducand Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

86 
 reducxor Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

87 
 reducor Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

88 
 reducnand Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

89 
 reducxnor Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

90 
 reducnor Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

91 
 primary Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

92 
 ExpressionMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

93 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

94 
Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

95 
= primary_number Number 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

96 
 primary_IDENTIFIER string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

97 
 primary_bit_select string Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

98 
 primary_part_select string Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

99 
 primary_gen_bit_select Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

100 
 primary_gen_part_select Expression Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

101 
 primary_concatenation Concatenation 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

102 
 primary_multiple_concatenation Multiple_concatenation 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

103 
 brackets Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

104 
 PrimaryMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

105 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

106 
Lvalue 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

107 
= lvalue string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

108 
 lvalue_bit_select string Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

109 
 lvalue_part_select string Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

110 
 lvalue_concatenation Concatenation 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

111 
 LvalueMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

112 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

113 
Number 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

114 
= decimal string 
7373  115 
 based "string option" string 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

116 
 NumberMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

117 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

118 
Concatenation 
7373  119 
= concatenation "Expression list"  ConcatenationMeta string 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

120 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

121 
Multiple_concatenation 
7373  122 
= multiple_concatenation Expression "Expression list" 
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

123 
 Multiple_concatenationMeta string 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

124 
and 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

125 
meta 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

126 
= Meta_Source_text Source_text 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

127 
 Meta_Module_item Module_item 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

128 
 Meta_Declaration Declaration 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

129 
 Meta_Range Range 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

130 
 Meta_Statement Statement 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

131 
 Meta_Statement_or_null Statement_or_null 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

132 
 Meta_Clock Clock 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

133 
 Meta_Case_item Case_item 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

134 
 Meta_Expression Expression 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

135 
 Meta_Primary Primary 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

136 
 Meta_Lvalue Lvalue 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

137 
 Meta_Number Number 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

138 
 Meta_Concatenation Concatenation 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

139 
 Meta_Multiple_concatenation Multiple_concatenation 
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

140 

8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset

141 
end 