ilang  1.1.4
ILAng: A Modeling and Verification Platform for SoCs
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Friends Macros
ast_hub.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_ILA_AST_HUB_H__
5 #define ILANG_ILA_AST_HUB_H__
6 
10 #include <ilang/ila/ast/func.h>
11 
13 namespace ilang {
14 
16 namespace asthub {
17 
19 inline AstUidSort GetUidSort(const ExprPtr& expr) {
20  return expr->sort()->uid();
21 }
22 
24 inline AstUidExprOp GetUidExprOp(const ExprPtr& expr) {
25  return std::dynamic_pointer_cast<ExprOp>(expr)->uid();
26 }
27 
28 /******************************************************************************/
29 // Variable
30 /******************************************************************************/
32 ExprPtr NewBoolVar(const std::string& name);
34 ExprPtr NewBvVar(const std::string& name, const int& bit_width);
36 ExprPtr NewMemVar(const std::string& name, const int& addr_width,
37  const int& data_width);
38 
39 /******************************************************************************/
40 // Constant
41 /******************************************************************************/
43 ExprPtr BoolConst(const bool& val);
45 ExprPtr BoolConst(const BoolVal& val);
47 ExprPtr BvConst(const BvValType& val, const int& bit_width);
49 ExprPtr BvConst(const BvVal& val, const int& bit_width);
51 ExprPtr MemConst(const BvValType& def_val, const int& addr_width,
52  const int& data_width);
54 ExprPtr MemConst(const MemVal& val, const int& addr_width,
55  const int& data_width);
56 
57 /******************************************************************************/
58 // Unary operation
59 /******************************************************************************/
61 ExprPtr Negate(const ExprPtr& obj);
63 ExprPtr Not(const ExprPtr& obj);
65 ExprPtr Complement(const ExprPtr& obj);
66 
67 /******************************************************************************/
68 // Binary operation
69 /******************************************************************************/
71 ExprPtr And(const ExprPtr& l, const ExprPtr& r);
73 ExprPtr Or(const ExprPtr& l, const ExprPtr& r);
75 ExprPtr Xor(const ExprPtr& l, const ExprPtr& r);
77 ExprPtr Shl(const ExprPtr& l, const ExprPtr& r);
79 ExprPtr Ashr(const ExprPtr& l, const ExprPtr& r);
81 ExprPtr Lshr(const ExprPtr& l, const ExprPtr& r);
83 ExprPtr Add(const ExprPtr& l, const ExprPtr& r);
85 ExprPtr Sub(const ExprPtr& l, const ExprPtr& r);
87 ExprPtr Div(const ExprPtr& l, const ExprPtr& r);
89 ExprPtr SRem(const ExprPtr& l, const ExprPtr& r);
91 ExprPtr URem(const ExprPtr& l, const ExprPtr& r);
93 ExprPtr SMod(const ExprPtr& l, const ExprPtr& r);
95 ExprPtr Mod(const ExprPtr& l, const ExprPtr& r);
97 ExprPtr Mul(const ExprPtr& l, const ExprPtr& r);
98 
99 // helper functions for constant arguments
101 ExprPtr And(const ExprPtr& l, const bool& r);
103 ExprPtr Or(const ExprPtr& l, const bool& r);
105 ExprPtr Xor(const ExprPtr& l, const bool& r);
107 ExprPtr Shl(const ExprPtr& l, const int& r);
109 ExprPtr Ashr(const ExprPtr& l, const int& r);
111 ExprPtr Lshr(const ExprPtr& l, const int& r);
113 ExprPtr Add(const ExprPtr& l, const BvValType& r);
115 ExprPtr Sub(const ExprPtr& l, const BvValType& r);
117 ExprPtr Mul(const ExprPtr& l, const BvValType& r);
118 
119 /******************************************************************************/
120 // Comparison
121 /******************************************************************************/
123 ExprPtr Eq(const ExprPtr& l, const ExprPtr& r);
125 ExprPtr Ne(const ExprPtr& l, const ExprPtr& r);
127 ExprPtr Lt(const ExprPtr& l, const ExprPtr& r);
129 ExprPtr Gt(const ExprPtr& l, const ExprPtr& r);
131 ExprPtr Le(const ExprPtr& l, const ExprPtr& r);
133 ExprPtr Ge(const ExprPtr& l, const ExprPtr& r);
135 ExprPtr Ult(const ExprPtr& l, const ExprPtr& r);
137 ExprPtr Ugt(const ExprPtr& l, const ExprPtr& r);
139 ExprPtr Ule(const ExprPtr& l, const ExprPtr& r);
141 ExprPtr Uge(const ExprPtr& l, const ExprPtr& r);
142 
143 // helper functions for constant arguments
144 #if 0
145 ExprPtr Eq(const ExprPtr& l, const bool& r);
147 #endif
148 ExprPtr Eq(const ExprPtr& l, const BvValType& r);
151 ExprPtr Ne(const ExprPtr& l, const BvValType& r);
153 ExprPtr Lt(const ExprPtr& l, const BvValType& r);
155 ExprPtr Gt(const ExprPtr& l, const BvValType& r);
157 ExprPtr Le(const ExprPtr& l, const BvValType& r);
159 ExprPtr Ge(const ExprPtr& l, const BvValType& r);
161 ExprPtr Ult(const ExprPtr& l, const BvValType& r);
163 ExprPtr Ugt(const ExprPtr& l, const BvValType& r);
165 ExprPtr Ule(const ExprPtr& l, const BvValType& r);
167 ExprPtr Uge(const ExprPtr& l, const BvValType& r);
168 
169 /******************************************************************************/
170 // Memory
171 /******************************************************************************/
173 ExprPtr Load(const ExprPtr& mem, const ExprPtr& addr);
175 ExprPtr Store(const ExprPtr& mem, const ExprPtr& addr, const ExprPtr& data);
176 
178 ExprPtr Load(const ExprPtr& mem, const BvValType& addr);
180 ExprPtr Store(const ExprPtr& mem, const BvValType& addr, const BvValType& data);
181 
183 bool SetMemSize(const ExprPtr& mem, const int& size = 0);
185 int GetMemSize(const ExprPtr& mem);
186 
187 /******************************************************************************/
188 // Bit manipulation
189 /******************************************************************************/
191 ExprPtr Concat(const ExprPtr& hi, const ExprPtr& lo);
193 ExprPtr Extract(const ExprPtr& bv, const int& hi, const int& lo);
195 ExprPtr ZExt(const ExprPtr& bv, const int& out_width);
197 ExprPtr SExt(const ExprPtr& bv, const int& out_width);
199 ExprPtr LRotate(const ExprPtr& bv, const int& immediate);
201 ExprPtr RRotate(const ExprPtr& bv, const int& immediate);
202 
203 /******************************************************************************/
204 // Function usage
205 /******************************************************************************/
207 ExprPtr AppFunc(const FuncPtr& func);
209 ExprPtr AppFunc(const FuncPtr& func, const ExprPtr& arg0);
211 ExprPtr AppFunc(const FuncPtr& func, const ExprPtr& arg0, const ExprPtr& arg1);
213 ExprPtr AppFunc(const FuncPtr& func, const ExprPtrVec& args);
214 
215 /******************************************************************************/
216 // Others
217 /******************************************************************************/
219 ExprPtr Imply(const ExprPtr& p, const ExprPtr& q);
221 ExprPtr Ite(const ExprPtr& cnd, const ExprPtr& true_expr,
222  const ExprPtr& false_expr);
223 
224 /******************************************************************************/
225 // Non-AST construction utilities
226 /******************************************************************************/
228 bool TopEq(const ExprPtr& a, const ExprPtr& b);
229 
230 } // namespace asthub
231 
232 } // namespace ilang
233 
234 #endif // ILANG_ILA_AST_HUB_H__
ExprRef BvConst(const NumericType &bv_val, const int &bit_width)
Return a bit-vector constant.
ExprRef SRem(const ExprRef &a, const ExprRef &b)
Arithmetic signed remainder.
ExprRef LRotate(const ExprRef &bv, const int &immediate)
Left-rotate the bit-vector with immediate number of times.
Expr::ExprPtr ExprPtr
Pointer type for normal use of Expr.
Definition: expr.h:138
ExprRef Ule(const ExprRef &a, const ExprRef &b)
Unsigned less than or equal to (bit-vectors only).
AstUidSort
Unified ID for Sort.
Definition: sort.h:18
ExprRef URem(const ExprRef &a, const ExprRef &b)
Arithmetic unsigned remainder.
AstUidExprOp
Unified ID for ExprOp.
Definition: expr_op.h:14
ExprRef Lshr(const ExprRef &a, const ExprRef &b)
Logical right shift for bit-vectors.
ExprRef Uge(const ExprRef &a, const ExprRef &b)
Unsigned greater than or equal to (bit-vectors only).
ExprRef Store(const ExprRef &mem, const ExprRef &addr, const ExprRef &data)
Store to memory.
ExprRef ZExt(const ExprRef &bv, const int &length)
Zero-extend the bit-vector to the specified length.
ExprRef SMod(const ExprRef &a, const ExprRef &b)
Arithmetic signed modular.
ExprRef Ugt(const ExprRef &a, const ExprRef &b)
Unsigned greater than (bit-vectors only).
ExprRef Load(const ExprRef &mem, const ExprRef &addr)
Load from memory.
Func::FuncPtr FuncPtr
Pointer type for normal use of Func.
Definition: func.h:83
ExprRef Imply(const ExprRef &ante, const ExprRef &cons)
Logical imply for Booleans.
ExprRef Extract(const ExprRef &bv, const int &hi, const int &lo)
Extract bit-field in the bit-vector.
Expr::ExprPtrVec ExprPtrVec
Type for storing a set of Expr.
Definition: expr.h:140
ExprRef BoolConst(bool bool_val)
Return a Boolean constant.
ExprRef Ite(const ExprRef &cond, const ExprRef &t, const ExprRef &f)
If-then-else on the Boolean condition.
ExprRef MemConst(const NumericType &def_val, const std::map< NumericType, NumericType > &vals, const int &addr_width, const int &data_width)
Return a memory constant.
ExprRef Concat(const ExprRef &msbv, const ExprRef &lsbv)
Concatenate two bit-vectors.
ExprRef RRotate(const ExprRef &bv, const int &immediate)
Right-rotate the bit-vector with immediate number of times.
ExprRef SExt(const ExprRef &bv, const int &length)
Sign-extend the bit-vector to the specified length.
BvVal::BvValType BvValType
Data type for storing BvVal.
Definition: sort_value.h:103
ExprRef Ult(const ExprRef &a, const ExprRef &b)
Unsigned less than (bit-vectors only).