the class to extract counterexample from a vcd file More...

Public Types
typedef std::string	vlg_val
	a uniform value type (any radix/bool/bv should be fine)

typedef std::map< std::string, vlg_val >	cex_t
	val_name -> val

typedef std::map< std::string, bool >	cex_is_reg_t
	when generating cex, will only use the regs

typedef std::function< bool(const std::string &)>	is_reg_t

Public Member Functions
	CexExtractor (const std::string &vcd_file_name, const std::string &scope, is_reg_t is_reg, bool reg_only)
	to specify the input vcd name and also the scope name (the submodule instance name) to look at

	CexExtractor (const std::string &fin)
	create from a existing file

std::string	GenInvAssert (const std::string &prefix, const std::set< std::string > &focus_name=std::set< std::string >()) const

const cex_t &	GetCex () const
	allow direct access to the counterexample

void	StoreCexToFile (const std::string &fn) const

void	DropStates (const std::vector< std::string > &vnames)

Static Public Member Functions
static void	StoreCexToFile (const std::string &fn, const cex_t &c)

Protected Member Functions
virtual void	parse_from (const std::string &vcd_file_name, const std::string &scope, is_reg_t is_reg, bool reg_only)

Detailed Description

the class to extract counterexample from a vcd file

Member Typedef Documentation

typedef std::function<bool(const std::string&)> ilang::CexExtractor::is_reg_t

a function to determine if some name is a true signal and a register in the original design or not

std::string ilang::CexExtractor::GenInvAssert	(	const std::string &	prefix,
		const std::set< std::string > &	focus_name = `std::set< std::string >()`
	)		const

return a string to be added to the design the argument actually has no use at all

virtual void ilang::CexExtractor::parse_from	(	const std::string &	vcd_file_name,
		const std::string &	scope,
		is_reg_t	is_reg,
		bool	reg_only
	)

protectedvirtual

the helper function to extract info from vcd for future extension, you can replace this function to deal with other file format

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