inv_syn_cegar.h

// ---Hongce Zhang

#ifndef ILANG_VTARGET_OUT_INV_SYN_CEGAR_H__
#define ILANG_VTARGET_OUT_INV_SYN_CEGAR_H__

#include <ilang/config.h>
#ifdef INVSYN_INTERFACE

#include <ilang/smt-inout/yosys_smt_parser.h>
#include <ilang/vtarget-out/design_stat.h>
#include <ilang/vtarget-out/vtarget_gen.h>

#include <memory>
#include <string>

namespace ilang {

class InvariantSynthesizerCegar {

public:
  // -------------------- TYPES ------------------ //
  using verify_backend_selector = VlgVerifTgtGenBase::backend_selector;
  using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t;
  using synthesis_backend_selector =
      VlgVerifTgtGenBase::synthesis_backend_selector;
  typedef enum { NEXT_V, V_RES, NEXT_S, S_RES, DONE, FAILED } cegar_status;
  using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t;
  enum _inv_check_res_t { INV_PROVED, INV_INVALID, INV_UNKNOWN };
  typedef std::map<std::string, int> additional_width_info_t;

public:
  // -------------------- CONSTRUCTOR ------------------ //
  InvariantSynthesizerCegar(
      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, verify_backend_selector vbackend,
      synthesis_backend_selector sbackend,
      const vtg_config_t& vtg_config = vtg_config_t(),
      const VerilogGenerator::VlgGenConfig& config =
          VerilogGenerator::VlgGenConfig());
  InvariantSynthesizerCegar(const InvariantSynthesizerCegar&) = delete;
  InvariantSynthesizerCegar&
  operator=(const InvariantSynthesizerCegar&) = delete;

public:
  // -------------------- HELPERs ------------------ //
  // to do things separately, you can provide the run function your self
  // or even do it step by step
  void GenerateVerificationTarget();
  void GenerateVerificationTarget(const std::vector<std::string>& invs);
  void GenerateInvariantVerificationTarget();
  void ExtractVerificationResult(bool autodet = true, bool pass = true,
                                 const std::string& res_file = "",
                                 const std::string& mod_inst_name = "");

  void GenerateTargetAndExtractSmt();
  unsigned QueryRtlStateWidth(const std::string& name) const;

  void CexGeneralizeRemoveStates(const std::vector<std::string>&);
  void GenerateSynthesisTarget();
  void ExtractSynthesisResult(bool autodet = true, bool reachable = true,
                              const std::string& res_file = "");
  void ExtractAbcSynthesisResultForEnhancement(InvariantInCnf& incremental_cnf,
                                               bool autodet = true,
                                               bool reachable = true);

  bool virtual RunVerifAuto(const std::string& script_selection,
                            const std::string& pid_fname = "",
                            bool run_test = false,
                            unsigned timeout = 0);
  bool virtual RunSynAuto(bool run_test = false);

  void AcceptAllCandidateInvariant();
  void PruneCandidateInvariant();
  void SupplyCandidateInvariant(const std::string& vlg);
  void ClearAllCandidateInvariants();

  // -------------------- GrainChc ------------------ //
  void ChangeGrainSyntax(const std::vector<std::string>& syn);
  bool WordLevelEnhancement(const InvariantInCnf& incremental_cnf,
                            bool run_test = false);
  const InvariantInCnf& GetCurrentCnfEnhance() const;
  void MergeCnf(const InvariantInCnf& incremental_cnf);
  void ExtractInvariantVarForEnhance(
      size_t inv_idx, InvariantInCnf& incremental_cnf, bool per_clause,
      const std::set<std::string>& vars_to_remove = {});

  // -------------------- ACCESSOR ------------------ //
  bool in_bad_state() const { return bad_state; }
  bool check_in_bad_state() const;
  void LoadDesignSmtInfo(const std::string& fn);
  const std::vector<std::string>& GetRunnableTargetScriptName() const;
  void LoadPrevStatisticsState(const std::string& fn);
  DesignStatistics GetDesignStatistics() const;
  const InvariantObject& GetInvariants() const;
  void RemoveInvariantsByIdx(size_t idx);
  const InvariantObject& GetCandidateInvariants() const;
  void LoadInvariantsFromFile(const std::string& fn);
  void LoadCandidateInvariantsFromFile(const std::string& fn);

protected:
  // -------------------- MEMBERS ------------------ //
  InvariantObject inv_obj;
  InvariantInCnf inv_cnf;
  InvariantObject inv_candidate;
  std::unique_ptr<CexExtractor> cex_extract;
  std::string vlg_mod_inst_name;
  cegar_status status;
  std::shared_ptr<smt::YosysSmtParser> design_smt_info;
  additional_width_info_t additional_width_info;
  bool bad_state;
  unsigned round_id;
  std::vector<std::string> runnable_script_name;
  bool verification_pass;
  std::string vcd_file_name;
  bool cex_reachable;
  std::string synthesis_result_fn;
  enum cur_inv_tp { NONE, GRAIN_CHC, CHC, CEGAR_ABC } current_inv_type;

  // --------------------------------------------------
  // for book-keeping purpose
  // --------------------------------------------------
  std::vector<std::string> implementation_incl_path;
  std::vector<std::string> implementation_srcs_path;
  std::string implementation_top_module_name;
  std::string refinement_variable_mapping_path;
  std::string refinement_condition_path;
  std::string _output_path;
  InstrLvlAbsPtr _host;
  verify_backend_selector v_backend;
  synthesis_backend_selector s_backend;
  vtg_config_t _vtg_config;
  VerilogGenerator::VlgGenConfig _vlg_config;

  // --------------------------------------------------
  // for statistics purpose
  // --------------------------------------------------
  double eqcheck_time;
  double inv_validate_time;
  double inv_proof_attempt_time;
  double inv_syn_time;
  double inv_enhance_time;
  std::vector<double> inv_syn_time_series;

public:
  long long total_grain_cand;

}; // class InvariantSynthesizerCegar

}; // namespace ilang

#endif // INVSYN_INTERFACE

#endif // ILANG_VTARGET_OUT_INV_SYN_CEGAR_H__