Inheritance diagram for ilang::VlgVerifTgtGen:

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

VlgVerifTgtGen &	operator= (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 VlgTgtSupplementaryInfo &	GetSupplementaryInfo () 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.

VerilogInfo *	vlg_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 = 128, CHC = YOSYS + 8, Z3PDR = CHC + 1, ELD_CEGAR = CHC + 2, GRAIN_SYGUS = CHC + 4, ABCPDR = YOSYS + 16, BTOR_GENERIC = YOSYS + 32, RELCHC = YOSYS + 64 }

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

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's	include path (if it uses `include)
[in]	verilog's	path, currently we only handle situation where all in the same folder
[in]	name	of the top module of the implementation, leave "" to allow auto analysis
[in]	where	to get variable mapping
[in]	where	to get refinement relation
[in]	output	path (ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???, modify-impl, it there is )
[in]	pointer	to the ila
[in]	(optional)	the default configuration for outputing verilog

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

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: