ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
Classes | Public Types | Static Public Member Functions | List of all members
ilang::VlgVerifTgtGenBase Class Referenceabstract

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

#include <vtarget_gen.h>

Inheritance diagram for ilang::VlgVerifTgtGenBase:
ilang::VlgVerifTgtGen

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 = 64,
  CHC = YOSYS + 8, Z3PDR = CHC + 1, ELD_CEGAR = CHC + 2, GRAIN_SYGUS = CHC + 4,
  ABCPDR = YOSYS + 16, BTOR_GENERIC = YOSYS + 32
}
 
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

◆ 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

◆ 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: