1 files changed, 79 insertions, 0 deletions
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
new file mode 100644
index 000000000..4f1cb5d0f
--- /dev/null
+++ b/frontends/verific/verific.h
@@ -0,0 +1,79 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#ifdef YOSYS_ENABLE_VERIFIC
+
+#include "DataBase.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+extern pool<int> verific_sva_prims;
+
+struct VerificImporter;
+
+struct VerificClockEdge {
+	Verific::Net *clock_net = nullptr;
+	SigBit clock_sig = State::Sx;
+	bool posedge = false;
+	VerificClockEdge(VerificImporter *importer, Verific::Instance *inst);
+};
+
+struct VerificImporter
+{
+	RTLIL::Module *module;
+	Verific::Netlist *netlist;
+
+	std::map<Verific::Net*, RTLIL::SigBit> net_map;
+	std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
+
+	bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
+
+	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose);
+
+	RTLIL::SigBit net_map_at(Verific::Net *net);
+
+	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, Verific::DesignObj *obj);
+
+	RTLIL::SigSpec operatorInput(Verific::Instance *inst);
+	RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
+	RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
+	RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
+	RTLIL::SigSpec operatorOutput(Verific::Instance *inst);
+
+	bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
+	bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name);
+
+	void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
+	void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
+
+	void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
+};
+
+
+void import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
+void import_sva_assume(VerificImporter *importer, Verific::Instance *inst);
+void import_sva_cover(VerificImporter *importer, Verific::Instance *inst);
+
+void svapp_assert(Verific::Instance *inst);
+void svapp_assume(Verific::Instance *inst);
+void svapp_cover(Verific::Instance *inst);
+
+YOSYS_NAMESPACE_END
+
+#endif