From bc5cc4e103bf59711c339719d6aabbc3d4b655a4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 12 Oct 2017 11:59:11 +0200 Subject: [PATCH 1/5] Add Verific fairness/liveness support --- frontends/verific/verific.cc | 43 +++++++++++++++++++++++++++--------- 1 file changed, 32 insertions(+), 11 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 1efba338b..e77931528 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1500,6 +1500,7 @@ struct VerificSvaImporter bool mode_assert = false; bool mode_assume = false; bool mode_cover = false; + bool eventually = false; Instance *net_to_ast_driver(Net *n) { @@ -1673,15 +1674,30 @@ struct VerificSvaImporter // parse disable_iff expression Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1(); - Instance *sequence_node = net_to_ast_driver(sequence_net); - if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { - disable_iff = importer->net_map_at(sequence_node->GetInput1()); - sequence_net = sequence_node->GetInput2(); - } else - if (sequence_node && sequence_node->Type() == PRIM_ABORT) { - disable_iff = importer->net_map_at(sequence_node->GetInput2()); - sequence_net = sequence_node->GetInput1(); + while (1) + { + Instance *sequence_node = net_to_ast_driver(sequence_net); + + if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { + eventually = true; + sequence_net = sequence_node->GetInput(); + continue; + } + + if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { + disable_iff = importer->net_map_at(sequence_node->GetInput1()); + sequence_net = sequence_node->GetInput2(); + continue; + } + + if (sequence_node && sequence_node->Type() == PRIM_ABORT) { + disable_iff = importer->net_map_at(sequence_node->GetInput2()); + sequence_net = sequence_node->GetInput1(); + continue; + } + + break; } // parse SVA sequence into trigger signal @@ -1694,9 +1710,14 @@ struct VerificSvaImporter RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); - if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en); - if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en); + if (eventually) { + if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en); + if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en); + } else { + if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en); + if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en); + if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en); + } } }; From 05068af88041d8fffbece6ec94f240c7ae3e4f54 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 13 Oct 2017 17:11:46 +0200 Subject: [PATCH 2/5] Update Verific README --- frontends/verific/README | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/frontends/verific/README b/frontends/verific/README index e747255db..b4c436a3a 100644 --- a/frontends/verific/README +++ b/frontends/verific/README @@ -33,6 +33,13 @@ make -j8 ./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top' +Verific Features that should be enabled in your Verific library +=============================================================== + +database/DBCompileFlags.h: + DB_PRESERVE_INITIAL_VALUE + + Testing Verific+Yosys+SymbiYosys for formal verification ======================================================== From e7a3c47cc793eaacff3b3bf0e996944f6963a7a8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 13 Oct 2017 20:12:51 +0200 Subject: [PATCH 3/5] Add "verific -vlog-incdir" and "verific -vlog-define" --- frontends/verific/verific.cc | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index e77931528..f8c1dcd0a 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1851,6 +1851,16 @@ struct VerificPass : public Pass { log("Load the specified VHDL files into Verific.\n"); log("\n"); log("\n"); + log(" verific -vlog-incdir ..\n"); + log("\n"); + log("Add Verilog include directories.\n"); + log("\n"); + log("\n"); + log(" verific -vlog-define [=]..\n"); + log("\n"); + log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n"); + log("\n"); + log("\n"); log(" verific -import [options] ..\n"); log("\n"); log("Elaborate the design for the specified top modules, import to Yosys and\n"); @@ -1909,6 +1919,8 @@ struct VerificPass : public Pass { Message::RegisterCallBackMsg(msg_func); RuntimeFlags::SetVar("db_allow_external_nets", 1); RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0); + veri_file::DefineCmdLineMacro("VERIFIC"); + veri_file::DefineCmdLineMacro("SYNTHESIS"); const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); @@ -1924,6 +1936,27 @@ struct VerificPass : public Pass { int argidx = 1; + if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") { + for (argidx++; argidx < GetSize(args); argidx++) + veri_file::AddIncludeDir(args[argidx].c_str()); + goto check_error; + } + + if (GetSize(args) > argidx && args[argidx] == "-vlog-define") { + for (argidx++; argidx < GetSize(args); argidx++) { + string name = args[argidx]; + size_t equal = name.find('='); + if (equal != std::string::npos) { + string value = name.substr(equal+1); + name = name.substr(0, equal); + veri_file::DefineCmdLineMacro(name.c_str(), value.c_str()); + } else { + veri_file::DefineCmdLineMacro(name.c_str()); + } + } + goto check_error; + } + if (GetSize(args) > argidx && args[argidx] == "-vlog95") { for (argidx++; argidx < GetSize(args); argidx++) if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95)) @@ -2139,6 +2172,8 @@ struct VerificPass : public Pass { nl_done.insert(nl); } + veri_file::Reset(); + vhdl_file::Reset(); Libset::Reset(); goto check_error; } From 1954c78ea7b6ddc732ac4dc9f02a0d0cbc104a64 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 13 Oct 2017 20:23:19 +0200 Subject: [PATCH 4/5] Add "verific -vlog-libdir" --- frontends/verific/verific.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index f8c1dcd0a..77594b8cf 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1856,6 +1856,12 @@ struct VerificPass : public Pass { log("Add Verilog include directories.\n"); log("\n"); log("\n"); + log(" verific -vlog-libdir ..\n"); + log("\n"); + log("Add Verilog library directories. Verific will search in this directories to\n"); + log("find undefined modules.\n"); + log("\n"); + log("\n"); log(" verific -vlog-define [=]..\n"); log("\n"); log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n"); @@ -1942,6 +1948,12 @@ struct VerificPass : public Pass { goto check_error; } + if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") { + for (argidx++; argidx < GetSize(args); argidx++) + veri_file::AddYDir(args[argidx].c_str()); + goto check_error; + } + if (GetSize(args) > argidx && args[argidx] == "-vlog-define") { for (argidx++; argidx < GetSize(args); argidx++) { string name = args[argidx]; From 716dbc92745aa8b41d85a60d50263433d5a79393 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 14 Oct 2017 11:57:04 +0200 Subject: [PATCH 5/5] Revert 90be0d8 as it causes endless loops for some designs --- passes/opt/opt_reduce.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/passes/opt/opt_reduce.cc b/passes/opt/opt_reduce.cc index 10bdf7221..eb9d02ad5 100644 --- a/passes/opt/opt_reduce.cc +++ b/passes/opt/opt_reduce.cc @@ -88,7 +88,6 @@ struct OptReduceWorker RTLIL::SigSpec new_sig_a(new_sig_a_bits); if (new_sig_a != sig_a || sig_a.size() != cell->getPort("\\A").size()) { - new_sig_a.sort_and_unify(); log(" New input vector for %s cell %s: %s\n", cell->type.c_str(), cell->name.c_str(), log_signal(new_sig_a)); did_something = true; total_count++;