vtarget_gen_jasper.h

// ---Hongce Zhang

#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_JASPER_H__
#define ILANG_VTARGET_OUT_VTARGET_GEN_JASPER_H__

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

namespace ilang {

class VlgSglTgtGen_Jasper : public VlgSglTgtGen {
  using target_type_t = VlgSglTgtGen::target_type_t;
  using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VlgSglTgtGen_Jasper(
      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);

  void add_addition_clock_info(const std::string& expr);
  void add_addition_reset_info(const std::string& expr);

protected:
  std::vector<std::pair<std::string, std::string>> assumptions;
  std::vector<std::pair<std::string, std::string>> assertions;
  std::vector<std::string>
      additional_clock_expr; // we don't put the "clk" here, as by default it
                             // will be there
  std::vector<std::string> additional_reset_expr;
  std::string jg_script_name;
  std::string abs_mem_name;

protected:
  virtual void add_an_assumption(const std::string& aspt,
                                 const std::string& dspt) override;
  virtual void add_an_assertion(const std::string& asst,
                                const std::string& dspt) override;
  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;

  virtual void add_wire_assign_assumption(const std::string& varname,
                                          const std::string& expression,
                                          const std::string& dspt) override;
  virtual void add_reg_cassign_assumption(const std::string& varname,
                                          const std::string& expression,
                                          int width, const std::string& cond,
                                          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_mem(const std::string& mem_name) override;
  virtual void Export_modify_verilog() override;

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

}; // class VlgVerifTgtGenCosaJasper

}; // namespace ilang

#endif // ILANG_VTARGET_OUT_VTARGET_GEN_JASPER_H__