ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
ilang::VlgVerifTgtGen Class Reference

#include <vtarget_gen_impl.h>

Inheritance diagram for ilang::VlgVerifTgtGen:
ilang::VlgVerifTgtGenBase

Public Member Functions

 VlgVerifTgtGen (const std::vector< std::string > &implementation_include_path, const std::vector< std::string > &implementation_srcs, const std::string &implementation_top_module, const std::string &refinement_variable_mapping, const std::string &refinement_conditions, const std::string &output_path, const InstrLvlAbsPtr &ila_ptr, backend_selector backend, const vtg_config_t &vtg_config, const VerilogGenerator::VlgGenConfig &config=VerilogGenerator::VlgGenConfig(), advanced_parameters_t *adv_ptr=NULL)
 
 VlgVerifTgtGen (const VlgVerifTgtGen &)=delete
 no copy constructor, please
 
VlgVerifTgtGenoperator= (const VlgVerifTgtGen &)=delete
 no assignment, please. I don't want to mess up w. vlg_info_ptr
 
virtual ~VlgVerifTgtGen ()
 release verilog info pointer
 
void GenerateTargets (void)
 Generate everything.
 
bool in_bad_state (void) const
 Return true if it is in bad state.
 
std::string GetVlgModuleInstanceName () const
 get vlg-module instance name
 
const std::vector< std::string > & GetRunnableScriptName () const
 generate the runable script name
 
const VlgTgtSupplementaryInfoGetSupplementaryInfo () const
 return the result from parsing supplymentary information
 

Protected Member Functions

bool bad_state_return (void)
 subroutine for generating synthesis using chc targets More...
 
void load_json (const std::string &fname, nlohmann::json &j)
 load json from a file name to the given j
 
void set_module_instantiation_name ()
 Get instance name from rfmap.
 

Protected Attributes

const std::vector< std::string > _vlg_impl_include_path
 implementation include path
 
const std::vector< std::string > _vlg_impl_srcs
 implementatino path
 
const std::string _vlg_impl_top_name
 implementation top module name
 
const std::string _rf_var_map_name
 refinement relation - variable mapping path
 
const std::string _rf_cond_name
 refinement relation - condition path
 
const std::string _output_path
 
const InstrLvlAbsPtr_ila_ptr
 The pointer to the instruction that is going to export.
 
std::string _vlg_mod_inst_name
 The name of verilog top module instance in the wrapper.
 
std::string _ila_mod_inst_name
 The name of ila-verilog top module instance in the wrapper.
 
VerilogInfovlg_info_ptr
 A pointer to create verilog analyzer.
 
backend_selector _backend
 to store the backend
 
VerilogGenerator::VlgGenConfig _cfg
 to store the verilog configuration
 
vtg_config_t _vtg_config
 to store the configuration
 
advanced_parameters_t_advanced_param_ptr
 to store the advanced parameter configurations
 
std::vector< std::string > runnable_script_name
 to store the generate script name
 
nlohmann::json rf_vmap
 store the vmap info
 
nlohmann::json rf_cond
 store the condition
 
VlgTgtSupplementaryInfo supplementary_info
 The supplementary information.
 

Additional Inherited Members

- Public Types inherited from ilang::VlgVerifTgtGenBase
enum  backend_selector {
  NONE = 0, COSA = 1, JASPERGOLD = 2, YOSYS = 64,
  CHC = YOSYS + 8, Z3PDR = CHC + 1, ELD_CEGAR = CHC + 2, GRAIN_SYGUS = CHC + 4,
  ABCPDR = YOSYS + 16, BTOR_GENERIC = YOSYS + 32
}
 
enum  synthesis_backend_selector {
  Z3 = Z3PDR ^ YOSYS, GRAIN = GRAIN_SYGUS ^ YOSYS, ABC = ABCPDR ^ YOSYS, ELDERICA = ELD_CEGAR ^ YOSYS,
  NOSYN = BTOR_GENERIC ^ YOSYS
}
 Type of invariant synthesis backend.
 
enum  _chc_target_t { CEX, INVCANDIDATE, GENERAL_PROPERTY }
 Type of the chc target.
 
typedef struct ilang::VlgVerifTgtGenBase::_vtg_config vtg_config_t
 Verilog Target Generation Configuration.
 
typedef struct ilang::VlgVerifTgtGenBase::_adv_parameters advanced_parameters_t
 
- Static Public Member Functions inherited from ilang::VlgVerifTgtGenBase
static bool isValidVerifBackend (backend_selector vbackend)
 check if a backend selector is valid
 

Detailed Description

brief Class of Verilog verification target generation, not to be used outside

Constructor & Destructor Documentation

◆ VlgVerifTgtGen()

ilang::VlgVerifTgtGen::VlgVerifTgtGen ( const std::vector< std::string > &  implementation_include_path,
const std::vector< std::string > &  implementation_srcs,
const std::string &  implementation_top_module,
const std::string &  refinement_variable_mapping,
const std::string &  refinement_conditions,
const std::string &  output_path,
const InstrLvlAbsPtr ila_ptr,
backend_selector  backend,
const vtg_config_t vtg_config,
const VerilogGenerator::VlgGenConfig config = VerilogGenerator::VlgGenConfig(),
advanced_parameters_t adv_ptr = NULL 
)
Parameters
[in]implementation'sinclude path (if it uses `include)
[in]verilog'spath, currently we only handle situation where all in the same folder
[in]nameof the top module of the implementation, leave "" to allow auto analysis
[in]whereto get variable mapping
[in]whereto get refinement relation
[in]outputpath (ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???, modify-impl, it there is )
[in]pointerto the ila
[in](optional)the default configuration for outputing verilog

Member Function Documentation

◆ bad_state_return()

bool ilang::VlgVerifTgtGen::bad_state_return ( void  )
protected

subroutine for generating synthesis using chc targets

If it is bad state, return true and display a message

Member Data Documentation

◆ _output_path

const std::string ilang::VlgVerifTgtGen::_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: