vtarget_gen_cosa.h

// ---Hongce Zhang

#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_COSA_H__
#define ILANG_VTARGET_OUT_VTARGET_GEN_COSA_H__

#include <ilang/vtarget-out/vlg_mod.h>
#include <ilang/vtarget-out/vtarget_gen_impl.h>

#include <iostream>
#include <string>
#include <vector>

#include <ilang/config.h>
#include <ilang/ila/instr_lvl_abs.h>

namespace ilang {

class VlgSglTgtGen_Cosa;

class Cosa_problem {
  friend class VlgSglTgtGen_Cosa;
  typedef std::vector<std::string> prop_t;
  typedef struct {
    // the name in [??]
    // std::string  problem_name;
    prop_t assertions;
  } problem_t;
  typedef std::map<std::string, problem_t> problemset_t;

protected:
  prop_t assumptions;
  problemset_t probitem;

}; // Cosa_problem

class VlgSglTgtGen_Cosa : public VlgSglTgtGen {
  using target_type_t = VlgSglTgtGen::target_type_t;
  using info_t = VerilogModifier::info_t;
  using fn_l_map_t = VerilogModifier::fn_l_map_t;
  using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VlgSglTgtGen_Cosa(
      const std::string& output_path, // will be a sub directory of the
                                      // output_path of its parent
      const InstrPtr& instr_ptr, // which could be an empty pointer, and it will
                                 // be used to verify invariants
      const InstrLvlAbsPtr& ila_ptr,
      const VerilogGenerator::VlgGenConfig& config, nlohmann::json& _rf_vmap,
      nlohmann::json& _rf_cond, VlgTgtSupplementaryInfo& _supplementary_info,
      VerilogInfo* _vlg_info_ptr, const std::string& vlg_mod_inst_name,
      const std::string& ila_mod_inst_name, const std::string& wrapper_name,
      const std::vector<std::string>& implementation_srcs,
      const std::vector<std::string>& include_dirs,
      const vtg_config_t& vtg_config, backend_selector backend,
      const target_type_t& target_tp, advanced_parameters_t* adv_ptr);

protected:
  Cosa_problem _problems;
  std::string cosa_prob_fname;

protected:
  virtual void add_a_direct_assumption(const std::string& aspt,
                                       const std::string& dspt) override;
  virtual void add_a_direct_assertion(const std::string& asst,
                                      const std::string& dspt) override;

  void virtual PreExportProcess() override {}
  virtual void Export_script(const std::string& script_name) override;
  virtual void
  Export_problem(const std::string& extra_name) override; // only for cosa
  virtual void Export_jg_tester_script(const std::string& extra_name);

  virtual void Export_mem(const std::string& mem_name) override;
  virtual void Export_modify_verilog() override;

public:
  virtual void do_not_instantiate(void) override{};

}; // class VlgVerifTgtGenCosa

}; // namespace ilang

#endif // ILANG_VTARGET_OUT_VTARGET_GEN_COSA_H__