aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile12
-rw-r--r--backends/smt2/smt2.cc18
-rw-r--r--frontends/verific/verific.cc7
-rw-r--r--frontends/verific/verific.h2
-rw-r--r--frontends/verific/verificsva.cc50
-rw-r--r--passes/hierarchy/hierarchy.cc22
6 files changed, 79 insertions, 32 deletions
diff --git a/Makefile b/Makefile
index af29ff414..0b8af9f8f 100644
--- a/Makefile
+++ b/Makefile
@@ -102,9 +102,9 @@ OBJS = kernel/version_$(GIT_REV).o
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
-ABCREV = 6e3c24b3308a
+ABCREV = a2d59be
ABCPULL = 1
-ABCURL ?= https://bitbucket.org/alanmi/abc
+ABCURL ?= https://github.com/berkeley-abc/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1
# set ABCEXTERNAL = <abc-command> to use an external ABC instance
@@ -442,14 +442,14 @@ yosys-config: misc/yosys-config.in
abc/abc-$(ABCREV)$(EXE):
$(P)
ifneq ($(ABCREV),default)
- $(Q) if ( cd abc 2> /dev/null && hg identify; ) | grep -q +; then \
+ $(Q) if ( cd abc 2> /dev/null && ! git diff-index --quiet HEAD; ); then \
echo 'REEBE: NOP pbagnvaf ybpny zbqvsvpngvbaf! Frg NOPERI=qrsnhyg va Lbflf Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \
fi
- $(Q) if test "`cd abc 2> /dev/null && hg identify | cut -f1 -d' '`" != "$(ABCREV)"; then \
+ $(Q) if test "`cd abc 2> /dev/null && git rev-parse --short HEAD`" != "$(ABCREV)"; then \
test $(ABCPULL) -ne 0 || { echo 'REEBE: NOP abg hc gb qngr naq NOPCHYY frg gb 0 va Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; exit 1; }; \
echo "Pulling ABC from $(ABCURL):"; set -x; \
- test -d abc || hg clone --insecure $(ABCURL) abc; \
- cd abc && $(MAKE) DEP= clean && hg pull --insecure && hg update -r $(ABCREV); \
+ test -d abc || git clone $(ABCURL) abc; \
+ cd abc && $(MAKE) DEP= clean && git fetch origin master && git checkout $(ABCREV); \
fi
endif
$(Q) rm -f abc/abc-[0-9a-f]*
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 47c993d05..2fb6d4da9 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -135,6 +135,24 @@ struct Smt2Worker
log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
+ if (cell->type.in("$mem") && conn.first.in("\\RD_CLK", "\\WR_CLK"))
+ {
+ SigSpec clk = sigmap(conn.second);
+ for (int i = 0; i < GetSize(clk); i++)
+ {
+ if (clk[i].wire == nullptr)
+ continue;
+
+ if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1)
+ continue;
+
+ if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\WR_CLK_POLARITY")[i] == State::S1)
+ clock_posedge.insert(clk[i]);
+ else
+ clock_negedge.insert(clk[i]);
+ }
+ }
+ else
if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C"))
{
bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 9f61d69a4..793e296f4 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1297,7 +1297,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
// ==================================================================
-VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
+VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
{
module = importer->module;
@@ -1320,6 +1320,11 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
body_net = body_inst->GetInput2();
}
}
+ else
+ {
+ if (sva_at_only)
+ return;
+ }
if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
{
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 877d79057..9e3e39695 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -42,7 +42,7 @@ struct VerificClocking {
bool posedge = true;
VerificClocking() { }
- VerificClocking(VerificImporter *importer, Verific::Net *net);
+ VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index c9c341516..1a1000b19 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1543,20 +1543,33 @@ struct VerificSvaImporter
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
- clocking = VerificClocking(importer, root->GetInput());
-
- if (clocking.body_net == nullptr)
- parser_error(stringf("Failed to parse SVA clocking"), root);
-
// parse SVA sequence into trigger signal
- Net *net = clocking.body_net;
- SigBit accept_bit = State::S0, reject_bit = State::S0;
+ clocking = VerificClocking(importer, root->GetInput(), true);
+ SigBit accept_bit = State::S0, reject_bit = State::S0;
- if (mode_assert || mode_assume) {
- parse_property(net, nullptr, &reject_bit);
- } else {
- parse_property(net, &accept_bit, nullptr);
+ if (clocking.body_net == nullptr)
+ {
+ if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr || clocking.cond_net != nullptr)
+ parser_error(stringf("Failed to parse SVA clocking"), root);
+
+ if (mode_assert || mode_assume) {
+ log_ping();
+ reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
+ } else {
+ log_ping();
+ accept_bit = parse_expression(root->GetInput());
+ }
+ }
+ else
+ {
+ if (mode_assert || mode_assume) {
+ log_ping();
+ parse_property(clocking.body_net, nullptr, &reject_bit);
+ } else {
+ log_ping();
+ parse_property(clocking.body_net, &accept_bit, nullptr);
+ }
}
if (mode_trigger)
@@ -1570,10 +1583,17 @@ struct VerificSvaImporter
// add final FF stage
- SigBit sig_a_q = module->addWire(NEW_ID);
- SigBit sig_en_q = module->addWire(NEW_ID);
- clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
- clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+ SigBit sig_a_q, sig_en_q;
+
+ if (clocking.body_net == nullptr) {
+ sig_a_q = sig_a;
+ sig_en_q = sig_en;
+ } else {
+ sig_a_q = module->addWire(NEW_ID);
+ sig_en_q = module->addWire(NEW_ID);
+ clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
+ clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+ }
// generate assert/assume/cover cell
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 898763c64..ba960faf4 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -173,16 +173,20 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
for (auto &dir : libdirs)
{
- filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".v";
- if (check_file_exists(filename)) {
- Frontend::frontend_call(design, NULL, filename, "verilog");
- goto loaded_module;
- }
+ static const vector<pair<string, string>> extensions_list =
+ {
+ {".v", "verilog"},
+ {".sv", "verilog -sv"},
+ {".il", "ilang"}
+ };
- filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".il";
- if (check_file_exists(filename)) {
- Frontend::frontend_call(design, NULL, filename, "ilang");
- goto loaded_module;
+ for (auto &ext : extensions_list)
+ {
+ filename = dir + "/" + RTLIL::unescape_id(cell->type) + ext.first;
+ if (check_file_exists(filename)) {
+ Frontend::frontend_call(design, NULL, filename, ext.second);
+ goto loaded_module;
+ }
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-19 02:07:13 +0000