Verilog Verification Target Generator – for JasperGold Unlike for cosa, we don't need a separate file although we do have some ... More...

#include <vtarget_gen_jasper.h>

Inheritance diagram for ilang::VlgSglTgtGen_Jasper:

Public Member Functions
	VlgSglTgtGen_Jasper (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 > &include_dirs, const vtg_config_t &vtg_config, backend_selector backend, const target_type_t &target_tp, advanced_parameters_t adv_ptr)

void	add_addition_clock_info (const std::string &expr)

void	add_addition_reset_info (const std::string &expr)

virtual void	do_not_instantiate (void) override
	It is okay to instantiation.

Public Member Functions inherited from 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)

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	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.

bool	in_bad_state (void) const
	check if this module is in a bad state

Protected Member Functions
virtual void	add_an_assumption (const std::string &aspt, const std::string &dspt) override
	Add an assumption.

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

virtual void	add_a_direct_assumption (const std::string &aspt, const std::string &dspt) override
	Add a direct assumption.

virtual void	add_a_direct_assertion (const std::string &asst, const std::string &dspt) override
	Add a direct assertion.

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

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

virtual void	PreExportProcess () override
	Pre export work : nothing for cosa.

virtual void	Export_script (const std::string &script_name) override
	export the script to run the verification

virtual void	Export_problem (const std::string &extra_name) override
	export extra things (problem)

virtual void	Export_mem (const std::string &mem_name) override

virtual void	Export_modify_verilog () override
	For jasper, this means do nothing, for yosys, you need to add (keep)

Protected Member Functions inherited from ilang::VlgSglTgtGen
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)

bool	bad_state_return (void)
	If it is bad state, return true and display a message.

Protected Attributes
std::vector< std::pair < std::string, std::string > >	assumptions

std::vector< std::pair < std::string, std::string > >	assertions
	vector of pairs of <assertions, description>

std::vector< std::string >	additional_clock_expr
	vector of clock signals that need to be taken care of

std::vector< std::string >	additional_reset_expr
	vector of clock signals that need to be taken care of

std::string	jg_script_name
	Name of the problem file.

std::string	abs_mem_name
	Name of the problem file.

Protected Attributes inherited from ilang::VlgSglTgtGen
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.

Additional Inherited Members
Public Types inherited from ilang::VlgSglTgtGen
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.

Static Protected Member Functions inherited from ilang::VlgSglTgtGen
static unsigned	TypeMatched (const ExprPtr &ila_var, const SignalInfoBase &vlg_var)

static unsigned	get_width (const ExprPtr &n)
	get width of an ila node

Detailed Description

Verilog Verification Target Generator – for JasperGold Unlike for cosa, we don't need a separate file although we do have some ...

Constructor & Destructor Documentation

ilang::VlgSglTgtGen_Jasper::VlgSglTgtGen_Jasper	(	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 > &	include_dirs,
		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	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]	all	implementation sources
[in]	all	include paths
[in]	which	backend to use, it needs this info to gen proper properties

Member Function Documentation

void ilang::VlgSglTgtGen_Jasper::add_addition_clock_info ( const std::string & expr )

if you have signals that are controled by assumptions to be equal as the outer clock, you need to put them here, because the assumptions do not work in the jaspergold reset step (unlike COSA)

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

overrideprotectedvirtual

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

Reimplemented from ilang::VlgSglTgtGen.

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

overrideprotectedvirtual

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

Reimplemented from ilang::VlgSglTgtGen.

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

overrideprotectedvirtual

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

Implements ilang::VlgSglTgtGen.

Member Data Documentation

std::vector<std::pair<std::string, std::string> > ilang::VlgSglTgtGen_Jasper::assumptions

protected

internal storage of problems vector of pairs of <assumption, description>

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

vtarget_gen_jasper.h

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation