-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
122 changed files
with
7,627 additions
and
11,365 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Submodule vexpparser
added at
dd94bf
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
/// \file rfexpr_shortcut.h Refinement map expression | ||
/// construction | ||
/// Hongce Zhang (zhanghongce@126.com) | ||
|
||
#ifndef ILANG_RFEXPR_SHORTCUT_H__ | ||
#define ILANG_RFEXPR_SHORTCUT_H__ | ||
|
||
#include <ilang/rfmap-in/rfmap_typecheck.h> | ||
|
||
namespace ilang { | ||
|
||
rfmap::RfExpr rfmap_reduce_or(const rfmap::RfExpr& in); | ||
rfmap::RfExpr rfmap_imply(const rfmap::RfExpr& l, const rfmap::RfExpr& r); | ||
rfmap::RfExpr rfmap_and(const rfmap::RfExpr& l, const rfmap::RfExpr& r); | ||
rfmap::RfExpr rfmap_or(const rfmap::RfExpr& l, const rfmap::RfExpr& r); | ||
rfmap::RfExpr rfmap_and(const std::vector<rfmap::RfExpr>& v); | ||
rfmap::RfExpr rfmap_or(const std::vector<rfmap::RfExpr>& v); | ||
|
||
rfmap::RfExpr rfmap_ite(const rfmap::RfExpr& c, const rfmap::RfExpr& l, | ||
const rfmap::RfExpr& r); | ||
|
||
rfmap::RfExpr rfmap_eq(const rfmap::RfExpr& l, const rfmap::RfExpr& r); | ||
rfmap::RfExpr rfmap_le(const rfmap::RfExpr& l, const rfmap::RfExpr& r); | ||
|
||
rfmap::RfExpr rfmap_not(const rfmap::RfExpr& l); | ||
|
||
rfmap::RfExpr rfmap_true(); | ||
rfmap::RfExpr rfmap_false(); | ||
rfmap::RfExpr rfmap_const(unsigned b, unsigned w, unsigned v); | ||
/// if it is RTL. or ILA. then will use MakeVar | ||
/// otherwise will use MakeSpecial | ||
/// will not determine its type | ||
/// ReplExpr will determine the type | ||
rfmap::RfExpr rfmap_var(const std::string& v); | ||
|
||
} // namespace ilang | ||
|
||
#endif // ILANG_RFEXPR_SHORTCUT_H__ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,58 @@ | ||
/// \file rfexpr_to_smt.cc Refinement map to smt-lib2 | ||
/// Hongce Zhang (hongcez@princeton.edu) | ||
|
||
#ifndef ILANG_RFEXPR_TO_SMT_H__ | ||
#define ILANG_RFEXPR_TO_SMT_H__ | ||
|
||
#include <ilang/rfmap-in/rfmap_typecheck.h> | ||
|
||
namespace ilang { | ||
namespace rfmap { | ||
|
||
struct SmtType : public RfMapVarType { | ||
bool bool_or_bv; | ||
|
||
SmtType() : RfMapVarType(1), bool_or_bv(true) {} | ||
SmtType(unsigned w) : RfMapVarType(w), bool_or_bv(false) {} | ||
SmtType(unsigned a, unsigned d) : RfMapVarType(a, d), bool_or_bv(false) {} | ||
SmtType(const RfMapVarType& r, bool request_bool) | ||
: RfMapVarType(r), bool_or_bv(request_bool) {} | ||
|
||
bool is_bool() const { return bool_or_bv && (RfMapVarType::is_bv()); } | ||
bool is_bv() const { return (!bool_or_bv) && (RfMapVarType::is_bv()); } | ||
bool operator==(const SmtType& r) const { | ||
if (bool_or_bv != r.bool_or_bv) | ||
return false; | ||
if (type != r.type) | ||
return false; | ||
if (type == TYPE::BV) | ||
return width == r.width; | ||
if (type == TYPE::MEM) | ||
return data_width == r.data_width && addr_width == r.addr_width; | ||
return false; // unknown type , unknown | ||
} // operator= | ||
|
||
std::string type_to_smt2() const; | ||
|
||
}; // SmtType | ||
|
||
struct RfExpr2Smt { | ||
|
||
public: | ||
static std::string to_smt2(const RfExpr& in, SmtType expected_type); | ||
|
||
protected: | ||
// helper function | ||
static std::string | ||
to_smt2_const(const std::shared_ptr<verilog_expr::VExprAstConstant>& in, | ||
SmtType expected_type); | ||
static std::string | ||
to_smt2_var(const std::shared_ptr<verilog_expr::VExprAstVar>& in, | ||
SmtType expected_type); | ||
|
||
}; // struct RfExpr2Smt | ||
|
||
} // namespace rfmap | ||
} // namespace ilang | ||
|
||
#endif // ILANG_RFEXPR_TO_SMT_H__ |
Oops, something went wrong.