ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | Static Public Member Functions | Friends | List of all members
ilang::InstrLvlAbs Class Reference

The class of Instruction-Level Abstraction (ILA). An ILA contains: More...

#include <instr_lvl_abs.h>

Inheritance diagram for ilang::InstrLvlAbs:
ilang::Object

Public Types

typedef std::shared_ptr< InstrLvlAbsInstrLvlAbsPtr
 Pointer type for normal use of InstrLvlAbs.
 
typedef std::shared_ptr< const InstrLvlAbsInstrLvlAbsCnstPtr
 Pointer type for read-only usage of InstrLvlAbs.
 
typedef KeyVec< Symbol, ExprPtrVarMap
 Type for storing a set of ExprPtr (input/state variables).
 
typedef KeyVec< Symbol, InstrPtrInstrMap
 Type for storing a set of Instr.
 
typedef KeyVec< Symbol, InstrLvlAbsPtrInstrLvlAbsMap
 Type for storing a set of ILA (child-ILAs).
 
- Public Types inherited from ilang::Object
typedef std::shared_ptr< ObjectObjPtr
 Pointer type for normal use of Object.
 

Public Member Functions

 InstrLvlAbs (const std::string &name="", const InstrLvlAbsPtr parent=NULL)
 Consturctor.
 
 ~InstrLvlAbs ()
 Default destructor.
 
bool is_instr_lvl_abs () const
 Return true if is InstrLvlAbs.
 
bool is_spec () const
 Return true if is specification (not implementation).
 
const InstrLvlAbsPtr parent () const
 Return the parent ILA.
 
const ExprMngrPtr expr_mngr () const
 Return the ast simplifier.
 
void set_spec (bool spec)
 Set the ILA to be specification if true.
 
void set_expr_mngr (const ExprMngrPtr expr_mngr)
 Update the ast simplifier.
 
size_t input_num () const
 Return the number of input variables.
 
size_t state_num () const
 Return the number of state variables.
 
size_t instr_num () const
 Return the number of instructions.
 
size_t child_num () const
 Return the number of child-ILAs.
 
size_t init_num () const
 Return the number of initial condition.
 
const ExprPtr fetch () const
 Return the fetch function.
 
const ExprPtr valid () const
 Return the valid function.
 
const ExprPtr input (const size_t &i) const
 Access the i-th input variable.
 
const ExprPtr state (const size_t &i) const
 Access the i-th state variable.
 
const InstrPtr instr (const size_t &i) const
 Access the i-th instruction.
 
const InstrLvlAbsPtr child (const size_t &i) const
 Access the i-th child-ILA.
 
const ExprPtr init (const size_t &i) const
 Access the i-th initial condition.
 
const ExprPtr input (const std::string &name) const
 Return the named input variable; return NULL if not registered.
 
const ExprPtr state (const std::string &name) const
 Return the named state variable; return NULL if not registered.
 
const InstrPtr instr (const std::string &name) const
 Return the named instruction; return NULL if not registered.
 
const InstrLvlAbsPtr child (const std::string &name) const
 Return the named child-ILA; return NULL if not registered.
 
const ExprPtr find_input (const Symbol &name) const
 Return the named input variable; return NULL if not registered.
 
const ExprPtr find_state (const Symbol &name) const
 Return the named state variable; return NULL if not registered.
 
const InstrPtr find_instr (const Symbol &name) const
 Return the named instruction; return NULL if not registered.
 
const InstrLvlAbsPtr find_child (const Symbol &name) const
 Return the named child-ILA; return NULL if not registered.
 
void AddInput (const ExprPtr input_var)
 Add one input variable to the ILA, and register to the simplifier. More...
 
void AddState (const ExprPtr state_var)
 Add one state variable to the ILA, and register to the simplifier. More...
 
void AddInit (const ExprPtr cntr_expr)
 Add one free variable to the ILA. More...
 
void SetFetch (const ExprPtr fetch_expr)
 Set the fetch function, and simplify (if needed) by the simplifier. More...
 
void SetValid (const ExprPtr valid_expr)
 Set the valid function, and simplify (if needed) by the simplifier. More...
 
void AddInstr (const InstrPtr instr)
 Add one instruction to the ILA, and simplify (if needed). Note that only fully constructed instruction can be added. More...
 
void AddChild (const InstrLvlAbsPtr child)
 Add one ILA to the child list. No simplification between ILAs. More...
 
const ExprPtr NewBoolInput (const std::string &name)
 Create one Boolean variable and register as an input. More...
 
const ExprPtr NewBvInput (const std::string &name, const int &bit_width)
 Create one Bitvector variable and register as an input. More...
 
const ExprPtr NewMemInput (const std::string &name, const int &addr_width, const int &data_width)
 Create one Memory variable and register as an input. More...
 
const ExprPtr NewBoolState (const std::string &name)
 Create one Boolean variable and register as a state. More...
 
const ExprPtr NewBvState (const std::string &name, const int &bit_width)
 Create one Bitvector variable and register as a state. More...
 
const ExprPtr NewMemState (const std::string &name, const int &addr_width, const int &data_width)
 Create one Memory variable and register as a state. More...
 
const ExprPtr NewBoolFreeVar (const std::string &name)
 Create one free Boolean variable. More...
 
const ExprPtr NewBvFreeVar (const std::string &name, const int &bit_width)
 Create one free bit-vector variable. More...
 
const ExprPtr NewMemFreeVar (const std::string &name, const int &addr_width, const int &data_width)
 Create one free Memory variable. More...
 
const InstrPtr NewInstr (const std::string &name="")
 Create and register one instruction. More...
 
const InstrLvlAbsPtr NewChild (const std::string &name)
 Create and register one child-ILA. More...
 
bool Check () const
 Sanity check for the ILA (e.g. sort marching). More...
 
void MergeChild ()
 Merge child-ILAs, including variables, simplifier, etc.
 
void SortInstr ()
 Sort instructions based on the sequencing, if any.
 
void AddSeqTran (const InstrPtr src, const InstrPtr dst, const ExprPtr cnd)
 Define instruction sequencing by adding a transition edge. More...
 
std::string GetRootName () const
 Return the ancestor names in sequence.
 
std::ostream & Print (std::ostream &out) const
 Output stream function.
 
template<class F >
void DepthFirstVisit (F &func) const
 Templated visitor: visit each child-ILA in a depth-first order.
 
template<class F >
void DepthFirstVisitPrePost (F &func) const
 Templated visitor: visit each child-ILA in a depth-first order and apply the function object F pre/pose on it.
 
- Public Member Functions inherited from ilang::Object
 Object ()
 Default constructor.
 
 Object (const std::string &name)
 Constructor with string name.
 
virtual ~Object ()
 Default destructor.
 
const Symbolname () const
 Get the symbol (name).
 
virtual bool is_instr () const
 Is type Instr.
 
virtual bool is_ast () const
 Is type Ast.
 

Static Public Member Functions

static InstrLvlAbsPtr New (const std::string &name, const InstrLvlAbsPtr parent=NULL)
 Create a new ILA (InstrLvlAbs) with the name. Used for hiding implementation specific type details.
 

Friends

class Instr
 
std::ostream & operator<< (std::ostream &out, InstrLvlAbs &ila)
 Overload output stream for object.
 
std::ostream & operator<< (std::ostream &out, InstrLvlAbsPtr ila)
 Overload output stream for pointer.
 
std::ostream & operator<< (std::ostream &out, InstrLvlAbsCnstPtr ila)
 Overload output stream for pointer.
 

Detailed Description

The class of Instruction-Level Abstraction (ILA). An ILA contains:

Member Function Documentation

◆ AddChild()

void ilang::InstrLvlAbs::AddChild ( const InstrLvlAbsPtr  child)

Add one ILA to the child list. No simplification between ILAs.

Parameters
[in]childpointer to the child-ILA being added.

◆ AddInit()

void ilang::InstrLvlAbs::AddInit ( const ExprPtr  cntr_expr)

Add one free variable to the ILA.

Parameters
[in]free_varpointer to the free variable being added. Add one constraint to the initial condition, i.e. no contraint means arbitrary initial values to the state variables.
[in]cntr_exprpointer to the constraint being added.

◆ AddInput()

void ilang::InstrLvlAbs::AddInput ( const ExprPtr  input_var)

Add one input variable to the ILA, and register to the simplifier.

Parameters
[in]input_varpointer to the input variable being added.

◆ AddInstr()

void ilang::InstrLvlAbs::AddInstr ( const InstrPtr  instr)

Add one instruction to the ILA, and simplify (if needed). Note that only fully constructed instruction can be added.

Parameters
[in]instrpointer to the instruction being added.

◆ AddSeqTran()

void ilang::InstrLvlAbs::AddSeqTran ( const InstrPtr  src,
const InstrPtr  dst,
const ExprPtr  cnd 
)

Define instruction sequencing by adding a transition edge.

Parameters
[in]srcsource instruction
[in]dsttarget instruction (destination)
[in]cndtransition condition (guard), i.e. dst.DECODE

◆ AddState()

void ilang::InstrLvlAbs::AddState ( const ExprPtr  state_var)

Add one state variable to the ILA, and register to the simplifier.

Parameters
[in]state_varpointer to the state variable being added.

◆ Check()

bool ilang::InstrLvlAbs::Check ( ) const

Sanity check for the ILA (e.g. sort marching).

Returns
True if check pass.

◆ NewBoolFreeVar()

const ExprPtr ilang::InstrLvlAbs::NewBoolFreeVar ( const std::string &  name)

Create one free Boolean variable.

Parameters
[in]nameof the Boolean variable.
Returns
pointer to the variable.

◆ NewBoolInput()

const ExprPtr ilang::InstrLvlAbs::NewBoolInput ( const std::string &  name)

Create one Boolean variable and register as an input.

Parameters
[in]nameof the bool input.
Returns
pointer to the input.

◆ NewBoolState()

const ExprPtr ilang::InstrLvlAbs::NewBoolState ( const std::string &  name)

Create one Boolean variable and register as a state.

Parameters
[in]nameof the bool state.
Returns
pointer to the state variable.

◆ NewBvFreeVar()

const ExprPtr ilang::InstrLvlAbs::NewBvFreeVar ( const std::string &  name,
const int &  bit_width 
)

Create one free bit-vector variable.

Parameters
[in]nameof the bit-vector variable.
[in]bit_widthlength of the bit-vector variable.
Returns
pointer to the variable.

◆ NewBvInput()

const ExprPtr ilang::InstrLvlAbs::NewBvInput ( const std::string &  name,
const int &  bit_width 
)

Create one Bitvector variable and register as an input.

Parameters
[in]nameof the bitvector input.
[in]bit_widthlength of the bitvector variable.
Returns
pointer to the input.

◆ NewBvState()

const ExprPtr ilang::InstrLvlAbs::NewBvState ( const std::string &  name,
const int &  bit_width 
)

Create one Bitvector variable and register as a state.

Parameters
[in]nameof the bitvector state.
[in]bit_widthvalue bit-width.
Returns
pointer to the state variable.

◆ NewChild()

const InstrLvlAbsPtr ilang::InstrLvlAbs::NewChild ( const std::string &  name)

Create and register one child-ILA.

Parameters
[in]nameof the child.
Returns
pointer to the child-ILA.

◆ NewInstr()

const InstrPtr ilang::InstrLvlAbs::NewInstr ( const std::string &  name = "")

Create and register one instruction.

Parameters
[in]nameof the instruction.
Returns
pointer to the instruction.

◆ NewMemFreeVar()

const ExprPtr ilang::InstrLvlAbs::NewMemFreeVar ( const std::string &  name,
const int &  addr_width,
const int &  data_width 
)

Create one free Memory variable.

Parameters
[in]nameof the memory variable.
[in]addr_widthaddress bit-width.
[in]data_widthdata bit-width.
Returns
pointer to the variable.

◆ NewMemInput()

const ExprPtr ilang::InstrLvlAbs::NewMemInput ( const std::string &  name,
const int &  addr_width,
const int &  data_width 
)

Create one Memory variable and register as an input.

Parameters
[in]nameof the memory input
[in]addr_widthaddress bit-width.
[in]data_widthdata bit-width.
Returns
pointer to the memory state.

◆ NewMemState()

const ExprPtr ilang::InstrLvlAbs::NewMemState ( const std::string &  name,
const int &  addr_width,
const int &  data_width 
)

Create one Memory variable and register as a state.

Parameters
[in]nameof the memory state.
[in]addr_widthaddress bit-width.
[in]data_widthdata bit-width.
Returns
pointer to the memory state.

◆ SetFetch()

void ilang::InstrLvlAbs::SetFetch ( const ExprPtr  fetch_expr)

Set the fetch function, and simplify (if needed) by the simplifier.

Parameters
[in]fetch_exprpointer to the fetch function (as an expression).

◆ SetValid()

void ilang::InstrLvlAbs::SetValid ( const ExprPtr  valid_expr)

Set the valid function, and simplify (if needed) by the simplifier.

Parameters
[in]valid_exprpointer to the valid function (as an expression).

The documentation for this class was generated from the following file: