vtarget_gen_impl.h

#ifndef ILANG_VTARGET_OUT_VTARGET_GEN_IMPL_H__
#define ILANG_VTARGET_OUT_VTARGET_GEN_IMPL_H__

#include <list>
#include <map>
#include <unordered_map>
#include <vector>

#include "nlohmann/json.hpp"
#include <ilang/config.h>
#include <ilang/ila/instr_lvl_abs.h>
#include <ilang/smt-inout/yosys_smt_parser.h>
#include <ilang/verilog-in/verilog_analysis_wrapper.h>
#include <ilang/verilog-out/verilog_gen.h>
#include <ilang/vtarget-out/directive.h>
#include <ilang/vtarget-out/supplementary_info.h>
#include <ilang/vtarget-out/var_extract.h>
#include <ilang/vtarget-out/vtarget_gen.h>

namespace ilang {

class VlgSglTgtGen {
public:
  // --------------------- TYPE DEFINITION ------------------------ //
  typedef enum { INVARIANTS, INSTRUCTIONS, INV_SYN_DESIGN_ONLY } target_type_t;
  typedef enum {
    NA = 0,
    READY_SIGNAL = 1,
    READY_BOUND = 2,
    BOTH = 3
  } ready_type_t;
  typedef std::map<std::string, unsigned> func_app_cnt_t;
  using backend_selector = VlgVerifTgtGenBase::backend_selector;
  using synthesis_backend_selector =
      VlgVerifTgtGenBase::synthesis_backend_selector;
  using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t;
  using ex_info_t = VlgVerifTgtGenBase::ex_info_t;
  using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VlgSglTgtGen(
      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>& implementation_include_path,
      const vtg_config_t& vtg_config, backend_selector backend,
      const target_type_t& target_tp, advanced_parameters_t* adv_ptr);

  virtual ~VlgSglTgtGen() {}

protected:
  // --------------------- MEMBERS ---------------------------- //
  // the following are used to store info presented
  const std::string _output_path;
  InstrPtr _instr_ptr; // could be nullptr
  InstrLvlAbsPtr _host; // should not be nullptr
  const std::string _vlg_mod_inst_name;
  const std::string _ila_mod_inst_name;

  VerilogGeneratorBase vlg_wrapper;
  VerilogGenerator vlg_ila;
  IntefaceDirectiveRecorder _idr;
  StateMappingDirectiveRecorder _sdr;
  // we don't know the module name, before analyzing the rfmap. so we cannot
  // initialize in the beginning
  VerilogInfo* vlg_info_ptr;
  VarExtractor _vext;
  nlohmann::json& rf_vmap;
  nlohmann::json& rf_cond;
  nlohmann::json empty_json;
  const VlgTgtSupplementaryInfo& supplementary_info;
  std::map<std::string, ex_info_t> _all_referred_vlg_names;
  target_type_t target_type;
  bool has_flush;
  ready_type_t ready_type;
  func_app_cnt_t func_cnt;
  unsigned max_bound;
  unsigned cnt_width;
  advanced_parameters_t* _advanced_param_ptr;
  const bool has_gussed_synthesized_invariant;
  const bool has_confirmed_synthesized_invariant;
  const bool has_rf_invariant;

private:
  unsigned mapping_counter;
  unsigned property_counter;

protected:
  // --------------------- HELPERS ---------------------------- //
  std::string new_mapping_id();
  std::string new_property_id();
  const ExprPtr IlaGetState(const std::string& sname) const;
  const ExprPtr IlaGetInput(const std::string& sname) const;
  std::pair<unsigned, unsigned>

