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

#include <vtarget_gen_impl.h>

Inheritance diagram for ilang::VlgSglTgtGen:

Public Types
enum	target_type_t { INVARIANTS, INSTRUCTIONS, INV_SYN_DESIGN_ONLY }
	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 verification backend.

using	synthesis_backend_selector = VlgVerifTgtGenBase::synthesis_backend_selector
	Type of the synthesis backend.

using	vtg_config_t = VlgVerifTgtGenBase::vtg_config_t
	Type of configuration.

using	ex_info_t = VlgVerifTgtGenBase::ex_info_t
	Type of record of extra info of a signal.

using	advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t
	Type of advanced parameter.

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, VlgTgtSupplementaryInfo &_supplementary_info, 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, const target_type_t &target_tp, advanced_parameters_t adv_ptr)

virtual	~VlgSglTgtGen ()
	Destructor: do nothing , most importantly it is virtual.

virtual void	ConstructWrapper ()

virtual void	PreExportProcess ()=0
	PreExportWork (modification and etc.)

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_reset_setup ()
	setup reset, add assumptions if necessary

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_assumption_or_assertion_target_invariant ()
	Add invariants as assumption/assertion when target is invariant.

void	ConstructWrapper_add_inv_assumption_or_assertion_target_instruction ()
	Add invariants as assumption/assertion when target is instruction.

void	ConstructWrapper_add_additional_mapping_control ()
	Add more assumptions for mapping (only use for instruction target)

void	ConstructWrapper_add_rf_assumptions ()
	Add more assumptions for I/O for example (both instruction/invariant)

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.

void	ConstructWrapper_add_post_value_holder ()
	Add post value holder (val @ cond == ...)

int	ConstructWrapper_add_post_value_holder_handle_obj (nlohmann::json &pv_cond_val, const std::string &pv_name, int width, bool create_reg)
	A sub function of the above post-value-holder hanlder.

void	ConstructWrapper_add_vlg_monitor ()
	Add Verilog inline monitor.

void	ConstructWrapper_add_inv_assumption_or_assertion_target_inv_syn_design_only ()
	Add invariants as assumption/assertion when target is inv_syn_design_only.

void	ConstructWrapper_inv_syn_connect_mem ()
	Connect the memory even we don't care a lot about them.

void	ConstructWrapper_inv_syn_cond_signals ()

std::string	ConstructWrapper_get_ila_module_inst ()
	get the ila module instantiation string

void	add_inv_obj_as_assertion (InvariantObject *inv_obj)
	add an invariant object as assertion

void	add_inv_obj_as_assumption (InvariantObject *inv_obj)
	add an invariant object as an assumption

void	add_rf_inv_as_assumption ()
	add rf inv as assumptions (if there are)

void	add_rf_inv_as_assertion ()
	add rf inv as assumptions (if there are)

virtual void	add_a_direct_assumption (const std::string &aspt, const std::string &dspt)=0
	Add an assumption – backend dependent.

virtual void	add_a_direct_assertion (const std::string &asst, const std::string &dspt)=0
	Add an assertion.

virtual void	add_an_assumption (const std::string &aspt, const std::string &dspt)
	Add an assumption – JasperGold will override this.

virtual void	add_an_assertion (const std::string &asst, const std::string &dspt)
	Add an assertion – JasperGold will override this.

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

virtual void	add_reg_cassign_assumption (const std::string &varname, const std::string &expression, int width, const std::string &cond, const std::string &dspt)

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

VerilogInfo *	vlg_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.

const VlgTgtSupplementaryInfo &	supplementary_info
	The supplementary information.

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

advanced_parameters_t *	_advanced_param_ptr
	to store the advanced parameter configurations

const bool	has_gussed_synthesized_invariant
	has guessed synthesized invariant

const bool	has_confirmed_synthesized_invariant
	has confirmed synthesized invariant

const bool	has_rf_invariant
	has rf provided invariant

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.

const VerilogGenerator::VlgGenConfig &	_vlg_cfg
	Store the vlg configurations.

backend_selector	_backend
	Store the selection of backend.

Detailed Description

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

Constructor & Destructor Documentation

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,
		VlgTgtSupplementaryInfo &	_supplementary_info,
		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,
		const target_type_t &	target_tp,
		advanced_parameters_t *	adv_ptr
	)

Parameters

[in]	output	path (ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???, modify-impl, it there is )
[in]	pointer	to the instruction
[in]	the	host ila
[in]	the	default configuration for outputing verilog
[in]	the	variable map
[in]	the	conditions
[in]	pointer	to verify info class
[in]	verilog	module name
[in]	ila	module name
[in]	verilog	wrapper module name
[in]	implemenation	sources, can be used to modify and copy
[in]	all	include paths
[in]	which	backend to use, it needs this info to gen proper properties

Member Function Documentation

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

protectedvirtual

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

Reimplemented in ilang::VlgSglTgtGen_Jasper.

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

protectedvirtual

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

Reimplemented in ilang::VlgSglTgtGen_Jasper.

virtual void ilang::VlgSglTgtGen::ConstructWrapper ( )

virtual

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

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

void ilang::VlgSglTgtGen::ConstructWrapper_inv_syn_cond_signals ( )

protected

Sometimes you need to add some signals that only appeared in Instruction target

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_Yosys, ilang::VlgSglTgtGen_Relchc, ilang::VlgSglTgtGen_Cosa, and ilang::VlgSglTgtGen_Jasper.

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

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

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

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:

vtarget_gen_impl.h

Public Types

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation