ilang::VlgVerifTgtGenBase::_vtg_config Struct Reference

Verilog Target Generation Configuration. More...

#include <vtarget_gen.h>

Public Types
enum	{ INST, INV, BOTH }
	Set the targets: instructions/invariants/both.
enum	_validate_synthesized_inv { NOINV, CANDIDATE, CONFIRMED, ALL }
enum	{ AUTO = 0, NEW = 1, OLD = 2 }
	For COSA target generator : whether to force NEW/OLD port declaration.
enum	CosaDotReferenceNotify_t { NOTIFY_PANIC = 0, NOTIFY_WARNING = 1, NOTIFY_IGNORE = 2 }
enum	_state_sort_t { UnintepretedFunc, Datatypes, BitVec }
enum	_abc_assumption_style_t { AigMiterExtraOutput, AssumptionRegister }
	ABC option : the way to handle assumptions.
typedef enum ilang::VlgVerifTgtGenBase::_vtg_config::_abc_assumption_style_t	AbcAssumptionStyle_t
	ABC option : the way to handle assumptions.

Public Member Functions
	_vtg_config ()
	The default constructor for default values.

Public Attributes
std::string	WrapperPreheader
	Preheader Content : will use in all targets.
enum ilang::VlgVerifTgtGenBase::_vtg_config:: { ... }	target_select
	Set the targets: instructions/invariants/both.
std::string	CheckThisInstructionOnly
	If not an empty string, then only check for that instruction.
bool	InstructionNoReset
bool	OnlyCheckInstUpdatedVars
bool	IteUnknownAutoIgnore
bool	VerificationSettingAvoidIssueStage
	whether to remove the extra issue cycle and starts from reset
enum ilang::VlgVerifTgtGenBase::_vtg_config::_validate_synthesized_inv	ValidateSynthesizedInvariant
bool	PerVariableProblemCosa
	Do we set separate problems for different var map (CoSA only)
bool	MemAbsReadAbstraction
	Whether to abstract the memory read.
bool	ForceInstCheckReset
	Whether to force the instruction check to start from reset state.
enum ilang::VlgVerifTgtGenBase::_vtg_config:: { ... }	PortDeclStyle
	For COSA target generator : whether to force NEW/OLD port declaration.
bool	CosaGenJgTesterScript
	Generate a jg script to help validate cosa?
bool	CosaFullTrace
	generate the trace for all variables? or just the relevent variables
bool	CosaAddKeep
enum ilang::VlgVerifTgtGenBase::_vtg_config::CosaDotReferenceNotify_t	CosaDotReferenceNotify
unsigned	MaxBound
bool	OnlyAssumeUpdatedVarsEq
	Only enforce var eq on updated vars, should not be used.
std::string	CosaPath
	If not empty, the generated script will include the path of Cosa.
std::string	CosaPyEnvironment
	If not empty, the generated script will include sourcing a script.
std::string	CosaSolver
	A choice of solver (in the script)
bool	CosaGenTraceVcd
	Whether the Solver should generate vcd trace.
bool	CosaAssumptionOverlyConstrainedCheck
	Assumption overly constrained check.
std::string	CosaOtherSolverOptions
	other CoSA options
std::string	YosysPath
	The path to yosys, if yosys is not in the PATH, default empty.
bool	YosysUndrivenNetAsInput
bool	YosysSmtFlattenHierarchy
	Whether to flatten the module hierarchy.
bool	YosysSmtFlattenDatatype
	Whether to flatten the datatypes.
bool	YosysPropertyCheckShowProof
	when used in property verification, show prove?
bool	YosysSmtArrayForRegFile
_state_sort_t	YosysSmtStateSort
bool	InvariantSynthesisKeepMemory
bool	InvariantCheckKeepMemory
	for invariant check, do we keep memory abstraction in Verilog
bool	InvariantSynthesisReachableCheckKeepOldInvariant
bool	ChcWordBlastArray
	CHC, whether to turn array into individual registers.
bool	ChcAssumptionsReset
	CHC, whether to force assumption on the init.
bool	ChcAssumptionNextState
	CHC, whether to force assumption on the next T.
