From caa78388cd72d3473903357d52908cd5c84a37d8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 10 Oct 2017 11:59:32 +0200 Subject: Allow $past, $stable, $rose, $fell in $global_clock blocks --- frontends/ast/simplify.cc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index cd2120b8c..4baed3bfc 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -405,9 +405,13 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, current_always_clocked = false; if (type == AST_ALWAYS) - for (auto child : children) + for (auto child : children) { if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) current_always_clocked = true; + if (child->type == AST_EDGE && GetSize(child->children) == 1 && + child->children[0]->type == AST_IDENTIFIER && child->children[0]->str == "\\$global_clock") + current_always_clocked = true; + } } int backup_width_hint = width_hint; -- cgit v1.2.3 From bc80426d4579d4973feed80e804c59cc46a5368c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 10 Oct 2017 12:00:48 +0200 Subject: Remove some dead code --- frontends/ast/simplify.cc | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 4baed3bfc..74e7b4675 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1828,21 +1828,6 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } - if (str == "\\$rose" || str == "\\$fell") - { - if (GetSize(children) != 1) - log_error("System function %s got %d arguments, expected 1 at %s:%d.\n", - RTLIL::unescape_id(str).c_str(), int(children.size()), filename.c_str(), linenum); - - if (!current_always_clocked) - log_error("System function %s is only allowed in clocked blocks at %s:%d.\n", - RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum); - - newNode = new AstNode(AST_EQ, children.at(0)->clone(), clone()); - newNode->children.at(1)->str = "\\$past"; - goto apply_newNode; - } - // $anyconst and $anyseq are mapped in AstNode::genRTLIL() if (str == "\\$anyconst" || str == "\\$anyseq") { recursion_counter--; -- cgit v1.2.3 From 142f4ca03a65bd590e6d17be8fbcf3e6a793febe Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 10 Oct 2017 13:32:04 +0200 Subject: Add timing constraints to osu035 example --- examples/osu035/Makefile | 2 +- examples/osu035/example.constr | 2 ++ examples/osu035/example.ys | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) create mode 100644 examples/osu035/example.constr diff --git a/examples/osu035/Makefile b/examples/osu035/Makefile index 8d8e247e3..2bb8162b3 100644 --- a/examples/osu035/Makefile +++ b/examples/osu035/Makefile @@ -1,5 +1,5 @@ -example.edif: example.ys example.v osu035_stdcells.lib +example.edif: example.ys example.v example.constr osu035_stdcells.lib yosys -l example.yslog -q example.ys osu035_stdcells.lib: diff --git a/examples/osu035/example.constr b/examples/osu035/example.constr new file mode 100644 index 000000000..eb2c6e8d5 --- /dev/null +++ b/examples/osu035/example.constr @@ -0,0 +1,2 @@ +set_driving_cell INVX1 +set_load 0.015 diff --git a/examples/osu035/example.ys b/examples/osu035/example.ys index 040f776a6..6821ef426 100644 --- a/examples/osu035/example.ys +++ b/examples/osu035/example.ys @@ -4,7 +4,7 @@ read_liberty -lib osu035_stdcells.lib synth -top top dfflibmap -liberty osu035_stdcells.lib -abc -liberty osu035_stdcells.lib +abc -D 10000 -constr example.constr -liberty osu035_stdcells.lib opt_clean stat -liberty osu035_stdcells.lib -- cgit v1.2.3 From 7c57d8fbb44cdc466f4e384528109ada7e52b4c1 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 10 Oct 2017 13:32:58 +0200 Subject: Rewrite ABC output to include proper net names in timing report --- passes/techmap/abc.cc | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 3d943e682..be86f642a 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -111,6 +111,7 @@ bool recover_init; bool clk_polarity, en_polarity; RTLIL::SigSpec clk_sig, en_sig; +dict pi_map, po_map; int map_signal(RTLIL::SigBit bit, gate_type_t gate_type = G(NONE), int in1 = -1, int in2 = -1, int in3 = -1, int in4 = -1) { @@ -601,6 +602,14 @@ struct abc_output_filter void next_line(const std::string &line) { + int pi, po; + if (sscanf(line.c_str(), "Start-point = pi%d. End-point = po%d.", &pi, &po) == 2) { + log("ABC: Start-point = pi%d (%s). End-point = po%d (%s).\n", + pi, pi_map.count(pi) ? pi_map.at(pi).c_str() : "???", + po, po_map.count(po) ? po_map.at(po).c_str() : "???"); + return; + } + for (char ch : line) next_char(ch); } @@ -616,6 +625,8 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin signal_map.clear(); signal_list.clear(); + pi_map.clear(); + po_map.clear(); recover_init = false; if (clk_str != "$") @@ -768,7 +779,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin if (!si.is_port || si.type != G(NONE)) continue; fprintf(f, " n%d", si.id); - count_input++; + pi_map[count_input++] = log_signal(si.bit); } if (count_input == 0) fprintf(f, " dummy_input\n"); @@ -780,7 +791,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin if (!si.is_port || si.type == G(NONE)) continue; fprintf(f, " n%d", si.id); - count_output++; + po_map[count_output++] = log_signal(si.bit); } fprintf(f, "\n"); @@ -1392,6 +1403,8 @@ struct AbcPass : public Pass { signal_list.clear(); signal_map.clear(); signal_init.clear(); + pi_map.clear(); + po_map.clear(); #ifdef ABCEXTERNAL std::string exe_file = ABCEXTERNAL; @@ -1819,6 +1832,8 @@ struct AbcPass : public Pass { signal_list.clear(); signal_map.clear(); signal_init.clear(); + pi_map.clear(); + po_map.clear(); log_pop(); } -- cgit v1.2.3 From c10e96c9ec8c4e56935ba796af0fa3d1f22b2a71 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 10 Oct 2017 15:16:39 +0200 Subject: Start work on pre-processor for Verific SVA properties --- frontends/verific/verific.cc | 163 ++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 153 insertions(+), 10 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index ae39f7c9d..1efba338b 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -99,6 +99,9 @@ struct VerificImporter; void import_sva_assert(VerificImporter *importer, Instance *inst); void import_sva_assume(VerificImporter *importer, Instance *inst); void import_sva_cover(VerificImporter *importer, Instance *inst); +void svapp_assert(VerificImporter *importer, Instance *inst); +void svapp_assume(VerificImporter *importer, Instance *inst); +void svapp_cover(VerificImporter *importer, Instance *inst); struct VerificClockEdge { Net *clock_net; @@ -115,14 +118,14 @@ struct VerificImporter std::map net_map; std::map sva_posedge_map; - bool mode_gates, mode_keep, mode_nosva, mode_names, verbose; + bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; pool verific_sva_prims; pool verific_psl_prims; - VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool verbose) : - mode_gates(mode_gates), mode_keep(mode_keep), - mode_nosva(mode_nosva), mode_names(mode_names), verbose(verbose) + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) : + mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), + mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose) { // Copy&paste from Verific 3.16_484_32_170630 Netlist.h vector sva_prims { @@ -1246,6 +1249,18 @@ struct VerificImporter } } + if (!mode_nosvapp) + { + for (auto inst : sva_asserts) + svapp_assert(this, inst); + + for (auto inst : sva_assumes) + svapp_assume(this, inst); + + for (auto inst : sva_covers) + svapp_cover(this, inst); + } + if (!mode_nosva) { for (auto inst : sva_asserts) @@ -1351,6 +1366,124 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) } } +// ================================================================== + +struct VerificSvaPP +{ + VerificImporter *importer; + Module *module; + + Netlist *netlist; + Instance *root; + + bool mode_assert = false; + bool mode_assume = false; + bool mode_cover = false; + + Instance *net_to_ast_driver(Net *n) + { + if (n == nullptr) + return nullptr; + + if (n->IsMultipleDriven()) + return nullptr; + + Instance *inst = n->Driver(); + + if (inst == nullptr) + return nullptr; + + if (!importer->verific_sva_prims.count(inst->Type()) && + !importer->verific_psl_prims.count(inst->Type())) + return nullptr; + + if (inst->Type() == PRIM_SVA_PAST) + return nullptr; + + return inst; + } + + Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); } + Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); } + Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); } + Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); } + Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); } + + Net *impl_to_seq(Instance *inst) + { + if (inst == nullptr) + return nullptr; + + if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) { + Net *new_net = impl_to_seq(get_ast_input(inst)); + if (new_net) { + inst->Disconnect(inst->View()->GetInput()); + inst->Connect(inst->View()->GetInput(), new_net); + } + return nullptr; + } + + if (inst->Type() == PRIM_SVA_AT) { + Net *new_net = impl_to_seq(get_ast_input2(inst)); + if (new_net) { + inst->Disconnect(inst->View()->GetInput2()); + inst->Connect(inst->View()->GetInput2(), new_net); + } + return nullptr; + } + + if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + if (mode_cover) { + Net *new_in1 = impl_to_seq(get_ast_input1(inst)); + Net *new_in2 = impl_to_seq(get_ast_input2(inst)); + if (!new_in1) new_in1 = inst->GetInput1(); + if (!new_in2) new_in2 = inst->GetInput2(); + return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile()); + } + } + + return nullptr; + } + + void run() + { + module = importer->module; + netlist = root->Owner(); + + // impl_to_seq(root); + } +}; + +void svapp_assert(VerificImporter *importer, Instance *inst) +{ + VerificSvaPP worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assert = true; + worker.run(); +} + +void svapp_assume(VerificImporter *importer, Instance *inst) +{ + VerificSvaPP worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assume = true; + worker.run(); +} + +void svapp_cover(VerificImporter *importer, Instance *inst) +{ + VerificSvaPP worker; + worker.importer = importer; + worker.root = inst; + worker.mode_cover = true; + worker.run(); +} + +// ================================================================== + struct VerificSvaImporter { VerificImporter *importer; @@ -1594,6 +1727,8 @@ void import_sva_cover(VerificImporter *importer, Instance *inst) worker.run(); } +// ================================================================== + struct VerificExtNets { int portname_cnt = 0; @@ -1715,10 +1850,6 @@ struct VerificPass : public Pass { log(" -extnets\n"); log(" Resolve references to external nets by adding module ports as needed.\n"); log("\n"); - log(" -nosva\n"); - log(" Ignore SVA properties, do not infer checker logic. (This also disables\n"); - log(" PSL properties in -vhdpsl mode.)\n"); - log("\n"); log(" -v\n"); log(" Verbose log messages.\n"); log("\n"); @@ -1731,6 +1862,13 @@ struct VerificPass : public Pass { log(" This will also add all SVA related cells to the design parallel to\n"); log(" the checker logic inferred by it.\n"); log("\n"); + log(" -nosva\n"); + log(" Ignore SVA properties, do not infer checker logic. (This also disables\n"); + log(" PSL properties in -vhdpsl mode.)\n"); + log("\n"); + log(" -nosvapp\n"); + log(" Disable SVA properties pre-processing pass. This implies -nosva.\n"); + log("\n"); log(" -n\n"); log(" Keep all Verific names on instances and nets. By default only\n"); log(" user-declared names are preserved.\n"); @@ -1844,7 +1982,7 @@ struct VerificPass : public Pass { { std::set nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; - bool mode_nosva = false, mode_names = false; + bool mode_nosva = false, mode_nosvapp = false, mode_names = false; bool verbose = false, flatten = false, extnets = false; string dumpfile; @@ -1873,6 +2011,11 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } + if (args[argidx] == "-nosvapp") { + mode_nosva = true; + mode_nosvapp = true; + continue; + } if (args[argidx] == "-n") { mode_names = true; continue; @@ -1968,7 +2111,7 @@ struct VerificPass : public Pass { while (!nl_todo.empty()) { Netlist *nl = *nl_todo.begin(); if (nl_done.count(nl) == 0) { - VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names, verbose); + VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose); importer.import_netlist(design, nl, nl_todo); } nl_todo.erase(nl); -- cgit v1.2.3 From 2b03a73a460a2033f8944c7c85623cef11600024 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 11 Oct 2017 13:58:51 +0200 Subject: Update ABC to hg rev 6283c5d99b06 --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 393701019..69c47f6b7 100644 --- a/Makefile +++ b/Makefile @@ -99,7 +99,7 @@ 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 = 0fc1803a77c0 +ABCREV = 6283c5d99b06 ABCPULL = 1 ABCURL ?= https://bitbucket.org/alanmi/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 -- cgit v1.2.3 From bc5cc4e103bf59711c339719d6aabbc3d4b655a4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 12 Oct 2017 11:59:11 +0200 Subject: 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); + } } }; -- cgit v1.2.3 From 90be0d800b350da12689c7943800e18420149eaa Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Thu, 12 Oct 2017 13:05:10 +0300 Subject: Fix input vector for reduce cells. --- passes/opt/opt_reduce.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/passes/opt/opt_reduce.cc b/passes/opt/opt_reduce.cc index eb9d02ad5..10bdf7221 100644 --- a/passes/opt/opt_reduce.cc +++ b/passes/opt/opt_reduce.cc @@ -88,6 +88,7 @@ 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++; -- cgit v1.2.3 From 05068af88041d8fffbece6ec94f240c7ae3e4f54 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 13 Oct 2017 17:11:46 +0200 Subject: 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 ======================================================== -- cgit v1.2.3 From e7a3c47cc793eaacff3b3bf0e996944f6963a7a8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 13 Oct 2017 20:12:51 +0200 Subject: 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; } -- cgit v1.2.3 From 1954c78ea7b6ddc732ac4dc9f02a0d0cbc104a64 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 13 Oct 2017 20:23:19 +0200 Subject: 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]; -- cgit v1.2.3 From 716dbc92745aa8b41d85a60d50263433d5a79393 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 14 Oct 2017 11:57:04 +0200 Subject: 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++; -- cgit v1.2.3 From 19aa26152766df6c8d1c608554c40f88ed923d5f Mon Sep 17 00:00:00 2001 From: Tim 'mithro' Ansell Date: Thu, 19 Oct 2017 18:45:09 -0400 Subject: Adding COPYING file with license information. This allows GitHub and other tools to detect the license info. Providing a COPYING for LICENSE file is also pretty standard. --- COPYING | 13 +++++++++++++ README.md | 2 +- 2 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 COPYING diff --git a/COPYING b/COPYING new file mode 100644 index 000000000..a01b7b697 --- /dev/null +++ b/COPYING @@ -0,0 +1,13 @@ +Copyright (C) 2012 - 2017 Clifford Wolf + +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. diff --git a/README.md b/README.md index 514e32b35..92dc68a6a 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ ``` yosys -- Yosys Open SYnthesis Suite -Copyright (C) 2012 - 2016 Clifford Wolf +Copyright (C) 2012 - 2017 Clifford Wolf Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above -- cgit v1.2.3 From 0a31a0b3ae570007196c4b4dd6c16ba7de7f3ba9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 20 Oct 2017 13:14:04 +0200 Subject: Remove all PSL support code from verific.cc --- frontends/verific/verific.cc | 196 ++++--------------------------------------- 1 file changed, 17 insertions(+), 179 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 77594b8cf..54210f98a 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -104,9 +104,9 @@ void svapp_assume(VerificImporter *importer, Instance *inst); void svapp_cover(VerificImporter *importer, Instance *inst); struct VerificClockEdge { - Net *clock_net; - SigBit clock_sig; - bool posedge; + Net *clock_net = nullptr; + SigBit clock_sig = State::Sx; + bool posedge = false; VerificClockEdge(VerificImporter *importer, Instance *inst); }; @@ -121,7 +121,6 @@ struct VerificImporter bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; pool verific_sva_prims; - pool verific_psl_prims; VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) : mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), @@ -152,29 +151,6 @@ struct VerificImporter for (int p : sva_prims) verific_sva_prims.insert(p); - - // Copy&paste from Verific 3.16_484_32_170630 Netlist.h - vector psl_prims { - OPER_PSLPREV, OPER_PSLNEXTFUNC, PRIM_PSL_ASSERT, PRIM_PSL_ASSUME, - PRIM_PSL_ASSUME_GUARANTEE, PRIM_PSL_RESTRICT, PRIM_PSL_RESTRICT_GUARANTEE, - PRIM_PSL_COVER, PRIM_ENDPOINT, PRIM_ROSE, PRIM_FELL, PRIM_AT, PRIM_ATSTRONG, - PRIM_ABORT, PRIM_PSL_NOT, PRIM_PSL_AND, PRIM_PSL_OR, PRIM_IMPL, PRIM_EQUIV, - PRIM_PSL_X, PRIM_PSL_XSTRONG, PRIM_PSL_G, PRIM_PSL_F, PRIM_PSL_U, PRIM_PSL_W, - PRIM_NEXT, PRIM_NEXTSTRONG, PRIM_ALWAYS, PRIM_NEVER, PRIM_EVENTUALLY, - PRIM_UNTIL, PRIM_UNTIL_, PRIM_UNTILSTRONG, PRIM_UNTILSTRONG_, PRIM_BEFORE, - PRIM_BEFORE_, PRIM_BEFORESTRONG, PRIM_BEFORESTRONG_, PRIM_NEXT_A, - PRIM_NEXT_ASTRONG, PRIM_NEXT_E, PRIM_NEXT_ESTRONG, PRIM_NEXT_EVENT, - PRIM_NEXT_EVENTSTRONG, PRIM_NEXT_EVENT_A, PRIM_NEXT_EVENT_ASTRONG, - PRIM_NEXT_EVENT_E, PRIM_NEXT_EVENT_ESTRONG, PRIM_SEQ_IMPL, PRIM_OSUFFIX_IMPL, - PRIM_SUFFIX_IMPL, PRIM_OSUFFIX_IMPLSTRONG, PRIM_SUFFIX_IMPLSTRONG, PRIM_WITHIN, - PRIM_WITHIN_, PRIM_WITHINSTRONG, PRIM_WITHINSTRONG_, PRIM_WHILENOT, - PRIM_WHILENOT_, PRIM_WHILENOTSTRONG, PRIM_WHILENOTSTRONG_, PRIM_CONCAT, - PRIM_FUSION, PRIM_SEQ_AND_LEN, PRIM_SEQ_AND, PRIM_SEQ_OR, PRIM_CONS_REP, - PRIM_NONCONS_REP, PRIM_GOTO_REP - }; - - for (int p : psl_prims) - verific_psl_prims.insert(p); } RTLIL::SigBit net_map_at(Net *net) @@ -1126,20 +1102,20 @@ struct VerificImporter if (!mode_gates) { if (import_netlist_instance_cells(inst, inst_name)) continue; - if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type())) + if (inst->IsOperator() && !verific_sva_prims.count(inst->Type())) log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); } else { if (import_netlist_instance_gates(inst, inst_name)) continue; } - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_PSL_ASSERT) + if (inst->Type() == PRIM_SVA_ASSERT) sva_asserts.insert(inst); - if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_PSL_ASSUME) + if (inst->Type() == PRIM_SVA_ASSUME) sva_assumes.insert(inst); - if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_PSL_COVER) + if (inst->Type() == PRIM_SVA_COVER) sva_covers.insert(inst); if (inst->Type() == PRIM_SVA_PAST && !mode_nosva) @@ -1159,38 +1135,9 @@ struct VerificImporter continue; } - if (inst->Type() == OPER_PSLPREV && !mode_nosva) - { - Net *clock = inst->GetClock(); - - if (!clock->IsConstant()) - { - VerificClockEdge clock_edge(this, clock->Driver()); - - SigSpec sig_d, sig_q; - - for (int i = 0; i < int(inst->InputSize()); i++) { - sig_d.append(net_map_at(inst->GetInputBit(i))); - sig_q.append(net_map_at(inst->GetOutputBit(i))); - } - - if (verbose) - log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); - - RTLIL::Cell *ff = module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); - - if (inst->InputSize() == 1) - past_ffs.insert(ff); - - if (!mode_keep) - continue; - } - } - - if (!mode_keep && (verific_sva_prims.count(inst->Type()) || verific_psl_prims.count(inst->Type()))) { + if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (verbose) - log(" skipping SVA/PSL cell in non k-mode\n"); + log(" skipping SVA cell in non k-mode\n"); continue; } @@ -1202,7 +1149,7 @@ struct VerificImporter if (!mode_keep) log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); - if (!verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type())) + if (!verific_sva_prims.count(inst->Type())) log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); } @@ -1277,36 +1224,6 @@ struct VerificImporter } }; -Net *verific_follow_inv(Net *w) -{ - if (w == nullptr || w->IsMultipleDriven()) - return nullptr; - - Instance *i = w->Driver(); - if (i == nullptr || i->Type() != PRIM_INV) - return nullptr; - - return i->GetInput(); -} - -Net *verific_follow_pslprev(Net *w) -{ - if (w == nullptr || w->IsMultipleDriven()) - return nullptr; - - Instance *i = w->Driver(); - if (i == nullptr || i->Type() != OPER_PSLPREV || i->InputSize() != 1) - return nullptr; - - return i->GetInputBit(0); -} - -Net *verific_follow_inv_pslprev(Net *w) -{ - w = verific_follow_inv(w); - return verific_follow_pslprev(w); -} - VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) { log_assert(importer != nullptr); @@ -1327,43 +1244,6 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) clock_sig = importer->net_map_at(clock_net); return; } - - // VHDL-flavored PSL clock - if (inst->Type() == PRIM_AND) - { - Net *w1 = inst->GetInput1(); - Net *w2 = inst->GetInput2(); - - clock_net = verific_follow_inv_pslprev(w1); - if (clock_net == w2) { - clock_sig = importer->net_map_at(clock_net); - posedge = true; - return; - } - - clock_net = verific_follow_inv_pslprev(w2); - if (clock_net == w1) { - clock_sig = importer->net_map_at(clock_net); - posedge = true; - return; - } - - clock_net = verific_follow_pslprev(w1); - if (clock_net == verific_follow_inv(w2)) { - clock_sig = importer->net_map_at(clock_net); - posedge = false; - return; - } - - clock_net = verific_follow_pslprev(w2); - if (clock_net == verific_follow_inv(w1)) { - clock_sig = importer->net_map_at(clock_net); - posedge = false; - return; - } - - log_abort(); - } } // ================================================================== @@ -1393,8 +1273,7 @@ struct VerificSvaPP if (inst == nullptr) return nullptr; - if (!importer->verific_sva_prims.count(inst->Type()) && - !importer->verific_psl_prims.count(inst->Type())) + if (!importer->verific_sva_prims.count(inst->Type())) return nullptr; if (inst->Type() == PRIM_SVA_PAST) @@ -1515,8 +1394,7 @@ struct VerificSvaImporter if (inst == nullptr) return nullptr; - if (!importer->verific_sva_prims.count(inst->Type()) && - !importer->verific_psl_prims.count(inst->Type())) + if (!importer->verific_sva_prims.count(inst->Type())) return nullptr; if (inst->Type() == PRIM_SVA_PAST) @@ -1625,31 +1503,6 @@ struct VerificSvaImporter return; } - // PSL Primitives - - if (inst->Type() == PRIM_ALWAYS) - { - parse_sequence(seq, inst->GetInput()); - return; - } - - if (inst->Type() == PRIM_IMPL) - { - parse_sequence(seq, inst->GetInput1()); - seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a); - parse_sequence(seq, inst->GetInput2()); - return; - } - - if (inst->Type() == PRIM_SUFFIX_IMPL) - { - parse_sequence(seq, inst->GetInput1()); - seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a); - sequence_ff(seq); - parse_sequence(seq, inst->GetInput2()); - return; - } - // Handle unsupported primitives if (!importer->mode_keep) @@ -1665,15 +1518,15 @@ struct VerificSvaImporter // parse SVA property clock event Instance *at_node = get_ast_input(root); - log_assert(at_node && (at_node->Type() == PRIM_SVA_AT || at_node->Type() == PRIM_AT)); + log_assert(at_node && at_node->Type() == PRIM_SVA_AT); - VerificClockEdge clock_edge(importer, at_node->Type() == PRIM_SVA_AT ? get_ast_input1(at_node) : at_node->GetInput2()->Driver()); + VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); clock = clock_edge.clock_sig; clock_posedge = clock_edge.posedge; // parse disable_iff expression - Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1(); + Net *sequence_net = at_node->GetInput2(); while (1) { @@ -1691,12 +1544,6 @@ struct VerificSvaImporter 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; } @@ -1846,7 +1693,7 @@ struct VerificPass : public Pass { log("Load the specified Verilog/SystemVerilog files into Verific.\n"); log("\n"); log("\n"); - log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl|-vhdpsl} ..\n"); + log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} ..\n"); log("\n"); log("Load the specified VHDL files into Verific.\n"); log("\n"); @@ -1900,8 +1747,7 @@ struct VerificPass : public Pass { log(" the checker logic inferred by it.\n"); log("\n"); log(" -nosva\n"); - log(" Ignore SVA properties, do not infer checker logic. (This also disables\n"); - log(" PSL properties in -vhdpsl mode.)\n"); + log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); log(" -nosvapp\n"); log(" Disable SVA properties pre-processing pass. This implies -nosva.\n"); @@ -2036,14 +1882,6 @@ struct VerificPass : public Pass { goto check_error; } - if (GetSize(args) > argidx && args[argidx] == "-vhdpsl") { - vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL)) - log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str()); - goto check_error; - } - if (GetSize(args) > argidx && args[argidx] == "-import") { std::set nl_todo, nl_done; -- cgit v1.2.3 From baddb017fe5eb72fbb65d6f89553dc2341663613 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 20 Oct 2017 13:16:24 +0200 Subject: Remove PSL example from tests/sva/ --- tests/sva/runtest.sh | 2 +- tests/sva/vhdlpsl00.vhd | 34 ---------------------------------- 2 files changed, 1 insertion(+), 35 deletions(-) delete mode 100644 tests/sva/vhdlpsl00.vhd diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 35c95a3e0..4c8e16542 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -29,7 +29,7 @@ generate_sby() { fi if [ -f $prefix.vhd ]; then - echo "verific -vhdpsl $prefix.vhd" + echo "verific -vhdl $prefix.vhd" fi cat <<- EOT diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd deleted file mode 100644 index 6d765d5a9..000000000 --- a/tests/sva/vhdlpsl00.vhd +++ /dev/null @@ -1,34 +0,0 @@ -library ieee; -use ieee.std_logic_1164.all; -use ieee.std_logic_unsigned.all; -use ieee.numeric_std.all; - -entity top is - port ( - clk : in std_logic; - rst : in std_logic; - up : in std_logic; - down : in std_logic; - cnt : buffer std_logic_vector(7 downto 0) - ); -end entity; - -architecture rtl of top is -begin - process (clk) begin - if rising_edge(clk) then - if rst = '1' then - cnt <= std_logic_vector(to_unsigned(0, 8)); - elsif up = '1' then - cnt <= cnt + std_logic_vector(to_unsigned(1, 8)); - elsif down = '1' then - cnt <= cnt - std_logic_vector(to_unsigned(1, 8)); - end if; - end if; - end process; - - -- PSL default clock is (rising_edge(clk)); - -- PSL assume always ( down -> not up ); - -- PSL assert always ( up |=> (cnt = prev(cnt) + std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1'; - -- PSL assert always ( down |=> (cnt = prev(cnt) - std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1'; -end architecture; -- cgit v1.2.3 From dd46d76394eb3f345d8af63ade4fd2b4f2e443e1 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 13:05:14 +0200 Subject: Fix a bug in yosys-smtbmc in ROM handling --- backends/smt2/smtbmc.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index c8151c266..d9b79e26e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -644,6 +644,9 @@ def write_vcd_trace(steps_start, steps_stop, index): data = ["x"] * width gotread = False + if len(wdata) == 0 and len(rdata) != 0: + wdata = [[]] * len(rdata) + assert len(rdata) == len(wdata) for i in range(len(wdata)): -- cgit v1.2.3 From c672c321e3cca1803e5f1108d3438e9e18800635 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 13:37:11 +0200 Subject: Capsulate smt-solver read/write in separate functions --- backends/smt2/smtio.py | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index abf8e812d..7cd7d0d59 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -58,6 +58,7 @@ class SmtIo: self.produce_models = True self.smt2cache = [list()] self.p = None + self.p_buffer = [] if opts is not None: self.logic = opts.logic @@ -209,6 +210,19 @@ class SmtIo: return stmt + def p_write(self, data): + # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1): + wlen = self.p.stdin.write(data) + assert wlen == len(data) + + def p_flush(self): + self.p.stdin.flush() + + def p_read(self): + if len(self.p_buffer) == 0: + return self.p.stdout.readline().decode("ascii") + assert 0 + def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) @@ -283,18 +297,19 @@ class SmtIo: if self.p is not None and not stmt.startswith("(get-"): self.p.stdin.close() self.p = None + self.p_buffer = [] if stmt == "(push 1)": self.smt2cache.append(list()) elif stmt == "(pop 1)": self.smt2cache.pop() else: if self.p is not None: - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + self.p_write(bytes(stmt + "\n", "ascii")) + self.p_flush() self.smt2cache[-1].append(stmt) else: - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + self.p_write(bytes(stmt + "\n", "ascii")) + self.p_flush() def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -408,7 +423,7 @@ class SmtIo: if self.solver == "dummy": line = self.dummy_fd.readline().strip() else: - line = self.p.stdout.readline().decode("ascii").strip() + line = self.p_read().strip() if self.dummy_file is not None: self.dummy_fd.write(line + "\n") @@ -443,13 +458,14 @@ class SmtIo: if self.p is not None: self.p.stdin.close() self.p = None + self.p_buffer = [] self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) for cache_ctx in self.smt2cache: for cache_stmt in cache_ctx: - self.p.stdin.write(bytes(cache_stmt + "\n", "ascii")) + self.p_write(bytes(cache_stmt + "\n", "ascii")) - self.p.stdin.write(bytes("(check-sat)\n", "ascii")) - self.p.stdin.flush() + self.p_write(bytes("(check-sat)\n", "ascii")) + self.p_flush() if self.timeinfo: i = 0 -- cgit v1.2.3 From a8cf431d9c1bd1c25a98e10ff45fad94f3e3a333 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 14:50:22 +0200 Subject: Remove vhdl2verilog --- frontends/vhdl2verilog/Makefile.inc | 1 - frontends/vhdl2verilog/vhdl2verilog.cc | 183 --------------------------------- 2 files changed, 184 deletions(-) delete mode 100644 frontends/vhdl2verilog/Makefile.inc delete mode 100644 frontends/vhdl2verilog/vhdl2verilog.cc diff --git a/frontends/vhdl2verilog/Makefile.inc b/frontends/vhdl2verilog/Makefile.inc deleted file mode 100644 index 003d89c4a..000000000 --- a/frontends/vhdl2verilog/Makefile.inc +++ /dev/null @@ -1 +0,0 @@ -OBJS += frontends/vhdl2verilog/vhdl2verilog.o diff --git a/frontends/vhdl2verilog/vhdl2verilog.cc b/frontends/vhdl2verilog/vhdl2verilog.cc deleted file mode 100644 index 6f9c0e3f5..000000000 --- a/frontends/vhdl2verilog/vhdl2verilog.cc +++ /dev/null @@ -1,183 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2012 Clifford Wolf - * - * 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. - * - */ - -#include "kernel/register.h" -#include "kernel/sigtools.h" -#include "kernel/log.h" -#include -#include -#include -#include -#include - -#ifndef _WIN32 -# include -# include -#endif - -YOSYS_NAMESPACE_BEGIN - -struct Vhdl2verilogPass : public Pass { - Vhdl2verilogPass() : Pass("vhdl2verilog", "importing VHDL designs using vhdl2verilog") { } - virtual void help() - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" vhdl2verilog [options] ..\n"); - log("\n"); - log("This command reads VHDL source files using the 'vhdl2verilog' tool and the\n"); - log("Yosys Verilog frontend.\n"); - log("\n"); - log(" -out \n"); - log(" do not import the vhdl2verilog output. instead write it to the\n"); - log(" specified file.\n"); - log("\n"); - log(" -vhdl2verilog_dir \n"); - log(" do use the specified vhdl2verilog installation. this is the directory\n"); - log(" that contains the setup_env.sh file. when this option is not present,\n"); - log(" it is assumed that vhdl2verilog is in the PATH environment variable.\n"); - log("\n"); - log(" -top \n"); - log(" The name of the top entity. This option is mandatory.\n"); - log("\n"); - log("The following options are passed as-is to vhdl2verilog:\n"); - log("\n"); - log(" -arch \n"); - log(" -unroll_generate\n"); - log(" -nogenericeval\n"); - log(" -nouniquify\n"); - log(" -oldparser\n"); - log(" -suppress \n"); - log(" -quiet\n"); - log(" -nobanner\n"); - log(" -mapfile \n"); - log("\n"); - log("vhdl2verilog can be obtained from:\n"); - log("http://www.edautils.com/vhdl2verilog.html\n"); - log("\n"); - } - virtual void execute(std::vector args, RTLIL::Design *design) - { - log_header(design, "Executing VHDL2VERILOG (importing VHDL designs using vhdl2verilog).\n"); - log_push(); - - std::string out_file, top_entity; - std::string vhdl2verilog_dir; - std::string extra_opts; - - size_t argidx; - for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-out" && argidx+1 < args.size()) { - out_file = args[++argidx]; - continue; - } - if (args[argidx] == "-top" && argidx+1 < args.size()) { - top_entity = args[++argidx]; - continue; - } - if (args[argidx] == "-vhdl2verilog_dir" && argidx+1 < args.size()) { - vhdl2verilog_dir = args[++argidx]; - continue; - } - if ((args[argidx] == "-arch" || args[argidx] == "-suppress" || args[argidx] == "-mapfile") && argidx+1 < args.size()) { - if (args[argidx] == "-mapfile" && !args[argidx+1].empty() && args[argidx+1][0] != '/') { - char pwd[PATH_MAX]; - if (!getcwd(pwd, sizeof(pwd))) { - log_cmd_error("getcwd failed: %s", strerror(errno)); - log_abort(); - } - args[argidx+1] = pwd + ("/" + args[argidx+1]); - } - extra_opts += std::string(" ") + args[argidx]; - extra_opts += std::string(" '") + args[++argidx] + std::string("'"); - continue; - } - if (args[argidx] == "-unroll_generate" || args[argidx] == "-nogenericeval" || args[argidx] == "-nouniquify" || - args[argidx] == "-oldparser" || args[argidx] == "-quiet" || args[argidx] == "-nobanner") { - extra_opts += std::string(" ") + args[argidx]; - continue; - } - break; - } - - if (argidx == args.size()) - cmd_error(args, argidx, "Missing filenames."); - if (args[argidx].substr(0, 1) == "-") - cmd_error(args, argidx, "Unknown option."); - if (top_entity.empty()) - log_cmd_error("Missing -top option.\n"); - - std::string tempdir_name = make_temp_dir("/tmp/yosys-vhdl2verilog-XXXXXX"); - log("Using temp directory %s.\n", tempdir_name.c_str()); - - if (!out_file.empty() && out_file[0] != '/') { - char pwd[PATH_MAX]; - if (!getcwd(pwd, sizeof(pwd))) { - log_cmd_error("getcwd failed: %s", strerror(errno)); - log_abort(); - } - out_file = pwd + ("/" + out_file); - } - - FILE *f = fopen(stringf("%s/files.list", tempdir_name.c_str()).c_str(), "wt"); - while (argidx < args.size()) { - std::string file = args[argidx++]; - if (file.empty()) - continue; - if (file[0] != '/') { - char pwd[PATH_MAX]; - if (!getcwd(pwd, sizeof(pwd))) { - log_cmd_error("getcwd failed: %s", strerror(errno)); - log_abort(); - } - file = pwd + ("/" + file); - } - fprintf(f, "%s\n", file.c_str()); - log("Adding '%s' to the file list.\n", file.c_str()); - } - fclose(f); - - std::string command = "exec 2>&1; "; - if (!vhdl2verilog_dir.empty()) - command += stringf("cd '%s'; . ./setup_env.sh; ", vhdl2verilog_dir.c_str()); - command += stringf("cd '%s'; vhdl2verilog -out '%s' -filelist files.list -top '%s'%s", tempdir_name.c_str(), - out_file.empty() ? "vhdl2verilog_output.v" : out_file.c_str(), top_entity.c_str(), extra_opts.c_str()); - - log("Running '%s'..\n", command.c_str()); - - int ret = run_command(command, [](const std::string &line) { log("%s", line.c_str()); }); - if (ret != 0) - log_error("Execution of command \"%s\" failed: return code %d.\n", command.c_str(), ret); - - if (out_file.empty()) { - std::ifstream ff; - ff.open(stringf("%s/vhdl2verilog_output.v", tempdir_name.c_str()).c_str()); - if (ff.fail()) - log_error("Can't open vhdl2verilog output file `vhdl2verilog_output.v'.\n"); - Frontend::frontend_call(design, &ff, stringf("%s/vhdl2verilog_output.v", tempdir_name.c_str()), "verilog"); - } - - log_header(design, "Removing temp directory `%s':\n", tempdir_name.c_str()); - remove_directory(tempdir_name); - log_pop(); - } -} Vhdl2verilogPass; - -YOSYS_NAMESPACE_END - -- cgit v1.2.3 From af36755e0a48cb02a14825125b78da66d50861a4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 14:51:59 +0200 Subject: Update ABC to hg rev f6838749f234 --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 69c47f6b7..54e03eb78 100644 --- a/Makefile +++ b/Makefile @@ -99,7 +99,7 @@ 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 = 6283c5d99b06 +ABCREV = f6838749f234 ABCPULL = 1 ABCURL ?= https://bitbucket.org/alanmi/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 -- cgit v1.2.3 From 9a038861c882d628cf9bb1d9c3e8ce0525f6c49a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 14:57:16 +0200 Subject: Add ENABLE_DEBUG config flag --- Makefile | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 54e03eb78..eb8f0f594 100644 --- a/Makefile +++ b/Makefile @@ -17,6 +17,7 @@ ENABLE_LIBYOSYS := 0 # other configuration flags ENABLE_GPROF := 0 +ENABLE_DEBUG := 0 ENABLE_NDEBUG := 0 LINK_CURSES := 0 LINK_TERMCAP := 0 @@ -251,7 +252,15 @@ LDFLAGS += -pg endif ifeq ($(ENABLE_NDEBUG),1) -CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os,$(CXXFLAGS)) +CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os -ggdb,$(CXXFLAGS)) +endif + +ifeq ($(ENABLE_DEBUG),1) +ifeq ($(CONFIG),clang) +CXXFLAGS := -O0 $(filter-out -Os,$(CXXFLAGS)) +else +CXXFLAGS := -Og $(filter-out -Os,$(CXXFLAGS)) +endif endif ifeq ($(ENABLE_ABC),1) -- cgit v1.2.3 From 104b9dc96bc0e8fa8a62177e1fd4b276f0a021d1 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 15:17:29 +0200 Subject: Disable OSX in .travis.yml --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index d8cd5b298..1c08c21a8 100644 --- a/.travis.yml +++ b/.travis.yml @@ -29,8 +29,8 @@ before_install: - (cd iverilog && autoconf && ./configure --prefix=$HOME/iverilog && make && make install) - export PATH=$PATH:$HOME/iverilog/bin compiler: -# - clang +# - clang - gcc os: - linux - - osx +# - osx -- cgit v1.2.3 From 76326c163a6698ab33059ca5fcf34b5e46bb8538 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 15:45:32 +0200 Subject: Improve p_* functions in smtio.py --- backends/smt2/smtio.py | 40 +++++++++++++++++++--------------------- 1 file changed, 19 insertions(+), 21 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 7cd7d0d59..18dee4e95 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -127,7 +127,7 @@ class SmtIo: if self.dummy_file is not None: self.dummy_fd = open(self.dummy_file, "w") if not self.noincr: - self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_open() if self.unroll: self.logic_uf = False @@ -210,19 +210,24 @@ class SmtIo: return stmt - def p_write(self, data): - # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1): - wlen = self.p.stdin.write(data) - assert wlen == len(data) + def p_open(self): + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - def p_flush(self): - self.p.stdin.flush() + def p_write(self, data, flush): + self.p.stdin.write(bytes(data, "ascii")) + if flush: + self.p.stdin.flush() def p_read(self): if len(self.p_buffer) == 0: return self.p.stdout.readline().decode("ascii") assert 0 + def p_close(self): + self.p.stdin.close() + self.p = None + self.p_buffer = [] + def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) @@ -295,21 +300,17 @@ class SmtIo: if self.solver != "dummy": if self.noincr: if self.p is not None and not stmt.startswith("(get-"): - self.p.stdin.close() - self.p = None - self.p_buffer = [] + self.p_close() if stmt == "(push 1)": self.smt2cache.append(list()) elif stmt == "(pop 1)": self.smt2cache.pop() else: if self.p is not None: - self.p_write(bytes(stmt + "\n", "ascii")) - self.p_flush() + self.p_write(stmt + "\n", True) self.smt2cache[-1].append(stmt) else: - self.p_write(bytes(stmt + "\n", "ascii")) - self.p_flush() + self.p_write(stmt + "\n", True) def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -456,16 +457,13 @@ class SmtIo: if self.solver != "dummy": if self.noincr: if self.p is not None: - self.p.stdin.close() - self.p = None - self.p_buffer = [] - self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_close() + self.p_open() for cache_ctx in self.smt2cache: for cache_stmt in cache_ctx: - self.p_write(bytes(cache_stmt + "\n", "ascii")) + self.p_write(cache_stmt + "\n", False) - self.p_write(bytes("(check-sat)\n", "ascii")) - self.p_flush() + self.p_write("(check-sat)\n", True) if self.timeinfo: i = 0 -- cgit v1.2.3 From f513494f5fabd2596b1748cf67dcaf70723b28f7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 19:59:56 +0200 Subject: Use separate writer thread for talking to SMT solver to avoid read/write deadlock --- backends/smt2/smtio.py | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 18dee4e95..6e7b68242 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -20,6 +20,8 @@ import sys, subprocess, re, os from copy import deepcopy from select import select from time import time +from queue import Queue +from threading import Thread hex_dict = { @@ -58,7 +60,6 @@ class SmtIo: self.produce_models = True self.smt2cache = [list()] self.p = None - self.p_buffer = [] if opts is not None: self.logic = opts.logic @@ -210,23 +211,36 @@ class SmtIo: return stmt + def p_thread_main(self): + while True: + data = self.p_queue.get() + if data is None: break + self.p.stdin.write(data[0]) + if data[1]: self.p.stdin.flush() + def p_open(self): + assert self.p is None self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_queue = Queue() + self.p_thread = Thread(target=self.p_thread_main) + self.p_thread.start() def p_write(self, data, flush): - self.p.stdin.write(bytes(data, "ascii")) - if flush: - self.p.stdin.flush() + assert self.p is not None + self.p_queue.put((bytes(data, "ascii"), flush)) def p_read(self): - if len(self.p_buffer) == 0: - return self.p.stdout.readline().decode("ascii") - assert 0 + assert self.p is not None + return self.p.stdout.readline().decode("ascii") def p_close(self): + assert self.p is not None + self.p_queue.put(None) + self.p_thread.join() self.p.stdin.close() self.p = None - self.p_buffer = [] + self.p_queue = None + self.p_thread = None def write(self, stmt, unroll=True): if stmt.startswith(";"): @@ -686,6 +700,7 @@ class SmtIo: def wait(self): if self.p is not None: self.p.wait() + self.p_close() class SmtOpts: -- cgit v1.2.3 From 11705082648143c8be1a8b8fd4ef60ee81451c01 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 26 Oct 2017 01:01:55 +0200 Subject: Improve smtio performance by using reader thread, not writer thread --- backends/smt2/smtio.py | 40 ++++++++++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 10 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 6e7b68242..61ac14c82 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -20,7 +20,7 @@ import sys, subprocess, re, os from copy import deepcopy from select import select from time import time -from queue import Queue +from queue import Queue, Empty from threading import Thread @@ -213,32 +213,52 @@ class SmtIo: def p_thread_main(self): while True: - data = self.p_queue.get() - if data is None: break - self.p.stdin.write(data[0]) - if data[1]: self.p.stdin.flush() + data = self.p.stdout.readline().decode("ascii") + if data == "": break + self.p_queue.put(data) + self.p_running = False def p_open(self): assert self.p is None self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_running = True + self.p_next = None self.p_queue = Queue() self.p_thread = Thread(target=self.p_thread_main) self.p_thread.start() def p_write(self, data, flush): assert self.p is not None - self.p_queue.put((bytes(data, "ascii"), flush)) + self.p.stdin.write(bytes(data, "ascii")) + if flush: self.p.stdin.flush() def p_read(self): assert self.p is not None - return self.p.stdout.readline().decode("ascii") + assert self.p_running + if self.p_next is not None: + data = self.p_next + self.p_next = None + return data + return self.p_queue.get() + + def p_poll(self): + assert self.p is not None + assert self.p_running + if self.p_next is not None: + return False + try: + self.p_next = self.p_queue.get(True, 0.1) + return False + except Empty: + return True def p_close(self): assert self.p is not None - self.p_queue.put(None) - self.p_thread.join() self.p.stdin.close() + self.p_thread.join() + assert not self.p_running self.p = None + self.p_next = None self.p_queue = None self.p_thread = None @@ -485,7 +505,7 @@ class SmtIo: count = 0 num_bs = 0 - while select([self.p.stdout], [], [], 0.1) == ([], [], []): + while self.p_poll(): count += 1 if count < 25: -- cgit v1.2.3 From 1e502ef5a005525840629e99c5a3f9cf938da52b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 26 Oct 2017 18:01:48 +0200 Subject: Fix typo in opt_clean log message --- passes/opt/opt_clean.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index fb1851868..2d2ffa9a1 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -392,7 +392,7 @@ bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose) } if (verbose) - log(" removing redundent init attribute on %s.\n", log_id(wire)); + log(" removing redundant init attribute on %s.\n", log_id(wire)); wire->attributes.erase("\\init"); did_something = true; -- cgit v1.2.3 From c238f45ecfd4fa3d556ea885a53d8e864e3c7566 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 26 Oct 2017 18:02:15 +0200 Subject: Fix memory corruption bug in opt_rmdff --- passes/opt/opt_rmdff.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc index 02f3e93f5..edec42c4d 100644 --- a/passes/opt/opt_rmdff.cc +++ b/passes/opt/opt_rmdff.cc @@ -430,6 +430,8 @@ struct OptRmdffPass : public Pass { assign_map.set(module); dff_init_map.set(module); + mux_drivers.clear(); + init_attributes.clear(); for (auto wire : module->wires()) { @@ -534,6 +536,7 @@ struct OptRmdffPass : public Pass { assign_map.clear(); mux_drivers.clear(); + init_attributes.clear(); if (total_count || total_initdrv) design->scratchpad_set_bool("opt.did_something", true); -- cgit v1.2.3 From 455c1c9d97330b9d20cafe62cd72c3c3f71d3573 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 29 Oct 2017 13:21:20 +0100 Subject: Fix SMT2 handling of initstate in sub-modules --- backends/smt2/smt2.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index dce7c25de..8daa52eb3 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -811,6 +811,9 @@ struct Smt2Worker Module *m = module->design->module(cell->type); log_assert(m != nullptr); + hier.push_back(stringf(" (= (|%s_is| state) (|%s_is| %s))\n", + get_id(module), get_id(cell->type), cell_state.c_str())); + for (auto &conn : cell->connections()) { Wire *w = m->wire(conn.first); -- cgit v1.2.3 From 4f31cb6daddedcee467d85797d81b79360ce1826 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 31 Oct 2017 12:40:25 +0100 Subject: Add "ltp" command --- passes/cmds/Makefile.inc | 1 + passes/cmds/ltp.cc | 185 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 186 insertions(+) create mode 100644 passes/cmds/ltp.cc diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc index 9e3934e16..44a83b2b9 100644 --- a/passes/cmds/Makefile.inc +++ b/passes/cmds/Makefile.inc @@ -28,4 +28,5 @@ OBJS += passes/cmds/edgetypes.o OBJS += passes/cmds/chformal.o OBJS += passes/cmds/chtype.o OBJS += passes/cmds/blackbox.o +OBJS += passes/cmds/ltp.o diff --git a/passes/cmds/ltp.cc b/passes/cmds/ltp.cc new file mode 100644 index 000000000..42dc794ec --- /dev/null +++ b/passes/cmds/ltp.cc @@ -0,0 +1,185 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * 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. + * + */ + +#include "kernel/yosys.h" +#include "kernel/celltypes.h" +#include "kernel/sigtools.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct LtpWorker +{ + RTLIL::Design *design; + RTLIL::Module *module; + SigMap sigmap; + + dict> bits; + dict> bit2bits; + dict> bit2ff; + + int maxlvl; + SigBit maxbit; + pool busy; + + LtpWorker(RTLIL::Module *module, bool noff) : design(module->design), module(module), sigmap(module) + { + CellTypes ff_celltypes; + + if (noff) { + ff_celltypes.setup_internals_mem(); + ff_celltypes.setup_stdcells_mem(); + } + + for (auto wire : module->selected_wires()) + for (auto bit : sigmap(wire)) + bits[bit] = tuple(-1, State::Sx, nullptr); + + for (auto cell : module->selected_cells()) + { + pool src_bits, dst_bits; + + for (auto &conn : cell->connections()) + for (auto bit : sigmap(conn.second)) { + if (cell->input(conn.first)) + src_bits.insert(bit); + if (cell->output(conn.first)) + dst_bits.insert(bit); + } + + if (noff && ff_celltypes.cell_known(cell->type)) { + for (auto s : src_bits) + for (auto d : dst_bits) { + bit2ff[s] = tuple(d, cell); + break; + } + continue; + } + + for (auto s : src_bits) + for (auto d : dst_bits) + bit2bits[s][d] = cell; + } + + maxlvl = -1; + maxbit = State::Sx; + } + + void runner(SigBit bit, int level, SigBit from, Cell *via) + { + auto &bitinfo = bits.at(bit); + + if (get<0>(bitinfo) >= level) + return; + + if (busy.count(bit) > 0) { + log_warning("Detected loop at %s in %s\n", log_signal(bit), log_id(module)); + return; + } + + busy.insert(bit); + get<0>(bitinfo) = level; + get<1>(bitinfo) = from; + get<2>(bitinfo) = via; + + if (level > maxlvl) { + maxlvl = level; + maxbit = bit; + } + + if (bit2bits.count(bit)) { + for (auto &it : bit2bits.at(bit)) + runner(it.first, level+1, bit, it.second); + } + + busy.erase(bit); + } + + void printpath(SigBit bit) + { + auto &bitinfo = bits.at(bit); + if (get<2>(bitinfo)) { + printpath(get<1>(bitinfo)); + log("%5d: %s (via %s)\n", get<0>(bitinfo), log_signal(bit), log_id(get<2>(bitinfo))); + } else { + log("%5d: %s\n", get<0>(bitinfo), log_signal(bit)); + } + } + + void run() + { + for (auto &it : bits) + if (get<0>(it.second) < 0) + runner(it.first, 0, State::Sx, nullptr); + + log("\n"); + log("Longest topological path in %s (length=%d):\n", log_id(module), maxlvl); + + if (maxlvl >= 0) + printpath(maxbit); + + if (bit2ff.count(maxbit)) + log("%5s: %s (via %s)\n", "ff", log_signal(get<0>(bit2ff.at(maxbit))), log_id(get<1>(bit2ff.at(maxbit)))); + } +}; + +struct LtpPass : public Pass { + LtpPass() : Pass("ltp", "print longest topological path") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" ltp [options] [selection]\n"); + log("\n"); + log("This command prints the longest topological path in the design. (Only considers\n"); + log("paths within a single module, so the design must be flattened.)\n"); + log("\n"); + log(" -noff\n"); + log(" automatically exclude FF cell types\n"); + log("\n"); + } + virtual void execute(std::vector args, RTLIL::Design *design) + { + bool noff = false; + + log_header(design, "Executing LTP pass (find longest path).\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-noff") { + noff = true; + continue; + } + break; + } + + extra_args(args, argidx, design); + + for (Module *module : design->selected_modules()) + { + if (module->has_processes_warn()) + continue; + + LtpWorker worker(module, noff); + worker.run(); + } + } +} LtpPass; + +PRIVATE_NAMESPACE_END -- cgit v1.2.3 From 9ae25039fb6e28db639372d67c1b72c4170feaa3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 8 Nov 2017 02:54:24 +0100 Subject: Add support for editline as replacement for readline --- Makefile | 6 ++++++ kernel/driver.cc | 16 +++++++++++++--- kernel/yosys.cc | 23 ++++++++++++++++------- passes/cmds/show.cc | 4 ++++ 4 files changed, 39 insertions(+), 10 deletions(-) diff --git a/Makefile b/Makefile index eb8f0f594..924fd88b7 100644 --- a/Makefile +++ b/Makefile @@ -11,6 +11,7 @@ ENABLE_TCL := 1 ENABLE_ABC := 1 ENABLE_PLUGINS := 1 ENABLE_READLINE := 1 +ENABLE_EDITLINE := 0 ENABLE_VERIFIC := 0 ENABLE_COVER := 1 ENABLE_LIBYOSYS := 0 @@ -226,6 +227,11 @@ endif ifeq ($(CONFIG),mxe) LDLIBS += -ltermcap endif +else +ifeq ($(ENABLE_EDITLINE),1) +CXXFLAGS += -DYOSYS_ENABLE_EDITLINE +LDLIBS += -ledit -ltinfo -lbsd +endif endif ifeq ($(ENABLE_PLUGINS),1) diff --git a/kernel/driver.cc b/kernel/driver.cc index 1fe61b499..c5e31d718 100644 --- a/kernel/driver.cc +++ b/kernel/driver.cc @@ -25,6 +25,10 @@ # include #endif +#ifdef YOSYS_ENABLE_EDITLINE +# include +#endif + #include #include #include @@ -119,27 +123,33 @@ const char *prompt() #else /* EMSCRIPTEN */ -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) int yosys_history_offset = 0; std::string yosys_history_file; #endif void yosys_atexit() { -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) if (!yosys_history_file.empty()) { +#if defined(YOSYS_ENABLE_READLINE) if (yosys_history_offset > 0) { history_truncate_file(yosys_history_file.c_str(), 100); append_history(where_history() - yosys_history_offset, yosys_history_file.c_str()); } else write_history(yosys_history_file.c_str()); +#else + write_history(yosys_history_file.c_str()); +#endif } clear_history(); +#if defined(YOSYS_ENABLE_READLINE) HIST_ENTRY **hist_list = history_list(); if (hist_list != NULL) free(hist_list); #endif +#endif } int main(int argc, char **argv) @@ -159,7 +169,7 @@ int main(int argc, char **argv) bool mode_v = false; bool mode_q = false; -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) if (getenv("HOME") != NULL) { yosys_history_file = stringf("%s/.yosys_history", getenv("HOME")); read_history(yosys_history_file.c_str()); diff --git a/kernel/yosys.cc b/kernel/yosys.cc index e5b22eba7..34665a0ad 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -25,6 +25,10 @@ # include #endif +#ifdef YOSYS_ENABLE_EDITLINE +# include +#endif + #ifdef YOSYS_ENABLE_PLUGINS # include #endif @@ -938,7 +942,7 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig Backend::backend_call(design, NULL, filename, command); } -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) static char *readline_cmd_generator(const char *text, int state) { static std::map::iterator it; @@ -1025,14 +1029,14 @@ void shell(RTLIL::Design *design) recursion_counter++; log_cmd_error_throw = true; -#ifdef YOSYS_ENABLE_READLINE - rl_readline_name = "yosys"; +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) + rl_readline_name = (char*)"yosys"; rl_attempted_completion_function = readline_completion; - rl_basic_word_break_characters = " \t\n"; + rl_basic_word_break_characters = (char*)" \t\n"; #endif char *command = NULL; -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) while ((command = readline(create_prompt(design, recursion_counter))) != NULL) { #else @@ -1046,7 +1050,7 @@ void shell(RTLIL::Design *design) #endif if (command[strspn(command, " \t\r\n")] == 0) continue; -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) add_history(command); #endif @@ -1114,7 +1118,7 @@ struct ShellPass : public Pass { } } ShellPass; -#ifdef YOSYS_ENABLE_READLINE +#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) struct HistoryPass : public Pass { HistoryPass() : Pass("history", "show last interactive commands") { } virtual void help() { @@ -1128,8 +1132,13 @@ struct HistoryPass : public Pass { } virtual void execute(std::vector args, RTLIL::Design *design) { extra_args(args, 1, design, false); +#ifdef YOSYS_ENABLE_READLINE for(HIST_ENTRY **list = history_list(); *list != NULL; list++) log("%s\n", (*list)->line); +#else + for (int i = where_history(); history_get(i); i++) + log("%s\n", history_get(i)->line); +#endif } } HistoryPass; #endif diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 3a3939a81..02624cf30 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -30,6 +30,10 @@ # include #endif +#ifdef YOSYS_ENABLE_EDITLINE +# include +#endif + USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -- cgit v1.2.3