  GetMemInfo(const std::string& ila_mem_name) const;
  bool TryFindIlaState(const std::string& sname);
  bool TryFindIlaInput(const std::string& sname);
  bool TryFindVlgState(const std::string& sname);
  ExprPtr TryFindIlaVarName(const std::string& sname);
  std::string ModifyCondExprAndRecordVlgName(const VarExtractor::token& t);
  static unsigned TypeMatched(const ExprPtr& ila_var,
                              const SignalInfoBase& vlg_var);
  static unsigned get_width(const ExprPtr& n);
  std::string ReplExpr(const std::string& expr, bool force_vlg_sts = false);
  std::string PerStateMap(const std::string& ila_state_name_or_equ,
                          const std::string& vlg_st_name);
  std::string GetStateVarMapExpr(const std::string& ila_state_name,
                                 nlohmann::json& m, bool is_assert = false);
  void handle_start_condition(nlohmann::json& dc);
  nlohmann::json& get_current_instruction_rf();

protected:
  // --------------- STEPS OF GENERATION ------------------------//
  void ConstructWrapper_add_ila_input();
  void ConstructWrapper_reset_setup();
  void ConstructWrapper_add_vlg_input_output();
  void ConstructWrapper_add_cycle_count_moniter();
  void ConstructWrapper_generate_header();
  void ConstructWrapper_add_varmap_assumptions();
  void ConstructWrapper_add_varmap_assertions();
  void ConstructWrapper_add_inv_assumption_or_assertion_target_invariant();
  void ConstructWrapper_add_inv_assumption_or_assertion_target_instruction();

  void ConstructWrapper_add_additional_mapping_control();
  void ConstructWrapper_add_rf_assumptions();
  void ConstructWrapper_add_condition_signals();
  void ConstructWrapper_register_extra_io_wire();
  void ConstructWrapper_add_module_instantiation();
  void ConstructWrapper_add_helper_memory();
  void ConstructWrapper_add_uf_constraints();
  void ConstructWrapper_add_post_value_holder();
  int ConstructWrapper_add_post_value_holder_handle_obj(
      nlohmann::json& pv_cond_val, const std::string& pv_name, int width,
      bool create_reg);
  void ConstructWrapper_add_vlg_monitor();

  // -------------------------------------------------------------------------
  void
  ConstructWrapper_add_inv_assumption_or_assertion_target_inv_syn_design_only();
  void ConstructWrapper_inv_syn_connect_mem();
  void ConstructWrapper_inv_syn_cond_signals();

protected:
  std::string ConstructWrapper_get_ila_module_inst();
  void add_inv_obj_as_assertion(InvariantObject* inv_obj);
  void add_inv_obj_as_assumption(InvariantObject* inv_obj);
  void add_rf_inv_as_assumption();
  void add_rf_inv_as_assertion();

protected:
  // ----------------------- MEMBERS for Export ------------------- //
  std::string top_mod_name;
  std::string top_file_name;
  std::string ila_file_name;
  std::vector<std::string> vlg_design_files; // mainly design file
  std::vector<std::string> vlg_include_files_path;
  vtg_config_t _vtg_config;
  const VerilogGenerator::VlgGenConfig& _vlg_cfg;
  backend_selector _backend;

public:
  void virtual ConstructWrapper();
  void virtual PreExportProcess() = 0;
  void virtual Export_wrapper(const std::string& wrapper_name);
  void virtual Export_ila_vlg(const std::string& ila_vlg_name);
  void virtual Export_script(const std::string& script_name) = 0;
  void virtual Export_problem(
      const std::string& extra_name) = 0; // only for cosa
  void virtual Export_mem(const std::string& mem_name) = 0;
  void virtual Export_modify_verilog() = 0;
  void virtual ExportAll(const std::string& wrapper_name,
                         const std::string& ila_vlg_name,
                         const std::string& script_name,
                         const std::string& extra_name,
                         const std::string& mem_name);

protected:
  // helper function to be implemented by COSA/JASPER
  virtual void add_a_direct_assumption(const std::string& aspt,
                                       const std::string& dspt) = 0;
  virtual void add_a_direct_assertion(const std::string& asst,
                                      const std::string& dspt) = 0;

  // helper function to be implemented by COSA, Yosys, invsyn, jasper is not
  virtual void add_an_assumption(const std::string& aspt,
                                 const std::string& dspt);
  virtual void add_an_assertion(const std::string& asst,
                                const std::string& dspt);