bool	ChcAssumptionEnd
	CHC, whether to force assumption on the end T.
std::string	BtorGenericCmdline
bool	BtorSingleProperty
	CHC, whether to turn array into individual registers.
bool	BtorAddCommentsInOutputs
	CHC, whether to force assumption on the init.
std::string	Z3Path
	The path to Z3, if "z3" is not in the PATH, default empty.
std::string	GrainPath
	The path to Grain, if "grain" is not in the PATH, default empty.
std::vector< std::string >	GrainOptions
	Grain Configuration Options.
bool	GrainHintsUseCnfStyle
	FreqHorn style (cocistyple, cnfstyle)
std::string	AbcPath
	The path to ABC, if "abc" is not in the PATH, default empty.
bool	AbcUseGla
	ABC option : whether to use gate-level abstraction.
unsigned	AbcGlaTimeLimit
	ABC option : gate-level abstraction time limit.
unsigned	AbcGlaFrameLimit
	ABC option : gate-level abstraction frame limit.
bool	AbcUseCorr
	ABC option : whether to use correlation analysis.
bool	AbcUseAiger
	ABC option : whether to pass aiger to ABC.
bool	AbcMinimizeInv
	ABC option : whether to minimize invariant.
AbcAssumptionStyle_t	AbcAssumptionStyle

Detailed Description

Verilog Target Generation Configuration.

Member Enumeration Documentation

enum ilang::VlgVerifTgtGenBase::_vtg_config::_state_sort_t

How to encode Verilog state DataSort seems to use PDR engine

enum ilang::VlgVerifTgtGenBase::_vtg_config::_validate_synthesized_inv

Configure the behavior of INV target, if false, will not check synthesized invariants by default (unless call generateInvariantVerificationTarget) if true, will check by default

enum ilang::VlgVerifTgtGenBase::_vtg_config::CosaDotReferenceNotify_t

whether to force dot reference check in the generation if you expect to use cosa on the it, yes, you need to use the default setting : NOTIFY_PANIC in some rare cases, you may want to use JasperGold after it in that case, it is okay to just ignore it

Member Data Documentation

std::string ilang::VlgVerifTgtGenBase::_vtg_config::BtorGenericCmdline

in the format of "xxxx [options] %btorfile% [options]" will replace btorfile% with the file

bool ilang::VlgVerifTgtGenBase::_vtg_config::CosaAddKeep

For CoSA backend: do we add (* keep *)? default true, however, it can be buggy, so you can disable it if you want

bool ilang::VlgVerifTgtGenBase::_vtg_config::InstructionNoReset

Ensure the instruction will not be reseted while in the whole execution of checking instruction from reseted –> to forever

bool ilang::VlgVerifTgtGenBase::_vtg_config::InvariantSynthesisKeepMemory

for invariant synthesis do we keep memory abstraction in Verilog you can keep it true, untill the invariant refers to some memory there

bool ilang::VlgVerifTgtGenBase::_vtg_config::InvariantSynthesisReachableCheckKeepOldInvariant

Whether to assume the old invariants when check for reachability It seems for Z3, setting this to be false is faster (I don't know why) For grain-enhance, this will be (internally) overwritten to be true

bool ilang::VlgVerifTgtGenBase::_vtg_config::IteUnknownAutoIgnore

A shortcut for SetUpdate(s, Ite(c, v, unknown() )) will only gnerate map like : ( ila.c => ila.v == vlg.v ) In this case, you don't need to deal with unknown in func map nor do you need to create a special refinement map function has to be defined as __unknown__X

bool ilang::VlgVerifTgtGenBase::_vtg_config::OnlyCheckInstUpdatedVars

Does not insert assertions of variable mapping if an instruction does not update that var

bool ilang::VlgVerifTgtGenBase::_vtg_config::YosysSmtArrayForRegFile

Whether to word-blast array or use SMT Array By default will word-blast

bool ilang::VlgVerifTgtGenBase::_vtg_config::YosysUndrivenNetAsInput

whether to explicitly turn the undriven net to input for smt-backend, the top level undriven net seems always turned into inputs, but the lower level may not

---

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

• vtarget_gen.h