frontends/verific/verific.h

   1 /*
   2  *  yosys -- Yosys Open SYnthesis Suite
   3  *
   4  *  Copyright (C) 2012  Claire Xenia Wolf <claire@yosyshq.com>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #ifdef YOSYS_ENABLE_VERIFIC
  21
  22 #include "DataBase.h"
  23
  24 YOSYS_NAMESPACE_BEGIN
  25
  26 extern int verific_verbose;
  27
  28 extern bool verific_import_pending;
  29 extern void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top = std::string());
  30
  31 extern pool<int> verific_sva_prims;
  32
  33 struct VerificImporter;
  34
  35 struct VerificClocking {
  36         RTLIL::Module *module = nullptr;
  37         Verific::Net *clock_net = nullptr;
  38         Verific::Net *enable_net = nullptr;
  39         Verific::Net *disable_net = nullptr;
  40         Verific::Net *body_net = nullptr;
  41         Verific::Net *cond_net = nullptr;
  42         SigBit clock_sig = State::Sx;
  43         SigBit enable_sig = State::S1;
  44         SigBit disable_sig = State::S0;
  45         bool posedge = true;
  46         bool gclk = false;
  47         bool cond_pol = true;
  48
  49         VerificClocking() { }
  50         VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
  51         RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
  52         RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
  53         RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
  54         RTLIL::Cell *addAldff(IdString name, RTLIL::SigSpec sig_aload, RTLIL::SigSpec sig_adata, SigSpec sig_d, SigSpec sig_q);
  55
  56         bool property_matches_sequence(const VerificClocking &seq) const {
  57                 if (clock_net != seq.clock_net)
  58                         return false;
  59                 if (enable_net != seq.enable_net)
  60                         return false;
  61                 if (posedge != seq.posedge)
  62                         return false;
  63                 return true;
  64         }
  65 };
  66
  67 struct VerificImporter
  68 {
  69         RTLIL::Module *module;
  70         Verific::Netlist *netlist;
  71
  72         std::map<Verific::Net*, RTLIL::SigBit> net_map;
  73         std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
  74         pool<Verific::Net*, hash_ptr_ops> any_all_nets;
  75
  76         bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
  77         bool mode_autocover, mode_fullinit;
  78
  79         VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);
  80
  81         RTLIL::SigBit net_map_at(Verific::Net *net);
  82
  83         RTLIL::IdString new_verific_id(Verific::DesignObj *obj);
  84         void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, Verific::DesignObj *obj, Verific::Netlist  *nl = nullptr);
  85
  86         RTLIL::SigSpec operatorInput(Verific::Instance *inst);
  87         RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
  88         RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
  89         RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
  90         RTLIL::SigSpec operatorOutput(Verific::Instance *inst, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr);
  91
  92         bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
  93         bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name);
  94
  95         void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
  96         void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
  97
  98         void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::map<std::string,Verific::Netlist*> &nl_todo, bool norename = false);
  99 };
 100
 101 void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
 102 void verific_import_sva_assume(VerificImporter *importer, Verific::Instance *inst);
 103 void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst);
 104 void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
 105 bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net);
 106
 107 extern int verific_sva_fsm_limit;
 108
 109 YOSYS_NAMESPACE_END
 110
 111 #endif