vtarget_gen.h

// --- Hongce Zhang

#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_H__
#define ILANG_VTARGET_OUT_VTARGET_GEN_H__

#include <ilang/config.h>
#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/verilog-out/verilog_gen.h>
#include <ilang/vtarget-out/inv-syn/cex_extract.h>
#include <ilang/vtarget-out/inv-syn/inv_obj.h>

namespace ilang {

class VlgVerifTgtGenBase {
  // ----------------------- Type Definition ----------------------- //
public:
  struct ex_info_t {
    std::string range;
    ex_info_t(const std::string& r) : range(r) {}
  };

  // ----------- Verification Settings -------------- //
  // YOSYS is for invariant synthesis use
  typedef enum {
    NONE = 0,
    COSA = 1,
    JASPERGOLD = 2,
    YOSYS = 128,              // 10000000
    CHC = YOSYS + 8,          // 10001000
    Z3PDR = CHC + 1,          // 10001001
    ELD_CEGAR = CHC + 2,      // 10001010
    GRAIN_SYGUS = CHC + 4,    // 10001100
    ABCPDR = YOSYS + 16,      // 10010000
    BTOR_GENERIC = YOSYS + 32,// 10100000
    RELCHC = YOSYS + 64       // 11000000
  } backend_selector;
  typedef enum {
    Z3 = Z3PDR ^ YOSYS,
    GRAIN = GRAIN_SYGUS ^ YOSYS,
    ABC = ABCPDR ^ YOSYS,        
    ELDERICA = ELD_CEGAR ^ YOSYS,// 0001010
    NOSYN = BTOR_GENERIC ^ YOSYS // 1000000
  } synthesis_backend_selector;
  enum _chc_target_t { CEX, INVCANDIDATE, GENERAL_PROPERTY };
  typedef struct _vtg_config {
    std::string WrapperPreheader;
    enum { INST, INV, BOTH } target_select;
    std::string CheckThisInstructionOnly;
    bool InstructionNoReset; // true
    bool OnlyCheckInstUpdatedVars; // true
    bool IteUnknownAutoIgnore; // false
    bool VerificationSettingAvoidIssueStage;
    enum _validate_synthesized_inv {
      NOINV,
      CANDIDATE,
      CONFIRMED,
      ALL
    } ValidateSynthesizedInvariant;

    // ----------- Options for CoSA settings -------------- //
    bool PerVariableProblemCosa; // true
    bool MemAbsReadAbstraction; // false
    bool ForceInstCheckReset;
    enum { AUTO = 0, NEW = 1, OLD = 2 } PortDeclStyle;
    bool CosaGenJgTesterScript;
    bool CosaFullTrace;
    bool CosaAddKeep;
    enum CosaDotReferenceNotify_t {
      NOTIFY_PANIC = 0,
      NOTIFY_WARNING = 1,
      NOTIFY_IGNORE = 2
    } CosaDotReferenceNotify;
    // The bound of BMC, default 127
    unsigned MaxBound;
    bool OnlyAssumeUpdatedVarsEq; // should be false


    // ----------- Options for CoSA script -------------- //
    std::string CosaPath;
    std::string CosaPyEnvironment;
    std::string CosaSolver;
    bool CosaGenTraceVcd;
    bool CosaAssumptionOverlyConstrainedCheck;
    std::string CosaOtherSolverOptions;

    // ----------- Options for Yosys SMT-LIB2 Generator -------------- //
    std::string YosysPath;
    bool YosysUndrivenNetAsInput;
    bool YosysSmtFlattenHierarchy;
    bool YosysSmtFlattenDatatype;
    bool YosysPropertyCheckShowProof;
    bool YosysSmtArrayForRegFile;
    typedef enum {
      UnintepretedFunc /*not supported*/,
      Datatypes, /*by default*/
      BitVec     /*optional for property check, not inv-syn*/
    } _state_sort_t;
    _state_sort_t YosysSmtStateSort;
    bool InvariantSynthesisKeepMemory;
    bool InvariantCheckKeepMemory;
    bool InvariantSynthesisReachableCheckKeepOldInvariant;

    // ----------- Options for CHC Solver -------------- //
    bool ChcWordBlastArray;
    bool ChcAssumptionsReset;
    bool ChcAssumptionNextState;
    bool ChcAssumptionEnd;

    // ----------- Options for Btor Output -------------- //
    std::string BtorGenericCmdline;
    bool BtorSingleProperty;
    bool BtorAddCommentsInOutputs;

    // ----------- Options for Z3/Grain/ABC Solver -------------- //
    std::string Z3Path;
    std::string GrainPath;
    std::vector<std::string> GrainOptions;
    bool GrainHintsUseCnfStyle;
    std::string AbcPath;

    // ----------- Extended Options for ABC Solver -------------- //
    bool AbcUseGla;
    unsigned AbcGlaTimeLimit;
    unsigned AbcGlaFrameLimit;
    bool AbcUseCorr;
    bool AbcUseAiger;
    bool AbcMinimizeInv;
    typedef enum _abc_assumption_style_t {
      AigMiterExtraOutput =
          0, // Use AIG's extra output to represent, cannot use with GLA
      AssumptionRegister =
          1 // Use extra register, may have issues in interpreting the invariant
    } AbcAssumptionStyle_t;
    AbcAssumptionStyle_t AbcAssumptionStyle;

    // ----------- Extended Options for Grain -------------- //

    _vtg_config()
        : target_select(BOTH), CheckThisInstructionOnly(""),
          InstructionNoReset(true), OnlyCheckInstUpdatedVars(true),
          IteUnknownAutoIgnore(false),
          VerificationSettingAvoidIssueStage(false),
          ValidateSynthesizedInvariant(ALL),

          // ----------- Options for CoSA settings -------------- //
          PerVariableProblemCosa(false), MemAbsReadAbstraction(false),
          ForceInstCheckReset(false), PortDeclStyle(AUTO),
          CosaGenJgTesterScript(false), CosaFullTrace(false), CosaAddKeep(true),
          CosaDotReferenceNotify(CosaDotReferenceNotify_t::NOTIFY_PANIC),
          MaxBound(127), OnlyAssumeUpdatedVarsEq(false),

          // ----------- Options for CoSA script -------------- //
          CosaPath(""), CosaPyEnvironment(""), CosaSolver(""),
          CosaGenTraceVcd(true), CosaAssumptionOverlyConstrainedCheck(false),
          CosaOtherSolverOptions(""),

          // ----------- Options for Yosys SMT-LIB2 Generator -------------- //
          YosysUndrivenNetAsInput(true), YosysSmtFlattenHierarchy(true),
          YosysSmtFlattenDatatype(false), YosysPropertyCheckShowProof(false),
          YosysSmtArrayForRegFile(false),
          YosysSmtStateSort(Datatypes), InvariantSynthesisKeepMemory(true),
          InvariantCheckKeepMemory(true),
          InvariantSynthesisReachableCheckKeepOldInvariant(false),

          // ----------- Options for CHCs -------------- //
          ChcWordBlastArray(true), ChcAssumptionsReset(false),
          ChcAssumptionNextState(false), ChcAssumptionEnd(false),

          // ----------- Options for Btor Output -------------- //
          BtorSingleProperty(true),
          BtorAddCommentsInOutputs(false),

          // ----------- Options for Z3/Grain/ABC Solver -------------- //
          GrainHintsUseCnfStyle(true),

          // ----------- Options for ABC -------------- //
          AbcUseGla(false), AbcGlaTimeLimit(500), AbcGlaFrameLimit(200),
          AbcUseCorr(false), AbcUseAiger(true), AbcMinimizeInv(false),
          AbcAssumptionStyle(_abc_assumption_style_t::AigMiterExtraOutput)

    {}
  } vtg_config_t;

  typedef struct _adv_parameters {
    InvariantObject* _inv_obj_ptr;
    InvariantObject* _candidate_inv_ptr;
    CexExtractor* _cex_obj_ptr;
    _adv_parameters()
        : _inv_obj_ptr(NULL), _candidate_inv_ptr(NULL), _cex_obj_ptr(NULL) {}
    virtual ~_adv_parameters(){};
  } advanced_parameters_t;

public:
  // ----------------------- Constructor/Destructor ----------------------- //
  // constructor : do nothing
  VlgVerifTgtGenBase() {}
  // destructor : do nothing (make it virtual !!!)
  virtual ~VlgVerifTgtGenBase() {}
  static bool isValidVerifBackend(backend_selector vbackend);

private:
  // avoid instantiation
  virtual void do_not_instantiate(void) = 0;
}; // class VlgVerifTgtGenBase

class VerilogVerificationTargetGenerator {
public:
  using backend_selector = VlgVerifTgtGenBase::backend_selector;
  using synthesis_backend_selector =
      VlgVerifTgtGenBase::synthesis_backend_selector;
  using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VerilogVerificationTargetGenerator(
      const std::vector<std::string>& implementation_include_path,
      const std::vector<std::string>& implementation_srcs,
      const std::string& implementation_top_module,
      const std::string& refinement_variable_mapping,
      const std::string& refinement_conditions, const std::string& output_path,
      const InstrLvlAbsPtr& ila_ptr, backend_selector backend,
      const vtg_config_t& vtg_config = vtg_config_t(),
      const VerilogGenerator::VlgGenConfig& config =
          VerilogGenerator::VlgGenConfig());
  // --------------------- DECONSTRUCTOR ---------------------------- //
  virtual ~VerilogVerificationTargetGenerator();

  void GenerateTargets(void);
  bool in_bad_state(void) const;
  std::string GetVlgModuleInstanceName(void) const;

private:
  VlgVerifTgtGenBase* _generator;

}; // VerilogVerificationTargetGenerator

}; // namespace ilang

#endif // ILANG_VTARGET_OUT_VTARGET_GEN_H__