  virtual void add_wire_assign_assumption(const std::string& varname,
                                          const std::string& expression,
                                          const std::string& dspt);
  virtual void add_reg_cassign_assumption(const std::string& varname,
                                          const std::string& expression,
                                          int width, const std::string& cond,
                                          const std::string& dspt);

public:
  // Do not instantiate
  virtual void do_not_instantiate(void) = 0;

  // ----------------------- BAD STATE -------------------- //
public:
  bool in_bad_state(void) const { return _bad_state; }

protected:
  bool bad_state_return(void);

private:
  bool _bad_state;

}; // class VlgSglTgtGen

class VlgVerifTgtGen : public VlgVerifTgtGenBase {
  // --------------------- TYPE DEFINITIONS ---------------------------- //
  using backend_selector = VlgVerifTgtGenBase::backend_selector;
  using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t;
  using target_type_t = VlgSglTgtGen::target_type_t;
  using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t;
  using _chc_target_t = VlgVerifTgtGenBase::_chc_target_t;

public:
  // --------------------- CONSTRUCTOR ---------------------------- //
  VlgVerifTgtGen(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,
                 const VerilogGenerator::VlgGenConfig& config =
                     VerilogGenerator::VlgGenConfig(),
                 advanced_parameters_t* adv_ptr = NULL);

  VlgVerifTgtGen(const VlgVerifTgtGen&) = delete;
  VlgVerifTgtGen& operator=(const VlgVerifTgtGen&) = delete;

  // --------------------- DESTRUCTOR ---------------------------- //
  virtual ~VlgVerifTgtGen();

protected:
  // --------------------- MEMBERS ---------------------------- //
  const std::vector<std::string> _vlg_impl_include_path;
  const std::vector<std::string> _vlg_impl_srcs;
  const std::string _vlg_impl_top_name;
  const std::string _rf_var_map_name;
  const std::string _rf_cond_name;
  const std::string _output_path;
  const InstrLvlAbsPtr& _ila_ptr;
  std::string _vlg_mod_inst_name;
  std::string _ila_mod_inst_name;
  VerilogInfo* vlg_info_ptr;
  backend_selector _backend;
  VerilogGenerator::VlgGenConfig _cfg;
  vtg_config_t _vtg_config;
  advanced_parameters_t* _advanced_param_ptr;
  std::vector<std::string> runnable_script_name;

protected:
  nlohmann::json rf_vmap;
  nlohmann::json rf_cond;
  VlgTgtSupplementaryInfo supplementary_info;

public:
  // --------------------- METHODS ---------------------------- //
  // only set the info pointer within it and delete it afterwards
  void GenerateTargets(void);
  bool in_bad_state(void) const { return _bad_state; }
  std::string GetVlgModuleInstanceName() const { return _vlg_mod_inst_name; }

#ifdef INVSYN_INTERFACE
  void GenerateInvSynTargetsAbc(bool useGla, bool useCorr, bool useAiger);
  std::shared_ptr<smt::YosysSmtParser>
  GenerateInvSynTargets(synthesis_backend_selector s_backend);
  std::shared_ptr<smt::YosysSmtParser>
  GenerateInvSynEnhanceTargets(const InvariantInCnf& cnf);
  std::shared_ptr<smt::YosysSmtParser> GenerateSmtTargets();
#endif

  const std::vector<std::string>& GetRunnableScriptName() const;
  const VlgTgtSupplementaryInfo& GetSupplementaryInfo() const;

protected:
  // --------------------- METHODS ---------------------------- //

protected:
  bool bad_state_return(void);
  void load_json(const std::string& fname, nlohmann::json& j);
  void set_module_instantiation_name();

private:
  bool _bad_state;
  virtual void do_not_instantiate() override {}

}; // class VlgVerifTgtGen

}; // namespace ilang

#endif // ILANG_VTARGET_OUT_VTARGET_GEN_IMPL_H__