ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
ilang++.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_ILANG_CPP_H__
5 #define ILANG_ILANG_CPP_H__
6 
7 #include <cstdint>
8 #include <map>
9 #include <memory>
10 #include <string>
11 #include <vector>
12 
13 #include "z3++.h"
14 
17 namespace ilang {
18 
20 typedef uint64_t NumericType;
21 
22 /******************************************************************************/
23 // Logging system.
24 /******************************************************************************/
31 void LogLevel(const int& lvl);
35 void LogPath(const std::string& path);
38 void LogToErr(bool to_err);
40 void EnableDebug(const std::string& tag);
42 void DisableDebug(const std::string& tag);
43 
44 /******************************************************************************/
45 // ILA Construction.
46 /******************************************************************************/
47 // implementation-specific structure
48 class Sort;
49 class Func;
50 class Expr;
51 class Instr;
52 class InstrLvlAbs;
53 class Unroller;
54 // forward declaration
55 class Ila;
56 
58 class SortRef {
59 private:
60  typedef std::shared_ptr<Sort> SortPtr;
61  // ------------------------- MEMBERS -------------------------------------- //
63  SortPtr ptr_ = NULL;
64 
65 public:
66  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
68  SortRef(SortPtr ptr);
70  ~SortRef();
71 
72  // ------------------------- HELPERS -------------------------------------- //
74  static SortRef BOOL();
76  static SortRef BV(const int& bit_w);
78  static SortRef MEM(const int& addr_w, const int& data_w);
79 
80  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
82  inline SortPtr get() const { return ptr_; }
83 }; // class SortRef
84 
86 class ExprRef {
87 private:
88  typedef std::shared_ptr<Expr> ExprPtr;
89  // ------------------------- MEMBERS -------------------------------------- //
91  ExprPtr ptr_ = NULL;
92 
93 public:
94  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
96  ExprRef(ExprPtr ptr);
98  ~ExprRef();
99 
100  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
102  inline ExprPtr get() const { return ptr_; }
104  int bit_width() const;
106  int addr_width() const;
108  int data_width() const;
109 
110  // ------------------------- METHODS -------------------------------------- //
111  /****************************************************************************/
112  // Memory-related operations
113  /****************************************************************************/
115  ExprRef Load(const ExprRef& addr) const;
117  ExprRef Store(const ExprRef& addr, const ExprRef& data) const;
119  ExprRef Load(const NumericType& addr) const;
121  ExprRef Store(const NumericType& addr, const NumericType& data) const;
122 
123  /****************************************************************************/
124  // Bit manipulation for bit-vectors.
125  /****************************************************************************/
127  ExprRef Append(const ExprRef& lsbv) const;
129  ExprRef operator()(const int& hi, const int& lo) const;
131  ExprRef operator()(const int& idx) const;
133  ExprRef ZExt(const int& length) const;
135  ExprRef SExt(const int& length) const;
136 
137  /****************************************************************************/
138  // Others
139  /****************************************************************************/
141  void ReplaceArg(const int& i, const ExprRef& new_arg);
143  void ReplaceArg(const ExprRef& org_arg, const ExprRef& new_arg);
144 
146  bool SetEntryNum(const int& num);
148  int GetEntryNum();
149 
150 }; // class ExprRef
151 
152 /******************************************************************************/
153 // Unary operation
154 /******************************************************************************/
156 ExprRef operator-(const ExprRef& a);
158 ExprRef operator!(const ExprRef& a);
160 ExprRef operator~(const ExprRef& a);
161 
162 /******************************************************************************/
163 // Binary operation
164 /******************************************************************************/
166 ExprRef operator&(const ExprRef& a, const ExprRef& b);
168 ExprRef operator|(const ExprRef& a, const ExprRef& b);
170 ExprRef operator^(const ExprRef& a, const ExprRef& b);
172 ExprRef operator<<(const ExprRef& a, const ExprRef& b);
174 ExprRef operator>>(const ExprRef& a, const ExprRef& b);
176 ExprRef Lshr(const ExprRef& a, const ExprRef& b);
178 ExprRef operator+(const ExprRef& a, const ExprRef& b);
180 ExprRef operator-(const ExprRef& a, const ExprRef& b);
182 ExprRef operator*(const ExprRef& a, const ExprRef& b);
184 ExprRef operator/(const ExprRef& a, const ExprRef& b);
185 
187 ExprRef operator&(const ExprRef& a, const bool& b);
189 ExprRef operator|(const ExprRef& a, const bool& b);
191 ExprRef operator^(const ExprRef& a, const bool& b);
193 ExprRef operator<<(const ExprRef& a, const int& b);
195 ExprRef operator>>(const ExprRef& a, const int& b);
197 ExprRef Lshr(const ExprRef& a, const int& b);
199 ExprRef operator+(const ExprRef& a, const NumericType& b);
201 ExprRef operator-(const ExprRef& a, const NumericType& b);
203 ExprRef operator*(const ExprRef& a, const NumericType& b);
205 ExprRef SRem(const ExprRef& a, const ExprRef& b);
207 ExprRef URem(const ExprRef& a, const ExprRef& b);
209 ExprRef SMod(const ExprRef& a, const ExprRef& b);
210 
211 /******************************************************************************/
212 // Binary comparison
213 /******************************************************************************/
216 void SetUnsignedComparison(bool sign);
218 ExprRef operator==(const ExprRef& a, const ExprRef& b);
220 ExprRef operator!=(const ExprRef& a, const ExprRef& b);
222 ExprRef operator<(const ExprRef& a, const ExprRef& b);
224 ExprRef operator>(const ExprRef& a, const ExprRef& b);
226 ExprRef operator<=(const ExprRef& a, const ExprRef& b);
228 ExprRef operator>=(const ExprRef& a, const ExprRef& b);
230 ExprRef Ult(const ExprRef& a, const ExprRef& b);
232 ExprRef Ugt(const ExprRef& a, const ExprRef& b);
234 ExprRef Ule(const ExprRef& a, const ExprRef& b);
236 ExprRef Uge(const ExprRef& a, const ExprRef& b);
238 ExprRef Slt(const ExprRef& a, const ExprRef& b);
240 ExprRef Sgt(const ExprRef& a, const ExprRef& b);
242 ExprRef Sle(const ExprRef& a, const ExprRef& b);
244 ExprRef Sge(const ExprRef& a, const ExprRef& b);
245 
246 // helper functions with constants
247 #if 0
248 ExprRef operator==(const ExprRef& a, const bool& b);
250 #endif
251 ExprRef operator==(const ExprRef& a, const NumericType& b);
254 ExprRef operator!=(const ExprRef& a, const NumericType& b);
256 ExprRef operator<(const ExprRef& a, const NumericType& b);
258 ExprRef operator>(const ExprRef& a, const NumericType& b);
260 ExprRef operator<=(const ExprRef& a, const NumericType& b);
262 ExprRef operator>=(const ExprRef& a, const NumericType& b);
264 ExprRef Ult(const ExprRef& a, const NumericType& b);
266 ExprRef Ugt(const ExprRef& a, const NumericType& b);
268 ExprRef Ule(const ExprRef& a, const NumericType& b);
270 ExprRef Uge(const ExprRef& a, const NumericType& b);
272 ExprRef Slt(const ExprRef& a, const NumericType& b);
274 ExprRef Sgt(const ExprRef& a, const NumericType& b);
276 ExprRef Sle(const ExprRef& a, const NumericType& b);
278 ExprRef Sge(const ExprRef& a, const NumericType& b);
279 
280 /******************************************************************************/
281 // Memory-related operations
282 /******************************************************************************/
284 ExprRef Load(const ExprRef& mem, const ExprRef& addr);
286 ExprRef Store(const ExprRef& mem, const ExprRef& addr, const ExprRef& data);
288 ExprRef Load(const ExprRef& mem, const NumericType& addr);
290 ExprRef Store(const ExprRef& mem, const NumericType& addr,
291  const NumericType& data);
292 
293 /******************************************************************************/
294 // Bit manipulation for bit-vectors.
295 /******************************************************************************/
299 ExprRef Concat(const ExprRef& msbv, const ExprRef& lsbv);
304 ExprRef Extract(const ExprRef& bv, const int& hi, const int& lo);
308 ExprRef SelectBit(const ExprRef& bv, const int& idx);
312 ExprRef ZExt(const ExprRef& bv, const int& length);
316 ExprRef SExt(const ExprRef& bv, const int& length);
320 ExprRef LRotate(const ExprRef& bv, const int& immediate);
324 ExprRef RRotate(const ExprRef& bv, const int& immediate);
325 
326 /******************************************************************************/
327 // Others
328 /******************************************************************************/
332 ExprRef Imply(const ExprRef& ante, const ExprRef& cons);
333 
338 ExprRef Ite(const ExprRef& cond, const ExprRef& t, const ExprRef& f);
339 
340 /******************************************************************************/
341 // Constant
342 /******************************************************************************/
345 ExprRef BoolConst(bool bool_val);
346 
350 ExprRef BvConst(const NumericType& bv_val, const int& bit_width);
351 
357 ExprRef MemConst(const NumericType& def_val,
358  const std::map<NumericType, NumericType>& vals,
359  const int& addr_width, const int& data_width);
360 
361 /******************************************************************************/
362 // Non-AST-construction
363 /******************************************************************************/
365 bool TopEqual(const ExprRef& a, const ExprRef& b);
366 
368 class FuncRef {
369 private:
370  typedef std::shared_ptr<Func> FuncPtr;
371  // ------------------------- MEMBERS -------------------------------------- //
373  FuncPtr ptr_ = NULL;
374 
375 public:
376  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
378  FuncRef(const std::string& name, const SortRef& range);
380  FuncRef(const std::string& name, const SortRef& range, const SortRef& d0);
382  FuncRef(const std::string& name, const SortRef& range, const SortRef& d0,
383  const SortRef& d1);
385  FuncRef(const std::string& name, const SortRef& range,
386  const std::vector<SortRef>& dvec);
388  ~FuncRef();
389 
390  // ------------------------- METHODS -------------------------------------- //
392  ExprRef operator()() const;
394  ExprRef operator()(const ExprRef& arg0) const;
396  ExprRef operator()(const ExprRef& arg0, const ExprRef& arg1) const;
398  ExprRef operator()(const std::vector<ExprRef>& argvec) const;
399 
400 private:
401  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
403  inline FuncPtr get() const { return ptr_; }
404 
405 }; // class FuncRef
406 
408 class InstrRef {
409 private:
410  typedef std::shared_ptr<Instr> InstrPtr;
411  // ------------------------- MEMBERS -------------------------------------- //
413  InstrPtr ptr_ = NULL;
414 
415 public:
416  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
418  InstrRef(InstrPtr ptr);
420  ~InstrRef();
421 
422  // ------------------------- METHODS -------------------------------------- //
425  void SetDecode(const ExprRef& decode);
426 
430  void SetUpdate(const ExprRef& state, const ExprRef& update);
431 
434  void SetProgram(const Ila& prog);
435 
438  ExprRef GetDecode() const;
439 
443  ExprRef GetUpdate(const ExprRef& state) const;
444 
445  // ------------------------- GENERATORS --------------------------------- //
448  void ExportToVerilog(std::ostream& fout) const;
449 
452  void ExportToVerilogWithChild(std::ostream& fout) const;
453 
454  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
456  inline InstrPtr get() const { return ptr_; }
457 
458 }; // class InstrRef
459 
461 class Ila {
462 private:
463  typedef std::shared_ptr<InstrLvlAbs> IlaPtr;
464  // ------------------------- MEMBERS -------------------------------------- //
466  IlaPtr ptr_ = NULL;
467 
468 public:
469  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
471  Ila(const std::string& name);
473  Ila(IlaPtr ptr);
475  ~Ila();
476 
477  // ------------------------- METHODS -------------------------------------- //
480  ExprRef NewBoolState(const std::string& name);
484  ExprRef NewBvState(const std::string& name, const int& bit_width);
489  ExprRef NewMemState(const std::string& name, const int& addr_width,
490  const int& data_width);
491 
494  ExprRef NewBoolInput(const std::string& name);
498  ExprRef NewBvInput(const std::string& name, const int& bit_width);
499 
502  void AddInit(const ExprRef& init);
503 
506  void SetFetch(const ExprRef& fetch);
507 
510  void SetValid(const ExprRef& valid);
511 
514  InstrRef NewInstr(const std::string& name);
515 
518  Ila NewChild(const std::string& name);
519 
520  // ------------------------- GENERATORS --------------------------------- //
523  void ExportToVerilog(std::ostream& fout) const;
524 
525  // ------------------------- ACCESSORS/MUTATORS --------------------------- //
527  size_t input_num() const;
529  size_t state_num() const;
531  size_t instr_num() const;
533  size_t child_num() const;
535  size_t init_num() const;
536 
538  std::string name() const;
540  ExprRef fetch() const;
542  ExprRef valid() const;
543 
545  ExprRef input(const size_t& i) const;
547  ExprRef state(const size_t& i) const;
549  InstrRef instr(const size_t& i) const;
551  Ila child(const size_t& i) const;
553  ExprRef init(const size_t& i) const;
554 
556  ExprRef input(const std::string& name) const;
558  ExprRef state(const std::string& name) const;
560  InstrRef instr(const std::string& name) const;
562  Ila child(const std::string& name) const;
563 
565  inline IlaPtr get() const { return ptr_; }
566 
567 }; // class Ila
568 
569 /******************************************************************************/
570 // Output stream helper
571 /******************************************************************************/
573 std::ostream& operator<<(std::ostream& out, const ExprRef& expr);
575 std::ostream& operator<<(std::ostream& out, const InstrRef& instr);
577 std::ostream& operator<<(std::ostream& out, const Ila& ila);
578 
579 /******************************************************************************/
580 // Converters
581 /******************************************************************************/
585 bool ExportIlaPortable(const Ila& ila, const std::string& file_name);
586 
589 Ila ImportIlaPortable(const std::string& file_name);
590 
594 Ila ImportSynthAbstraction(const std::string& file_name,
595  const std::string& ila_name);
596 
602 void ImportChildSynthAbstraction(const std::string& file_name, Ila& parent,
603  const std::string& ila_name);
604 
605 /******************************************************************************/
606 // Verification.
607 /******************************************************************************/
610 public:
611  // ------------------------- CONSTRUCTOR/DESTRUCTOR ----------------------- //
613  IlaZ3Unroller(z3::context& ctx, const std::string& suff = "");
615  ~IlaZ3Unroller();
616 
617  // ------------------------- METHODS -------------------------------------- //
619  inline void AddGlobPred(const ExprRef& p) { glob_pred_.push_back(p); }
621  inline void AddInitPred(const ExprRef& p) { init_pred_.push_back(p); }
623  inline void AddStepPred(const int& k, const ExprRef& p) {
624  step_pred_.push_back({k, p});
625  }
627  inline void ClearGlobPred() { glob_pred_.clear(); }
629  inline void ClearInitPred() { init_pred_.clear(); }
631  inline void ClearStepPred() { step_pred_.clear(); }
632 
637  z3::expr UnrollMonoConn(const Ila& top, const int& k, const int& init = 0);
638 
643  z3::expr UnrollMonoFree(const Ila& top, const int& k, const int& init = 0);
644 
648  z3::expr UnrollPathConn(const std::vector<InstrRef>& path,
649  const int& init = 0);
650 
654  z3::expr UnrollPathFree(const std::vector<InstrRef>& path,
655  const int& init = 0);
656 
657  // ------------------------- HELPERS -------------------------------------- //
659  z3::expr CurrState(const ExprRef& v, const int& t);
661  z3::expr NextState(const ExprRef& v, const int& t);
663  z3::expr GetZ3Expr(const ExprRef& v, const int& t = 0);
665  z3::expr Equal(const ExprRef& va, const int& ta, const ExprRef& vb,
666  const int& tb);
667 
668 private:
669  // ------------------------- MEMBERS -------------------------------------- //
671  z3::context& ctx_;
672 
674  std::vector<ExprRef> glob_pred_;
676  std::vector<ExprRef> init_pred_;
678  std::vector<std::pair<int, ExprRef>> step_pred_;
680  std::string extra_suff_;
681 
683  std::shared_ptr<Unroller> univ_ = NULL;
684 
685  // ------------------------- HELPERS -------------------------------------- //
687  template <class T> void InitializeUnroller(T unroller) {
688  for (auto it = glob_pred_.begin(); it != glob_pred_.end(); it++) {
689  unroller->AddGlobPred(it->get());
690  }
691  for (auto it = init_pred_.begin(); it != init_pred_.end(); it++) {
692  unroller->AddInitPred(it->get());
693  }
694  for (auto it = step_pred_.begin(); it != step_pred_.end(); it++) {
695  unroller->AddStepPred(it->second.get(), it->first);
696  }
697  // unroller->SetExtraSuffix(extra_suff_);
698  }
699 
700 }; // class IlaZ3Unroller
701 
702 } // namespace ilang
703 
704 #endif // ILANG_ILANG_CPP_H__
ilang::Store
ExprRef Store(const ExprRef &mem, const ExprRef &addr, const ExprRef &data)
Store to memory.
ilang::ExprRef::SExt
ExprRef SExt(const int &length) const
Sign-extend the bit-vector to the specified length.
ilang::ImportSynthAbstraction
Ila ImportSynthAbstraction(const std::string &file_name, const std::string &ila_name)
Import the synthesized abstraction from file.
ilang::Ila::init_num
size_t init_num() const
Return the number of initial condition.
ilang::ExprRef::data_width
int data_width() const
Return the data bit-width if is memory; return -1 otherwise.
ilang::operator/
ExprRef operator/(const ExprRef &a, const ExprRef &b)
Unsigned division for bit-vectors.
ilang::ExprRef::ExprRef
ExprRef(ExprPtr ptr)
Constructor with the pointer of the actual data.
ilang::FuncRef::~FuncRef
~FuncRef()
Default destructor.
ilang::operator!
ExprRef operator!(const ExprRef &a)
Logical not for Booleans.
ilang::Ila::child_num
size_t child_num() const
Return the number of child-ILAs.
ilang::SExt
ExprRef SExt(const ExprRef &bv, const int &length)
Sign-extend the bit-vector to the specified length.
ilang::Ila::valid
ExprRef valid() const
Return the valid function.
ilang::Ila::NewChild
Ila NewChild(const std::string &name)
Declare a child-ILA.
ilang::Ila::state
ExprRef state(const size_t &i) const
Access the i-th state variable.
ilang::ExprRef::GetEntryNum
int GetEntryNum()
GEt the entry number of the memory (size regardless of bit-width).
ilang::Ite
ExprRef Ite(const ExprRef &cond, const ExprRef &t, const ExprRef &f)
If-then-else on the Boolean condition.
ilang::Instr
The class for the Instruction. An Instr object contains:
Definition: instr.h:24
ilang::Ila
The wrapper of InstrLvlAbs (ILA).
Definition: ilang++.h:461
ilang::Load
ExprRef Load(const ExprRef &mem, const ExprRef &addr)
Load from memory.
ilang::SortRef::BV
static SortRef BV(const int &bit_w)
Return a bit-vector Sort of the given bit-width.
ilang::InstrRef::ExportToVerilog
void ExportToVerilog(std::ostream &fout) const
Export instruction without child-program as Verilog.
ilang::Ila::NewBvInput
ExprRef NewBvInput(const std::string &name, const int &bit_width)
Declare an input of bit-vector type.
ilang::Ila::fetch
ExprRef fetch() const
Return the fetch function.
ilang::InstrRef::get
InstrPtr get() const
Return the wrapped ILA pointer.
Definition: ilang++.h:456
ilang::TopEqual
bool TopEqual(const ExprRef &a, const ExprRef &b)
Topologically equivalent.
ilang::InstrRef
The wrapper of Instr (instruction).
Definition: ilang++.h:408
ilang::IlaZ3Unroller::NextState
z3::expr NextState(const ExprRef &v, const int &t)
Return the z3::expr representing the next state at the time.
ilang::SortRef::MEM
static SortRef MEM(const int &addr_w, const int &data_w)
Return a memory (array) Sort of the given address/data bit-width.
ilang::Ila::NewBoolInput
ExprRef NewBoolInput(const std::string &name)
Declare an input of Boolean type.
ilang::ExprRef::~ExprRef
~ExprRef()
Default destructor.
ilang::MemConst
ExprRef MemConst(const NumericType &def_val, const std::map< NumericType, NumericType > &vals, const int &addr_width, const int &data_width)
Return a memory constant.
ilang::SelectBit
ExprRef SelectBit(const ExprRef &bv, const int &idx)
Extract single bit in the bit-vector.
ilang::Uge
ExprRef Uge(const ExprRef &a, const ExprRef &b)
Unsigned greater than or equal to (bit-vectors only).
ilang::Func
The class for uninterpreted function.
Definition: func.h:19
ilang::RRotate
ExprRef RRotate(const ExprRef &bv, const int &immediate)
Right-rotate the bit-vector with immediate number of times.
ilang::Ila::NewInstr
InstrRef NewInstr(const std::string &name)
Declare an instruction.
ilang::Ila::SetFetch
void SetFetch(const ExprRef &fetch)
Set the fetch function of the ILA.
ilang::ExprRef::Load
ExprRef Load(const ExprRef &addr) const
Load from memory.
ilang::InstrRef::SetDecode
void SetDecode(const ExprRef &decode)
Set the decode function of the instruction.
ilang::Ila::NewBvState
ExprRef NewBvState(const std::string &name, const int &bit_width)
Declare a state variable of bit-vector type.
ilang::IlaZ3Unroller
The wrapper of generating z3::expr for verification.
Definition: ilang++.h:609
ilang::InstrRef::~InstrRef
~InstrRef()
Default destructor.
ilang::Ila::name
std::string name() const
Return the Ila name.
ilang::FuncRef::operator()
ExprRef operator()() const
Apply the function with no argument.
ilang::InstrLvlAbs
The class of Instruction-Level Abstraction (ILA). An ILA contains:
Definition: instr_lvl_abs.h:35
ilang::BvConst
ExprRef BvConst(const NumericType &bv_val, const int &bit_width)
Return a bit-vector constant.
ilang::operator>>
ExprRef operator>>(const ExprRef &a, const ExprRef &b)
Arithmetic right shift for bit-vectors.
ilang::SortRef::~SortRef
~SortRef()
Default destructor.
ilang::SMod
ExprRef SMod(const ExprRef &a, const ExprRef &b)
Arithmetic signed modular.
ilang::FuncRef
The wrapper of Func (uninterpreted function).
Definition: ilang++.h:368
ilang::ExprRef::operator()
ExprRef operator()(const int &hi, const int &lo) const
Extract bit-field in the bit-vector.
ilang::EnableDebug
void EnableDebug(const std::string &tag)
Add a debug tag.
ilang::SRem
ExprRef SRem(const ExprRef &a, const ExprRef &b)
Arithmetic signed remainder.
ilang::IlaZ3Unroller::AddStepPred
void AddStepPred(const int &k, const ExprRef &p)
Add a predicate that should be asserted at the k-th step.
Definition: ilang++.h:623
ilang::ExprRef::ZExt
ExprRef ZExt(const int &length) const
Zero-extend the bit-vector to the specified length.
ilang::Ila::init
ExprRef init(const size_t &i) const
Access the i-th initial condition.
ilang::Sgt
ExprRef Sgt(const ExprRef &a, const ExprRef &b)
Signed greater than (bit-vectors only).
ilang::Ult
ExprRef Ult(const ExprRef &a, const ExprRef &b)
Unsigned less than (bit-vectors only).
ilang::operator~
ExprRef operator~(const ExprRef &a)
Bit-wise complement for bit-vectors.
ilang::LRotate
ExprRef LRotate(const ExprRef &bv, const int &immediate)
Left-rotate the bit-vector with immediate number of times.
ilang::LogToErr
void LogToErr(bool to_err)
Pipe log to stderr. Log messages to stderr instead of logfiles, if set to 1.
ilang::IlaZ3Unroller::CurrState
z3::expr CurrState(const ExprRef &v, const int &t)
Return the z3::expr representing the current state at the time.
ilang::ExprRef::Store
ExprRef Store(const ExprRef &addr, const ExprRef &data) const
Store to memory.
ilang::Sort
The class for sort (type for expr, and the range/domain of functions).
Definition: sort.h:18
ilang::ExprRef
The wrapper of Expr (e.g. state var, var relation, constant, etc).
Definition: ilang++.h:86
ilang::InstrRef::GetDecode
ExprRef GetDecode() const
Get the decode function of the instruction.
ilang::NumericType
uint64_t NumericType
Data type for numerics. NOTE: SHOULD BE SYNCED WITH BvValType!!
Definition: ilang++.h:20
ilang::Ila::child
Ila child(const size_t &i) const
Access the i-th child-ILA.
ilang::InstrRef::GetUpdate
ExprRef GetUpdate(const ExprRef &state) const
Set the update function of the given state variable.
ilang::IlaZ3Unroller::Equal
z3::expr Equal(const ExprRef &va, const int &ta, const ExprRef &vb, const int &tb)
Return the z3::expr representing a and b are equal at their time.
ilang::IlaZ3Unroller::AddInitPred
void AddInitPred(const ExprRef &p)
Add a predicate that should be asserted in the initial condition.
Definition: ilang++.h:621
ilang::Unroller
Base class for unrolling ILA execution in different settings.
Definition: unroller.h:18
ilang::Expr
The class for expression, which is the basic type for variables, constraints, state update expression...
Definition: expr.h:25
ilang::SortRef::BOOL
static SortRef BOOL()
Return a Boolean Sort.
ilang::SetUnsignedComparison
void SetUnsignedComparison(bool sign)
ilang::BoolConst
ExprRef BoolConst(bool bool_val)
Return a Boolean constant.
ilang::Sle
ExprRef Sle(const ExprRef &a, const ExprRef &b)
Signed less than or equal to (bit-vectors only).
ilang::operator<=
ExprRef operator<=(const ExprRef &a, const ExprRef &b)
Signed/Unsigned less than or equal to (bit-vectors only).
ilang::DisableDebug
void DisableDebug(const std::string &tag)
Remove a debug tag.
ilang::SortRef::SortRef
SortRef(SortPtr ptr)
Constructor with the pointer of the actual data.
ilang::IlaZ3Unroller::ClearInitPred
void ClearInitPred()
Clear the initial predicates.
Definition: ilang++.h:629
ilang::operator>
ExprRef operator>(const ExprRef &a, const ExprRef &b)
Signed/Unsigned greater than (bit-vectors only).
ilang::ExprRef::bit_width
int bit_width() const
Return the bit-width if is bit-vector; return -1 otherwise.
ilang::InstrRef::InstrRef
InstrRef(InstrPtr ptr)
Constructor with the pointer of the actual data.
ilang::ExprRef::get
ExprPtr get() const
Return the wrapped Expr pointer.
Definition: ilang++.h:102
ilang
ilang::Ila::instr_num
size_t instr_num() const
Return the number of instructions.
ilang::IlaZ3Unroller::GetZ3Expr
z3::expr GetZ3Expr(const ExprRef &v, const int &t=0)
Return the z3::expr representing the current-based Expr at the time.
ilang::InstrRef::SetUpdate
void SetUpdate(const ExprRef &state, const ExprRef &update)
Set the update function of the given state variable.
ilang::SortRef::get
SortPtr get() const
Return the wrapped Sort pointer.
Definition: ilang++.h:82
ilang::Ila::get
IlaPtr get() const
Return the wrapped ILA pointer.
Definition: ilang++.h:565
ilang::Ila::ExportToVerilog
void ExportToVerilog(std::ostream &fout) const
Export an ILA as Verilog.
ilang::Slt
ExprRef Slt(const ExprRef &a, const ExprRef &b)
Signed less than (bit-vectors only).
ilang::ZExt
ExprRef ZExt(const ExprRef &bv, const int &length)
Zero-extend the bit-vector to the specified length.
ilang::ExprRef::Append
ExprRef Append(const ExprRef &lsbv) const
Append another bit-vector to the less significant side.
ilang::operator==
ExprRef operator==(const ExprRef &a, const ExprRef &b)
Equal.
ilang::ExprRef::addr_width
int addr_width() const
Return the address bit-width if is memory; return -1 otherwise.
ilang::Ila::state_num
size_t state_num() const
Return the number of state variables.
ilang::ImportChildSynthAbstraction
void ImportChildSynthAbstraction(const std::string &file_name, Ila &parent, const std::string &ila_name)
Import the synthesized (child-)abstraction from file, under the given parent ILA.
ilang::Ugt
ExprRef Ugt(const ExprRef &a, const ExprRef &b)
Unsigned greater than (bit-vectors only).
ilang::InstrRef::SetProgram
void SetProgram(const Ila &prog)
Set the child-program of the instruction.
ilang::IlaZ3Unroller::ClearStepPred
void ClearStepPred()
Clear the step-specific predicates.
Definition: ilang++.h:631
ilang::IlaZ3Unroller::UnrollMonoConn
z3::expr UnrollMonoConn(const Ila &top, const int &k, const int &init=0)
Unroll the ILA monolithically with each step connected.
ilang::IlaZ3Unroller::UnrollPathFree
z3::expr UnrollPathFree(const std::vector< InstrRef > &path, const int &init=0)
Unroll a path with each step freely defined.
ilang::operator^
ExprRef operator^(const ExprRef &a, const ExprRef &b)
Logical XOR (bit-wise for bit-vectors).
ilang::ImportIlaPortable
Ila ImportIlaPortable(const std::string &file_name)
Import the ILA portable from file.
ilang::IlaZ3Unroller::AddGlobPred
void AddGlobPred(const ExprRef &p)
Add a predicate that should be asserted globally when unrolled.
Definition: ilang++.h:619
ilang::Ila::input_num
size_t input_num() const
Return the number of input variables.
ilang::FuncRef::FuncRef
FuncRef(const std::string &name, const SortRef &range)
Constructor with zero input argument (domain).
ilang::IlaZ3Unroller::UnrollMonoFree
z3::expr UnrollMonoFree(const Ila &top, const int &k, const int &init=0)
Unroll the ILA monolithically with each step freely defined.
ilang::Ule
ExprRef Ule(const ExprRef &a, const ExprRef &b)
Unsigned less than or equal to (bit-vectors only).
ilang::Concat
ExprRef Concat(const ExprRef &msbv, const ExprRef &lsbv)
Concatenate two bit-vectors.
ilang::operator<
ExprRef operator<(const ExprRef &a, const ExprRef &b)
Signed/Unsigned less than (bit-vectors only).
ilang::SortRef
The wrapper of Sort (type for different AST nodes).
Definition: ilang++.h:58
ilang::operator>=
ExprRef operator>=(const ExprRef &a, const ExprRef &b)
Signed/Unsigned greater than or equal to (bit-vectors only).
ilang::operator|
ExprRef operator|(const ExprRef &a, const ExprRef &b)
Logical OR (bit-wise for bit-vectors).
ilang::Imply
ExprRef Imply(const ExprRef &ante, const ExprRef &cons)
Logical imply for Booleans.
ilang::operator*
ExprRef operator*(const ExprRef &a, const ExprRef &b)
Unsigned multiply for bit-vectors.
ilang::Ila::NewMemState
ExprRef NewMemState(const std::string &name, const int &addr_width, const int &data_width)
Declare a state variable of memory (array) type.
ilang::operator+
ExprRef operator+(const ExprRef &a, const ExprRef &b)
Unsigned addition for bit-vectors.
ilang::Ila::~Ila
~Ila()
Default destructor.
ilang::ExprRef::ReplaceArg
void ReplaceArg(const int &i, const ExprRef &new_arg)
Replace the i-th argument with the new node.
ilang::operator<<
ExprRef operator<<(const ExprRef &a, const ExprRef &b)
Left shift for bit-vectors.
ilang::IlaZ3Unroller::~IlaZ3Unroller
~IlaZ3Unroller()
Default virtual destructor.
ilang::ExportIlaPortable
bool ExportIlaPortable(const Ila &ila, const std::string &file_name)
Export the ILA portable to file.
ilang::Extract
ExprRef Extract(const ExprRef &bv, const int &hi, const int &lo)
Extract bit-field in the bit-vector.
ilang::URem
ExprRef URem(const ExprRef &a, const ExprRef &b)
Arithmetic unsigned remainder.
ilang::Ila::NewBoolState
ExprRef NewBoolState(const std::string &name)
Declare a state variable of Boolean type.
ilang::operator&
ExprRef operator&(const ExprRef &a, const ExprRef &b)
Logical AND (bit-wise for bit-vectors).
ilang::Ila::SetValid
void SetValid(const ExprRef &valid)
Set the valid function of the ILA.
ilang::InstrRef::ExportToVerilogWithChild
void ExportToVerilogWithChild(std::ostream &fout) const
Export instruction with the child-program as Verilog.
ilang::Ila::input
ExprRef input(const size_t &i) const
Access the i-th input variable.
ilang::Ila::Ila
Ila(const std::string &name)
Constructor with the specified name.
ilang::Ila::instr
InstrRef instr(const size_t &i) const
Access the i-th instruction.
ilang::Ila::AddInit
void AddInit(const ExprRef &init)
Add one initial constraint.
ilang::LogLevel
void LogLevel(const int &lvl)
Set the minimun log level. Log messages at or above this level will be logged. (Default: 0)
ilang::operator-
ExprRef operator-(const ExprRef &a)
Arithmetic negate for bit-vectors.
ilang::Lshr
ExprRef Lshr(const ExprRef &a, const ExprRef &b)
Logical right shift for bit-vectors.
ilang::IlaZ3Unroller::IlaZ3Unroller
IlaZ3Unroller(z3::context &ctx, const std::string &suff="")
Default constructor.
ilang::operator!=
ExprRef operator!=(const ExprRef &a, const ExprRef &b)
Not equal.
ilang::LogPath
void LogPath(const std::string &path)
Set the path for log file. If specified, logfiles are written into this directory instead of the defa...
ilang::IlaZ3Unroller::ClearGlobPred
void ClearGlobPred()
Clear the global predicates.
Definition: ilang++.h:627
ilang::ExprRef::SetEntryNum
bool SetEntryNum(const int &num)
Set the entry number of the memory (size regardless of bit-width).
ilang::IlaZ3Unroller::UnrollPathConn
z3::expr UnrollPathConn(const std::vector< InstrRef > &path, const int &init=0)
Unroll a path with each step connected.
ilang::Sge
ExprRef Sge(const ExprRef &a, const ExprRef &b)
Signed greater than or equal to (bit-vectors only).