ilang::VlgSglTgtGen_Yosys Class Reference

a class to interface w. Yosys More...

#include <vtarget_gen_yosys.h>

Inheritance diagram for ilang::VlgSglTgtGen_Yosys:

Public Types
using	target_type_t = VlgSglTgtGen::target_type_t
	using the target type
using	info_t = VerilogModifier::info_t
	a tuple to store all related info for modification
using	fn_l_map_t = VerilogModifier::fn_l_map_t
	filename -> (lineno, varname, is_port_sig) vec
using	advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t
	Type of advanced parameter.
using	_chc_target_t = VlgVerifTgtGenBase::_chc_target_t
	Type of yosys target.
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.

Public Member Functions
	VlgSglTgtGen_Yosys (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 &_sup_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 vbackend, const target_type_t &target_tp, advanced_parameters_t *adv_ptr, _chc_target_t chc_target)
virtual	~VlgSglTgtGen_Yosys ()
	do nothing
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) override
	overwrite the Export
std::shared_ptr < smt::YosysSmtParser >	GetDesignSmtInfo () const
	accessor of the design info
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
bool	in_bad_state (void) const
	check if this module is in a bad state

Protected Member Functions
virtual void	add_a_direct_assumption (const std::string &aspt, const std::string &dspt) override
	Add a direct assumption – needed by base class.
virtual void	add_a_direct_assertion (const std::string &asst, const std::string &dspt) override
	Add a direct assertion – needed by base class.
virtual void	PreExportProcess () override
	Pre export work : add assume and asssert to the top level.
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: the chc script, the smt template
virtual void	Export_mem (const std::string &mem_name) override
virtual void	Export_modify_verilog () override
	For jasper, this means do nothing, for chc, 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)
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.

Protected Attributes
Yosys_problem	_problems
	Yosys problem generate.
std::string	prob_fname
	Yosys problem file name.
std::string	run_script_name
	Yosys script 'run.sh' name.
synthesis_backend_selector	s_backend
	the synthesis backend
std::shared_ptr < smt::YosysSmtParser >	design_smt_info
	the smt info of the design
bool	generate_proof
	whether to require a proof
_chc_target_t	chc_target
	what are the targets
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
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

a class to interface w. Yosys

Constructor & Destructor Documentation

ilang::VlgSglTgtGen_Yosys::VlgSglTgtGen_Yosys	(	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 &	_sup_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	vbackend,
		const target_type_t &	target_tp,
		advanced_parameters_t *	adv_ptr,
		_chc_target_t	chc_target
	)

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

virtual void ilang::VlgSglTgtGen_Yosys::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.

---

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

• vtarget_gen_yosys.h