ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Classes | Public Types | Public Member Functions | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
ilang::VlgSglTgtGen Class Referenceabstract

Generating a target (just the invairant or for an instruction) More...

#include <vtarget_gen_impl.h>

Inheritance diagram for ilang::VlgSglTgtGen:
ilang::VlgSglTgtGen_Cosa ilang::VlgSglTgtGen_Jasper

Classes

struct  ex_info_t
 Type of record of extra info of a signal. More...
 

Public Types

enum  target_type_t { INVARIANTS, INSTRUCTIONS }
 Type of the target.
 
enum  ready_type_t { NA = 0, READY_SIGNAL = 1, READY_BOUND = 2, BOTH = 3 }
 Type of the ready condition.
 
typedef std::map< std::string, unsigned > func_app_cnt_t
 Per func apply counter.
 
using backend_selector = VlgVerifTgtGenBase::backend_selector
 Type of the backend.
 
using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t
 Type of configuration.
 

Public Member Functions

 VlgSglTgtGen (const std::string &output_path, const InstrPtr &instr_ptr, const InstrLvlAbsPtr &ila_ptr, const VerilogGenerator::VlgGenConfig &config, nlohmann::json &_rf_vmap, nlohmann::json &_rf_cond, VerilogInfo *_vlg_info_ptr, const std::string &vlg_mod_inst_name, const std::string &ila_mod_inst_name, const std::string &wrapper_name, const std::vector< std::string > &implementation_srcs, const std::vector< std::string > &implementation_include_path, const vtg_config_t &vtg_config, backend_selector backend)
 
virtual ~VlgSglTgtGen ()
 Destructor: do nothing , most importantly it is virtual.
 
virtual void ConstructWrapper ()
 
virtual void Export_wrapper (const std::string &wrapper_name)
 create the wrapper file
 
virtual void Export_ila_vlg (const std::string &ila_vlg_name)
 export the ila verilog
 
virtual void Export_script (const std::string &script_name)=0
 export the script to run the verification
 
virtual void Export_problem (const std::string &extra_name)=0
 export extra things (problem)
 
virtual void Export_mem (const std::string &mem_name)=0
 
virtual void Export_modify_verilog ()=0
 For jasper, this means do nothing, for yosys, you need to add (keep)
 
virtual void ExportAll (const std::string &wrapper_name, const std::string &ila_vlg_name, const std::string &script_name, const std::string &extra_name, const std::string &mem_name)
 Take care of exporting all of a single target.
 
virtual void do_not_instantiate (void)=0
 
bool in_bad_state (void) const
 check if this module is in a bad state
 

Protected Member Functions

std::string new_mapping_id ()
 Return a new variable name for mapping.
 
std::string new_property_id ()
 Return a new variable name for property.
 
const ExprPtr IlaGetState (const std::string &sname) const
 Get the pointer of a ila state, it must exist.
 
const ExprPtr IlaGetInput (const std::string &sname) const
 Get the pointer of an ila input, it must exist.
 
std::pair< unsigned, unsigned > GetMemInfo (const std::string &ila_mem_name) const
 Get (a,d) width of a memory, if not existing, (0,0)
 
bool TryFindIlaState (const std::string &sname)
 Test if a string represents an ila state name.
 
bool TryFindIlaInput (const std::string &sname)
 Test if a string represents an ila input name.
 
bool TryFindVlgState (const std::string &sname)
 Test if a string represents a Verilog signal name.
 
ExprPtr TryFindIlaVarName (const std::string &sname)
 Try to find a ILA var according to a name.
 
std::string ModifyCondExprAndRecordVlgName (const VarExtractor::token &t)
 Modify a token and record its use.
 
std::string ReplExpr (const std::string &expr, bool force_vlg_sts=false)
 Parse and modify a condition string.
 
std::string PerStateMap (const std::string &ila_state_name_or_equ, const std::string &vlg_st_name)
 handle a single string map (s-name/equ-string)
 
std::string GetStateVarMapExpr (const std::string &ila_state_name, nlohmann::json &m, bool is_assert=false)
 
void handle_start_condition (nlohmann::json &dc)
 add a start condition if it is given
 
nlohmann::json & get_current_instruction_rf ()
 Find the current instruction mapping.
 
void ConstructWrapper_add_ila_input ()
 add ila input to the wrapper
 
void ConstructWrapper_add_vlg_input_output ()
 add the vlg input ouput to the wrapper I/O
 
void ConstructWrapper_add_cycle_count_moniter ()
 add a cycle counter to be used to deal with the end cycle
 
void ConstructWrapper_generate_header ()
 generate the `define TRUE 1
 
void ConstructWrapper_add_varmap_assumptions ()
 add state equ assumptions
 
void ConstructWrapper_add_varmap_assertions ()
 add state equ assertions
 
void ConstructWrapper_add_inv_assumptions ()
 Add invariants as assumptions.
 
void ConstructWrapper_add_inv_assertions ()
 Add invariants as assertions.
 
void ConstructWrapper_add_additional_mapping_control ()
 Add more assumptions/assertions.
 
void ConstructWrapper_add_condition_signals ()
 Generate ISSUE, IEND, ... signals.
 
void ConstructWrapper_register_extra_io_wire ()
 Register the extra wires to the idr.
 
void ConstructWrapper_add_module_instantiation ()
 Add instantiation statement of the two modules.
 
void ConstructWrapper_add_helper_memory ()
 
void ConstructWrapper_add_uf_constraints ()
 Add buffers and assumption/assertions about the.
 
std::string ConstructWrapper_get_ila_module_inst ()
 get the ila module instantiation string
 
virtual void add_an_assumption (const std::string &aspt, const std::string &dspt)=0
 Add an assumption.
 
virtual void add_an_assertion (const std::string &asst, const std::string &dspt)=0
 Add an assertion.
 
virtual void add_a_direct_assumption (const std::string &aspt, const std::string &dspt)=0
 Add an assumption.
 
virtual void add_a_direct_assertion (const std::string &asst, const std::string &dspt)=0
 Add an assertion.
 
virtual void add_wire_assign_assumption (const std::string &varname, const std::string &expression, const std::string &dspt)=0
 
virtual void add_reg_cassign_assumption (const std::string &varname, const std::string &expression, const std::string &cond, const std::string &dspt)=0
 
bool bad_state_return (void)
 If it is bad state, return true and display a message.
 

Static Protected Member Functions

static unsigned TypeMatched (const ExprPtr &ila_var, const SignalInfoBase &vlg_var)
 
static unsigned get_width (const ExprPtr &n)
 get width of an ila node
 

Protected Attributes

const std::string _output_path
 
InstrPtr _instr_ptr
 The pointer to the instruction that is going to export.
 
InstrLvlAbsPtr _host
 The pointer to the host ila.
 
const std::string _vlg_mod_inst_name
 The name of verilog top module instance in the wrapper.
 
const std::string _ila_mod_inst_name
 The name of ila-verilog top module instance in the wrapper.
 
VerilogGeneratorBase vlg_wrapper
 Generator for the wrapper module.
 
VerilogGenerator vlg_ila
 Generator for the ila verilog.
 
IntefaceDirectiveRecorder _idr
 inteface directive recorder
 
StateMappingDirectiveRecorder _sdr
 state directive recorder
 
VerilogInfovlg_info_ptr
 Analyzer for the implementation.
 
VarExtractor _vext
 variable extractor to handle property expressions
 
nlohmann::json & rf_vmap
 refinement relation variable mapping
 
nlohmann::json & rf_cond
 refinement relation instruction conditions
 
nlohmann::json empty_json
 An empty json for default fallthrough cases.
 
std::map< std::string, ex_info_t_all_referred_vlg_names
 record all the referred vlg names, so you can add (keep) if needed
 
target_type_t target_type
 target type
 
bool has_flush
 a shortcut of whether rf has flush condition set
 
ready_type_t ready_type
 ready type
 
func_app_cnt_t func_cnt
 func apply counter
 
unsigned max_bound
 max bound , default 127
 
unsigned cnt_width
 the width of the counter
 
std::string top_mod_name
 top verilog module name
 
std::string top_file_name
 top verilog module file
 
std::string ila_file_name
 top verilog module file
 
std::vector< std::string > vlg_design_files
 design files
 
std::vector< std::string > vlg_include_files_path
 include paths
 
vtg_config_t _vtg_config
 Store the configuration.
 
backend_selector _backend
 Store the selection of backend.
 

Detailed Description

Generating a target (just the invairant or for an instruction)

Constructor & Destructor Documentation

◆ VlgSglTgtGen()

ilang::VlgSglTgtGen::VlgSglTgtGen ( const std::string &  output_path,
const InstrPtr instr_ptr,
const InstrLvlAbsPtr ila_ptr,
const VerilogGenerator::VlgGenConfig config,
nlohmann::json &  _rf_vmap,
nlohmann::json &  _rf_cond,
VerilogInfo _vlg_info_ptr,
const std::string &  vlg_mod_inst_name,
const std::string &  ila_mod_inst_name,
const std::string &  wrapper_name,
const std::vector< std::string > &  implementation_srcs,
const std::vector< std::string > &  implementation_include_path,
const vtg_config_t vtg_config,
backend_selector  backend 
)
Parameters
[in]outputpath (ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???, modify-impl, it there is )
[in]pointerto the instruction
[in]thehost ila
[in]thedefault configuration for outputing verilog
[in]thevariable map
[in]theconditions
[in]pointerto verify info class
[in]verilogmodule name
[in]ilamodule name
[in]verilogwrapper module name
[in]implemenationsources, can be used to modify and copy
[in]allinclude paths
[in]whichbackend to use, it needs this info to gen proper properties

Member Function Documentation

◆ add_reg_cassign_assumption()

virtual void ilang::VlgSglTgtGen::add_reg_cassign_assumption ( const std::string &  varname,
const std::string &  expression,
const std::string &  cond,
const std::string &  dspt 
)
protectedpure virtual

Add an assignment to a register which in JasperGold could be an assignment, but in CoSA has to be an assumption

Implemented in ilang::VlgSglTgtGen_Cosa, and ilang::VlgSglTgtGen_Jasper.

◆ add_wire_assign_assumption()

virtual void ilang::VlgSglTgtGen::add_wire_assign_assumption ( const std::string &  varname,
const std::string &  expression,
const std::string &  dspt 
)
protectedpure virtual

Add an assignment which in JasperGold could be an assignment, but in CoSA has to be an assumption

Implemented in ilang::VlgSglTgtGen_Cosa, and ilang::VlgSglTgtGen_Jasper.

◆ ConstructWrapper()

virtual void ilang::VlgSglTgtGen::ConstructWrapper ( )
virtual

Call the separate construct functions to make a wrapper (not yet export it)

◆ ConstructWrapper_add_helper_memory()

void ilang::VlgSglTgtGen::ConstructWrapper_add_helper_memory ( )
protected

Add instantiation of the memory and put the needed mem implementation in extra export This also include the assertions

◆ Export_mem()

virtual void ilang::VlgSglTgtGen::Export_mem ( const std::string &  mem_name)
pure virtual

export the memory abstraction (implementation) Yes, this is also implementation specific, (jasper may use a different one)

Implemented in ilang::VlgSglTgtGen_Cosa, and ilang::VlgSglTgtGen_Jasper.

◆ GetStateVarMapExpr()

std::string ilang::VlgSglTgtGen::GetStateVarMapExpr ( const std::string &  ila_state_name,
nlohmann::json &  m,
bool  is_assert = false 
)
protected

handle a var map will create new variables "m?" and return it

  1. "ila-state":"**MEM**.?" 2a. "ila-state":"statename" –> PerStateMap 2b. "ila-state":"(cond)&map" –> PerStateMap
  2. "ila-state":[ "cond&map" ]
  3. "ila-state":[ {"cond":,"map":}, ]

◆ TypeMatched()

static unsigned ilang::VlgSglTgtGen::TypeMatched ( const ExprPtr ila_var,
const SignalInfoBase vlg_var 
)
staticprotected

Check if ila name and vlg name are type compatible (not including special directives)

Member Data Documentation

◆ _output_path

const std::string ilang::VlgSglTgtGen::_output_path
protected

output path, output the ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???


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