ilang::VlgVerifTgtGenBase Class Reference

VlgVerifTgtGenBase: do nothing, should not instantiate. More...

#include <vtarget_gen.h>

Inheritance diagram for ilang::VlgVerifTgtGenBase:

Classes
struct	_adv_parameters
struct	_vtg_config
	Verilog Target Generation Configuration. More...
struct	ex_info_t

Public Types
enum	backend_selector {   NONE = 0, COSA = 1, JASPERGOLD = 2, YOSYS = 128,   CHC = YOSYS + 8, Z3PDR = CHC + 1, ELD_CEGAR = CHC + 2, GRAIN_SYGUS = CHC + 4,   ABCPDR = YOSYS + 16, BTOR_GENERIC = YOSYS + 32, RELCHC = YOSYS + 64 }
enum	synthesis_backend_selector {   Z3 = Z3PDR ^ YOSYS, GRAIN = GRAIN_SYGUS ^ YOSYS, ABC = ABCPDR ^ YOSYS, ELDERICA = ELD_CEGAR ^ YOSYS,   NOSYN = BTOR_GENERIC ^ YOSYS }
	Type of invariant synthesis backend.
enum	_chc_target_t { CEX, INVCANDIDATE, GENERAL_PROPERTY }
	Type of the chc target.
typedef struct ilang::VlgVerifTgtGenBase::_vtg_config	vtg_config_t
	Verilog Target Generation Configuration.
typedef struct ilang::VlgVerifTgtGenBase::_adv_parameters	advanced_parameters_t

Static Public Member Functions
static bool	isValidVerifBackend (backend_selector vbackend)
	check if a backend selector is valid

Detailed Description

VlgVerifTgtGenBase: do nothing, should not instantiate.

Member Typedef Documentation

typedef struct ilang::VlgVerifTgtGenBase::_adv_parameters ilang::VlgVerifTgtGenBase::advanced_parameters_t

Advanced parameters used for invariant synthesizer should not be used by generat NOTE: this function can be inherited and only expose a visible interface to the outside

Member Enumeration Documentation

enum ilang::VlgVerifTgtGenBase::backend_selector

Type of the backend: CoSA, JasperGold, CHC for chc solver, AIGER for abc

---

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

• vtarget_gen.h