2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
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.
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.
20 #ifdef YOSYS_ENABLE_VERIFIC
26 extern int verific_verbose
;
28 extern bool verific_import_pending
;
29 extern void verific_import(Design
*design
, std::string top
= std::string());
31 extern pool
<int> verific_sva_prims
;
33 struct VerificImporter
;
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
;
49 VerificClocking(VerificImporter
*importer
, Verific::Net
*net
, bool sva_at_only
= false);
50 RTLIL::Cell
*addDff(IdString name
, SigSpec sig_d
, SigSpec sig_q
, Const init_value
= Const());
51 RTLIL::Cell
*addAdff(IdString name
, RTLIL::SigSpec sig_arst
, SigSpec sig_d
, SigSpec sig_q
, Const arst_value
);
52 RTLIL::Cell
*addDffsr(IdString name
, RTLIL::SigSpec sig_set
, RTLIL::SigSpec sig_clr
, SigSpec sig_d
, SigSpec sig_q
);
54 bool property_matches_sequence(const VerificClocking
&seq
) const {
55 if (clock_net
!= seq
.clock_net
)
57 if (enable_net
!= seq
.enable_net
)
59 if (posedge
!= seq
.posedge
)
65 struct VerificImporter
67 RTLIL::Module
*module
;
68 Verific::Netlist
*netlist
;
70 std::map
<Verific::Net
*, RTLIL::SigBit
> net_map
;
71 std::map
<Verific::Net
*, Verific::Net
*> sva_posedge_map
;
72 pool
<Verific::Net
*, hash_ptr_ops
> any_all_nets
;
74 bool mode_gates
, mode_keep
, mode_nosva
, mode_names
, mode_verific
;
77 VerificImporter(bool mode_gates
, bool mode_keep
, bool mode_nosva
, bool mode_names
, bool mode_verific
, bool mode_autocover
);
79 RTLIL::SigBit
net_map_at(Verific::Net
*net
);
81 RTLIL::IdString
new_verific_id(Verific::DesignObj
*obj
);
82 void import_attributes(dict
<RTLIL::IdString
, RTLIL::Const
> &attributes
, Verific::DesignObj
*obj
);
84 RTLIL::SigSpec
operatorInput(Verific::Instance
*inst
);
85 RTLIL::SigSpec
operatorInput1(Verific::Instance
*inst
);
86 RTLIL::SigSpec
operatorInput2(Verific::Instance
*inst
);
87 RTLIL::SigSpec
operatorInport(Verific::Instance
*inst
, const char *portname
);
88 RTLIL::SigSpec
operatorOutput(Verific::Instance
*inst
, const pool
<Verific::Net
*, hash_ptr_ops
> *any_all_nets
= nullptr);
90 bool import_netlist_instance_gates(Verific::Instance
*inst
, RTLIL::IdString inst_name
);
91 bool import_netlist_instance_cells(Verific::Instance
*inst
, RTLIL::IdString inst_name
);
93 void merge_past_ffs_clock(pool
<RTLIL::Cell
*> &candidates
, SigBit clock
, bool clock_pol
);
94 void merge_past_ffs(pool
<RTLIL::Cell
*> &candidates
);
96 void import_netlist(RTLIL::Design
*design
, Verific::Netlist
*nl
, std::set
<Verific::Netlist
*> &nl_todo
);
99 void verific_import_sva_assert(VerificImporter
*importer
, Verific::Instance
*inst
);
100 void verific_import_sva_assume(VerificImporter
*importer
, Verific::Instance
*inst
);
101 void verific_import_sva_cover(VerificImporter
*importer
, Verific::Instance
*inst
);
102 void verific_import_sva_trigger(VerificImporter
*importer
, Verific::Instance
*inst
);
103 bool verific_is_sva_net(VerificImporter
*importer
, Verific::Net
*net
);
105 extern int verific_sva_fsm_limit
;