diff options
103 files changed, 4704 insertions, 421 deletions
@@ -2,9 +2,30 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.25 .. Yosys 0.25-dev +Yosys 0.26 .. Yosys 0.26-dev -------------------------- + +Yosys 0.25 .. Yosys 0.26 +-------------------------- + * New commands and options + - Added "bwmuxmap" pass to replace $bwmux cells with equivalent logic. + - Added "xprop" experimental pass for formal x propagation. + - Added "splitcells" pass to split up multi-bit cells. + - Added "viz" pass to visualize data flow graph. + - Added option "-make_cover" to "miter" pass. + - Added option "-noparallelcase" to "write_verilog" pass. + - Added option "-chain" to "insbuf" pass. + - Added options "-hierarchy" and "-assume" to "formalff" pass. + - Added options "-append" and "-summary" to "sim" pass. + - Added option "-ywmap" to "write_btor" pass. + - Added option "-ignore-self-reset" to "fsm_detect" pass. + + * Verilog + - Support for struct members of union type. + - Support for struct member package types. + * Various + - Added Yosys witness (.yw) cosimulation. - GCC 4.8 is deprecated, compiler with full C++11 support is required. Yosys 0.24 .. Yosys 0.25 @@ -141,7 +141,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.25+8 +YOSYS_VER := 0.26+53 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -157,7 +157,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline e02b7f6.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7e58866.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -165,7 +165,7 @@ bumpversion: # 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 = be9a35c +ABCREV = 2c1c83f ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) @@ -653,7 +653,7 @@ ifneq ($(ABCEXTERNAL),) kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' endif endif -OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o +OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o ifeq ($(ENABLE_ZLIB),1) OBJS += kernel/fstdata.o endif @@ -837,6 +837,9 @@ ABCOPT="" endif test: $(TARGETS) $(EXTRA_TARGETS) +ifeq ($(ENABLE_VERIFIC),1) + +cd tests/verific && bash run-test.sh $(SEEDOPT) +endif +cd tests/simple && bash run-test.sh $(SEEDOPT) +cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT) +cd tests/hana && bash run-test.sh $(SEEDOPT) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 513f9d95a..4ef28be9f 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -19,6 +19,8 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/json.h" +#include "kernel/yw.h" #include "libs/json11/json11.hpp" USING_YOSYS_NAMESPACE @@ -709,30 +711,19 @@ struct AigerWriter f << it.second; } - template<class T> static std::vector<std::string> witness_path(T *obj) { - std::vector<std::string> path; - if (obj->name.isPublic()) { - auto hdlname = obj->get_string_attribute(ID::hdlname); - for (auto token : split_tokens(hdlname)) - path.push_back("\\" + token); - } - if (path.empty()) - path.push_back(obj->name.str()); - return path; - } - - void write_ywmap(std::ostream &f) + void write_ywmap(PrettyJson &json) { - f << "{\n"; - f << " \"version\": \"Yosys Witness Aiger Map\",\n"; - f << stringf(" \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str()); - f << stringf(" \"latch_count\": %d,\n", aig_l); - f << stringf(" \"input_count\": %d,\n", aig_i); + json.begin_object(); + json.entry("version", "Yosys Witness Aiger map"); + json.entry("gennerator", yosys_version_str); - dict<int, string> clock_lines; - dict<int, string> input_lines; - dict<int, string> init_lines; - dict<int, string> seq_lines; + json.entry("latch_count", aig_l); + json.entry("input_count", aig_i); + + dict<int, Json> clock_lines; + dict<int, Json> input_lines; + dict<int, Json> init_lines; + dict<int, Json> seq_lines; for (auto cell : module->cells()) { @@ -751,21 +742,21 @@ struct AigerWriter if (init_inputs.count(sig[i])) { int a = init_inputs.at(sig[i]); log_assert((a & 1) == 0); - init_lines[a] += json11::Json(json11::Json::object { + init_lines[a] = json11::Json(json11::Json::object { { "path", witness_path(wire) }, { "input", (a >> 1) - 1 }, { "offset", sig_qy[i].offset }, - }).dump(); + }); } if (input_bits.count(sig[i])) { int a = aig_map.at(sig[i]); log_assert((a & 1) == 0); - seq_lines[a] += json11::Json(json11::Json::object { + seq_lines[a] = json11::Json(json11::Json::object { { "path", witness_path(wire) }, { "input", (a >> 1) - 1 }, { "offset", sig_qy[i].offset }, - }).dump(); + }); } } } @@ -783,60 +774,55 @@ struct AigerWriter int a = aig_map.at(sig[i]); log_assert((a & 1) == 0); - input_lines[a] += json11::Json(json11::Json::object { + input_lines[a] = json11::Json(json11::Json::object { { "path", path }, { "input", (a >> 1) - 1 }, { "offset", i }, - }).dump(); + }); if (ywmap_clocks.count(sig[i])) { int clock_mode = ywmap_clocks[sig[i]]; if (clock_mode != 3) { - clock_lines[a] += json11::Json(json11::Json::object { + clock_lines[a] = json11::Json(json11::Json::object { { "path", path }, { "input", (a >> 1) - 1 }, { "offset", i }, { "edge", clock_mode == 1 ? "posedge" : "negedge" }, - }).dump(); + }); } } } } } - f << " \"clocks\": ["; + json.name("clocks"); + json.begin_array(); clock_lines.sort(); - const char *sep = "\n "; - for (auto &it : clock_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ],\n"; + for (auto &it : clock_lines) + json.value(it.second); + json.end_array(); - f << " \"inputs\": ["; + json.name("inputs"); + json.begin_array(); input_lines.sort(); - sep = "\n "; - for (auto &it : input_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ],\n"; + for (auto &it : input_lines) + json.value(it.second); + json.end_array(); - f << " \"seqs\": ["; - sep = "\n "; - for (auto &it : seq_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ],\n"; + json.name("seqs"); + json.begin_array(); + input_lines.sort(); + for (auto &it : seq_lines) + json.value(it.second); + json.end_array(); - f << " \"inits\": ["; - sep = "\n "; - for (auto &it : init_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ]\n}\n"; + json.name("inits"); + json.begin_array(); + input_lines.sort(); + for (auto &it : init_lines) + json.value(it.second); + json.end_array(); + json.end_object(); } }; @@ -991,9 +977,12 @@ struct AigerBackend : public Backend { if (!yw_map_filename.empty()) { std::ofstream mapf; mapf.open(yw_map_filename.c_str(), std::ofstream::trunc); - if (mapf.fail()) - log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno)); - writer.write_ywmap(mapf); + + PrettyJson json; + + if (!json.write_to_file(yw_map_filename)) + log_error("Can't open file `%s' for writing: %s\n", yw_map_filename.c_str(), strerror(errno)); + writer.write_ywmap(json); } } } AigerBackend; diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 8368ab82d..4c43e91e7 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -28,6 +28,8 @@ #include "kernel/celltypes.h" #include "kernel/log.h" #include "kernel/mem.h" +#include "kernel/json.h" +#include "kernel/yw.h" #include <string> USING_YOSYS_NAMESPACE @@ -83,6 +85,22 @@ struct BtorWorker vector<string> info_lines; dict<int, int> info_clocks; + struct ywmap_btor_sig { + SigSpec sig; + Cell *cell = nullptr; + + ywmap_btor_sig(const SigSpec &sig) : sig(sig) {} + ywmap_btor_sig(Cell *cell) : cell(cell) {} + }; + + vector<ywmap_btor_sig> ywmap_inputs; + vector<ywmap_btor_sig> ywmap_states; + dict<SigBit, int> ywmap_clock_bits; + dict<SigBit, int> ywmap_clock_inputs; + + + PrettyJson ywmap_json; + void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3)) { va_list ap; @@ -126,6 +144,50 @@ struct BtorWorker return " " + infostr; } + void ywmap_state(const SigSpec &sig) { + if (ywmap_json.active()) + ywmap_states.emplace_back(sig); + } + + void ywmap_state(Cell *cell) { + if (ywmap_json.active()) + ywmap_states.emplace_back(cell); + } + + void ywmap_input(const SigSpec &sig) { + if (ywmap_json.active()) + ywmap_inputs.emplace_back(sig); + } + + void emit_ywmap_btor_sig(const ywmap_btor_sig &btor_sig) { + if (btor_sig.cell == nullptr) { + if (btor_sig.sig.empty()) { + ywmap_json.value(nullptr); + return; + } + ywmap_json.begin_array(); + ywmap_json.compact(); + for (auto &chunk : btor_sig.sig.chunks()) { + log_assert(chunk.is_wire()); + + ywmap_json.begin_object(); + ywmap_json.entry("path", witness_path(chunk.wire)); + ywmap_json.entry("width", chunk.width); + ywmap_json.entry("offset", chunk.offset); + ywmap_json.end_object(); + } + ywmap_json.end_array(); + } else { + ywmap_json.begin_object(); + ywmap_json.compact(); + ywmap_json.entry("path", witness_path(btor_sig.cell)); + Mem *mem = mem_cells[btor_sig.cell]; + ywmap_json.entry("width", mem->width); + ywmap_json.entry("size", mem->size); + ywmap_json.end_object(); + } + } + void btorf_push(const string &id) { if (verbose) { @@ -617,7 +679,7 @@ struct BtorWorker SigSpec sig_d = sigmap(cell->getPort(ID::D)); SigSpec sig_q = sigmap(cell->getPort(ID::Q)); - if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_))) + if ((!info_filename.empty() || ywmap_json.active()) && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_))) { SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C)); int nid = get_sig_nid(sig_c); @@ -629,7 +691,11 @@ struct BtorWorker if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool()) negedge = true; - info_clocks[nid] |= negedge ? 2 : 1; + if (!info_filename.empty()) + info_clocks[nid] |= negedge ? 2 : 1; + + if (ywmap_json.active()) + ywmap_clock_bits[sig_c] |= negedge ? 2 : 1; } IdString symbol; @@ -662,6 +728,8 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(symbol)); + ywmap_state(sig_q); + if (nid_init_val >= 0) { int nid_init = next_nid++; if (verbose) @@ -683,6 +751,8 @@ struct BtorWorker btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str()); + ywmap_state(sig_y); + if (cell->type == ID($anyconst)) { int nid2 = next_nid++; btorf("%d next %d %d %d\n", nid2, sid, nid, nid); @@ -705,6 +775,8 @@ struct BtorWorker btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str()); btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid); btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid); + + ywmap_state(sig_y); } add_nid_sig(initstate_nid, sig_y); @@ -768,6 +840,8 @@ struct BtorWorker nid_init_val = next_nid++; btorf("%d state %d\n", nid_init_val, sid); + ywmap_state(nullptr); + for (int i = 0; i < mem->size; i++) { Const thisword = initdata.extract(i*mem->width, mem->width); if (thisword.is_fully_undef()) @@ -793,6 +867,8 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(mem->memid)); + ywmap_state(cell); + if (nid_init_val >= 0) { int nid_init = next_nid++; @@ -915,10 +991,13 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig)); int nid_input = next_nid++; - if (is_init) + if (is_init) { btorf("%d state %d\n", nid_input, sid); - else + ywmap_state(sig); + } else { btorf("%d input %d\n", nid_input, sid); + ywmap_input(sig); + } int nid_masked_input; if (sig_mask_undef.is_fully_ones()) { @@ -993,6 +1072,7 @@ struct BtorWorker int sid = get_bv_sid(GetSize(s)); int nid = next_nid++; btorf("%d input %d\n", nid, sid); + ywmap_input(s); nid_width[nid] = GetSize(s); for (int j = 0; j < GetSize(s); j++) @@ -1075,12 +1155,15 @@ struct BtorWorker return nid; } - BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename) : + BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename, string ywmap_filename) : f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), print_internal_names(print_internal_names), info_filename(info_filename) { if (!info_filename.empty()) infof("name %s\n", log_id(module)); + if (!ywmap_filename.empty()) + ywmap_json.write_to_file(ywmap_filename); + memories = Mem::get_all_memories(module); dict<IdString, Mem*> mem_dict; @@ -1094,6 +1177,20 @@ struct BtorWorker btorf_push("inputs"); + if (ywmap_json.active()) { + for (auto wire : module->wires()) + { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr == wire->attributes.end()) + continue; + SigSpec sig = sigmap(wire); + if (gclk_attr->second == State::S1) + ywmap_clock_bits[sig] |= 1; + else if (gclk_attr->second == State::S0) + ywmap_clock_bits[sig] |= 2; + } + } + for (auto wire : module->wires()) { if (wire->attributes.count(ID::init)) { @@ -1111,6 +1208,7 @@ struct BtorWorker int nid = next_nid++; btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str()); + ywmap_input(wire); add_nid_sig(nid, sig); if (!info_filename.empty()) { @@ -1122,6 +1220,16 @@ struct BtorWorker info_clocks[nid] |= 2; } } + + if (ywmap_json.active()) { + for (int i = 0; i < GetSize(sig); i++) { + auto input_bit = SigBit(wire, i); + auto bit = sigmap(input_bit); + if (!ywmap_clock_bits.count(bit)) + continue; + ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit]; + } + } } btorf_pop("inputs"); @@ -1378,6 +1486,42 @@ struct BtorWorker f << it; f.close(); } + + if (ywmap_json.active()) + { + ywmap_json.begin_object(); + ywmap_json.entry("version", "Yosys Witness BTOR map"); + ywmap_json.entry("generator", yosys_version_str); + + ywmap_json.name("clocks"); + ywmap_json.begin_array(); + for (auto &entry : ywmap_clock_inputs) { + if (entry.second != 1 && entry.second != 2) + continue; + log_assert(entry.first.is_wire()); + ywmap_json.begin_object(); + ywmap_json.compact(); + ywmap_json.entry("path", witness_path(entry.first.wire)); + ywmap_json.entry("offset", entry.first.offset); + ywmap_json.entry("edge", entry.second == 1 ? "posedge" : "negedge"); + ywmap_json.end_object(); + } + ywmap_json.end_array(); + + ywmap_json.name("inputs"); + ywmap_json.begin_array(); + for (auto &entry : ywmap_inputs) + emit_ywmap_btor_sig(entry); + ywmap_json.end_array(); + + ywmap_json.name("states"); + ywmap_json.begin_array(); + for (auto &entry : ywmap_states) + emit_ywmap_btor_sig(entry); + ywmap_json.end_array(); + + ywmap_json.end_object(); + } } }; @@ -1406,11 +1550,15 @@ struct BtorBackend : public Backend { log(" -x\n"); log(" Output symbols for internal netnames (starting with '$')\n"); log("\n"); + log(" -ywmap <filename>\n"); + log(" Create a map file for conversion to and from Yosys witness traces\n"); + log("\n"); } void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override { bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false; string info_filename; + string ywmap_filename; log_header(design, "Executing BTOR backend.\n"); @@ -1443,6 +1591,10 @@ struct BtorBackend : public Backend { print_internal_names = true; continue; } + if (args[argidx] == "-ywmap" && argidx+1 < args.size()) { + ywmap_filename = args[++argidx]; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -1455,7 +1607,7 @@ struct BtorBackend : public Backend { *f << stringf("; BTOR description generated by %s for module %s.\n", yosys_version_str, log_id(topmod)); - BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename); + BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename, ywmap_filename); *f << stringf("; end of yosys output\n"); } diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc index e483117d1..eb30ab4b9 100644 --- a/backends/firrtl/firrtl.cc +++ b/backends/firrtl/firrtl.cc @@ -346,6 +346,12 @@ void emit_elaborated_extmodules(RTLIL::Design *design, std::ostream &f) { // Find the module corresponding to this instance. auto modInstance = design->module(cell->type); + // Ensure that we actually have a module instance + if (modInstance == nullptr) { + log_error("Unknown cell type %s\n", cell->type.c_str()); + return; + } + bool modIsBlackbox = modInstance->get_blackbox_attribute(); if (modIsBlackbox) @@ -1238,6 +1244,9 @@ struct FirrtlBackend : public Backend { if (top == nullptr) top = last; + if (!top) + log_cmd_error("There is no top module in this design!\n"); + std::string circuitFileinfo = getFileinfo(top); *f << stringf("circuit %s: %s\n", make_id(top->name), circuitFileinfo.c_str()); diff --git a/backends/jny/jny.cc b/backends/jny/jny.cc index 2b8d51b76..0be11a52c 100644 --- a/backends/jny/jny.cc +++ b/backends/jny/jny.cc @@ -546,8 +546,9 @@ struct JnyPass : public Pass { std::ostream *f; std::stringstream buf; + bool empty = filename.empty(); - if (!filename.empty()) { + if (!empty) { rewrite_filename(filename); std::ofstream *ff = new std::ofstream; ff->open(filename.c_str(), std::ofstream::trunc); @@ -565,7 +566,7 @@ struct JnyPass : public Pass { JnyWriter jny_writer(*f, false, connections, attributes, properties); jny_writer.write_metadata(design, 0, invk.str()); - if (!filename.empty()) { + if (!empty) { delete f; } else { log("%s", buf.str().c_str()); diff --git a/backends/json/json.cc b/backends/json/json.cc index 1ff0a6c66..fd2c922fd 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -666,8 +666,9 @@ struct JsonPass : public Pass { std::ostream *f; std::stringstream buf; + bool empty = filename.empty(); - if (!filename.empty()) { + if (!empty) { rewrite_filename(filename); std::ofstream *ff = new std::ofstream; ff->open(filename.c_str(), std::ofstream::trunc); @@ -683,7 +684,7 @@ struct JsonPass : public Pass { JsonWriter json_writer(*f, true, aig_mode, compat_int_mode); json_writer.write_design(design); - if (!filename.empty()) { + if (!empty) { delete f; } else { log("%s", buf.str().c_str()); diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc index b5163aefe..574eb3aaa 100644 --- a/backends/rtlil/rtlil_backend.cc +++ b/backends/rtlil/rtlil_backend.cc @@ -51,7 +51,7 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi } } f << stringf("%d'", width); - if (data.is_fully_undef()) { + if (data.is_fully_undef_x_only()) { f << "x"; } else { for (int i = offset+width-1; i >= offset; i--) { @@ -530,8 +530,9 @@ struct DumpPass : public Pass { std::ostream *f; std::stringstream buf; + bool empty = filename.empty(); - if (!filename.empty()) { + if (!empty) { rewrite_filename(filename); std::ofstream *ff = new std::ofstream; ff->open(filename.c_str(), append ? std::ofstream::app : std::ofstream::trunc); @@ -546,7 +547,7 @@ struct DumpPass : public Pass { RTLIL_BACKEND::dump_design(*f, design, true, flag_m, flag_n); - if (!filename.empty()) { + if (!empty) { delete f; } else { log("%s", buf.str().c_str()); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index fe50ca7f6..48da3f4be 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -458,11 +458,14 @@ struct Smt2Worker { RTLIL::SigSpec sig_a, sig_b; RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); + bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool(); int width = GetSize(sig_y); if (type == 's' || type == 'S' || type == 'd' || type == 'b') { - width = max(width, GetSize(cell->getPort(ID::A))); + if (type == 'b') + width = GetSize(cell->getPort(ID::A)); + else + width = max(width, GetSize(cell->getPort(ID::A))); if (cell->hasPort(ID::B)) width = max(width, GetSize(cell->getPort(ID::B))); } @@ -483,6 +486,7 @@ struct Smt2Worker if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B)); + else if (ch == 'S') processed_expr += get_bv(cell->getPort(ID::S)); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; @@ -639,6 +643,9 @@ struct Smt2Worker if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)"); if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)"); + if (cell->type == ID($bweqx)) return export_bvop(cell, "(bvxnor A B)", 'U'); + if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U'); + if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's'); if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's'); if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's'); @@ -994,7 +1001,7 @@ struct Smt2Worker if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); - if (contains_clock) { + if (wire->port_input && contains_clock) { for (int i = 0; i < GetSize(sig); i++) { bool is_posedge = clock_posedge.count(sig[i]); bool is_negedge = clock_negedge.count(sig[i]); @@ -1744,7 +1751,6 @@ struct Smt2Backend : public Backend { log_push(); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); - Pass::call(design, "bwmuxmap"); log_pop(); size_t argidx; diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index a1e65569d..8d0cc8112 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -110,6 +110,10 @@ class AigerMap: def __init__(self, mapfile): data = json.load(mapfile) + version = data.get("version") if isinstance(data, dict) else {} + if version != "Yosys Witness Aiger map": + raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}") + self.latch_count = data["latch_count"] self.input_count = data["input_count"] @@ -250,5 +254,157 @@ def yw2aiw(input, mapfile, output): click.echo(f"Converted {len(inyw)} time steps.") +class BtorMap: + def __init__(self, mapfile): + self.data = data = json.load(mapfile) + + version = data.get("version") if isinstance(data, dict) else {} + if version != "Yosys Witness BTOR map": + raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}") + + self.sigmap = WitnessSigMap() + + for mode in ("states", "inputs"): + for btor_signal_def in data[mode]: + if btor_signal_def is None: + continue + if isinstance(btor_signal_def, dict): + btor_signal_def["path"] = tuple(btor_signal_def["path"]) + else: + for chunk in btor_signal_def: + chunk["path"] = tuple(chunk["path"]) + + +@cli.command(help=""" +Convert a BTOR witness trace into a Yosys witness trace. + +This requires a Yosys witness BTOR map file as generated by 'write_btor -ywmap'. +""") +@click.argument("input", type=click.File("r")) +@click.argument("mapfile", type=click.File("r")) +@click.argument("output", type=click.File("w")) +def wit2yw(input, mapfile, output): + input_name = input.name + click.echo(f"Converting BTOR witness trace {input_name!r} to Yosys witness trace {output.name!r}...") + click.echo(f"Using Yosys witness BTOR map file {mapfile.name!r}") + btor_map = BtorMap(mapfile) + + input = filter(None, (line.split(';', 1)[0].strip() for line in input)) + + sat = next(input, None) + if sat != "sat": + raise click.ClickException(f"{input_name}: not a BTOR witness file") + + props = next(input, None) + + t = -1 + + line = next(input, None) + + frames = [] + bits = {} + + while line and not line.startswith('.'): + current_t = int(line[1:].strip()) + if line[0] == '#': + mode = "states" + elif line[0] == '@': + mode = "inputs" + else: + raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file") + + if current_t > t: + t = current_t + values = WitnessValues() + array_inits = set() + frames.append(values) + + line = next(input, None) + while line and line[0] not in "#@.": + if current_t > 0 and mode == "states": + line = next(input, None) + continue + tokens = line.split() + line = next(input, None) + + btor_sig = btor_map.data[mode][int(tokens[0])] + btor_sigs = [btor_sig] + + if btor_sig is None: + continue + + if isinstance(btor_sig, dict): + addr = tokens[1] + if not addr.startswith('['): + addr = '[*]' + value = tokens[1] + else: + value = tokens[2] + if not addr.endswith(']'): + raise click.ClickException(f"{input_name}: expected address in BTOR witness file") + path = btor_sig["path"] + width = btor_sig["width"] + size = btor_sig["size"] + if addr == '[*]': + btor_sigs = [ + [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + for addr in range(size) + if (path, addr) not in array_inits + ] + array_inits.update((path, addr) for addr in range(size)) + else: + addr = int(addr[1:-1], 2) + + if addr < 0 or addr >= size: + raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file") + + array_inits.add((path, addr)) + btor_sig = [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + btor_sigs = [btor_sig] + else: + value = tokens[1] + + for btor_sig in btor_sigs: + value_bits = iter(reversed(value)) + + for chunk in btor_sig: + offset = chunk["offset"] + path = chunk["path"] + for i in range(offset, offset + chunk["width"]): + key = (path, i) + bits[key] = mode == "inputs" + values[key] = next(value_bits) + + if next(value_bits, None) is not None: + raise click.ClickException(f"{input_name}: excess bits in BTOR witness file") + + + if line is None: + raise click.ClickException(f"{input_name}: unexpected end of BTOR witness file") + if line.strip() != '.': + raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file") + if next(input, None) is not None: + raise click.ClickException(f"{input_name}: unexpected trailing data in BTOR witness file") + + outyw = WriteWitness(output, 'yosys-witness wit2yw') + + outyw.signals = coalesce_signals((), bits) + for clock in btor_map.data["clocks"]: + outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) + + for values in frames: + outyw.step(values) + + outyw.end_trace() + click.echo(f"Converted {outyw.t} time steps.") + if __name__ == "__main__": cli() diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py index 8469b4162..39cfac41e 100644 --- a/backends/smt2/ywio.py +++ b/backends/smt2/ywio.py @@ -175,8 +175,9 @@ class WitnessSig: return self.sort_key < other.sort_key -def coalesce_signals(signals): - bits = {} +def coalesce_signals(signals, bits=None): + if bits is None: + bits = {} for sig in signals: for bit in sig.bits(): if sig.init_only: diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 0a9c0590e..3da168960 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -2329,7 +2329,6 @@ struct VerilogBackend : public Backend { if (!noexpr) { Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); - Pass::call(design, "bwmuxmap"); } Pass::call(design, "clean_zerowidth"); log_pop(); diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc index 6097f02f5..982943d1b 100644 --- a/frontends/ast/ast.cc +++ b/frontends/ast/ast.cc @@ -1649,7 +1649,7 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, const dict<RTLIL::IdStr AstNode *new_ast = NULL; std::string modname = derive_common(design, parameters, &new_ast, quiet); - if (!design->has(modname)) { + if (!design->has(modname) && new_ast) { new_ast->str = modname; process_module(design, new_ast, false, NULL, quiet); design->module(modname)->check(); @@ -1699,6 +1699,7 @@ std::string AST::derived_module_name(std::string stripped_name, const std::vecto std::string AstModule::derive_common(RTLIL::Design *design, const dict<RTLIL::IdString, RTLIL::Const> ¶meters, AstNode **new_ast_out, bool quiet) { std::string stripped_name = name.str(); + (*new_ast_out) = nullptr; if (stripped_name.compare(0, 9, "$abstract") == 0) stripped_name = stripped_name.substr(9); diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 9327b34ee..1016ef636 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -877,7 +877,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun this_width = id_ast->children[0]->range_left - id_ast->children[0]->range_right + 1; if (children.size() > 1) range = children[1]; - } else if (id_ast->type == AST_STRUCT_ITEM || id_ast->type == AST_STRUCT) { + } else if (id_ast->type == AST_STRUCT_ITEM || id_ast->type == AST_STRUCT || id_ast->type == AST_UNION) { AstNode *tmp_range = make_struct_member_range(this, id_ast); this_width = tmp_range->range_left - tmp_range->range_right + 1; delete tmp_range; diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index da7933d2f..7edff38d9 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -278,17 +278,21 @@ static int range_width(AstNode *node, AstNode *rnode) log_file_error(node->filename, node->location.first_line, "Unpacked array in packed struct/union member %s\n", node->str.c_str()); } -static void save_struct_array_width(AstNode *node, int width) +static void save_struct_range_dimensions(AstNode *node, AstNode *rnode) { - // stash the stride for the array - node->multirange_dimensions.push_back(width); - + node->multirange_dimensions.push_back(rnode->range_right); + node->multirange_dimensions.push_back(range_width(node, rnode)); + node->multirange_swapped.push_back(rnode->range_swapped); } -static void save_struct_range_swapped(AstNode *node, bool range_swapped) +static int get_struct_range_offset(AstNode *node, int dimension) { - node->multirange_swapped.push_back(range_swapped); + return node->multirange_dimensions[2*dimension]; +} +static int get_struct_range_width(AstNode *node, int dimension) +{ + return node->multirange_dimensions[2*dimension + 1]; } static int size_packed_struct(AstNode *snode, int base_offset) @@ -322,14 +326,17 @@ static int size_packed_struct(AstNode *snode, int base_offset) if (node->children[1]->type == AST_RANGE) { // Unpacked array, e.g. bit [63:0] a [0:3] auto rnode = node->children[1]; - // C-style array size, e.g. bit [63:0] a [4] - bool c_type = rnode->children.size() == 1; - int array_count = c_type ? rnode->range_left : range_width(node, rnode); - save_struct_array_width(node, array_count); - save_struct_range_swapped(node, rnode->range_swapped || c_type); - save_struct_array_width(node, width); - save_struct_range_swapped(node, node->children[0]->range_swapped); - width *= array_count; + if (rnode->children.size() == 1) { + // C-style array size, e.g. bit [63:0] a [4] + node->multirange_dimensions.push_back(0); + node->multirange_dimensions.push_back(rnode->range_left); + node->multirange_swapped.push_back(true); + width *= rnode->range_left; + } else { + save_struct_range_dimensions(node, rnode); + width *= range_width(node, rnode); + } + save_struct_range_dimensions(node, node->children[0]); } else { // The Yosys extension for unpacked arrays in packed structs / unions @@ -338,8 +345,7 @@ static int size_packed_struct(AstNode *snode, int base_offset) } } else { // Vector - save_struct_array_width(node, width); - save_struct_range_swapped(node, node->children[0]->range_swapped); + save_struct_range_dimensions(node, node->children[0]); } // range nodes are now redundant for (AstNode *child : node->children) @@ -355,10 +361,8 @@ static int size_packed_struct(AstNode *snode, int base_offset) } width = 1; for (auto rnode : node->children[0]->children) { - int rwidth = range_width(node, rnode); - save_struct_array_width(node, rwidth); - save_struct_range_swapped(node, rnode->range_swapped); - width *= rwidth; + save_struct_range_dimensions(node, rnode); + width *= range_width(node, rnode); } // range nodes are now redundant for (AstNode *child : node->children) @@ -422,9 +426,14 @@ static AstNode *normalize_struct_index(AstNode *expr, AstNode *member_node, int { expr = expr->clone(); + int offset = get_struct_range_offset(member_node, dimension); + if (offset) { + expr = new AstNode(AST_SUB, expr, node_int(offset)); + } + if (member_node->multirange_swapped[dimension]) { // The dimension has swapped range; swap index into the struct accordingly. - int msb = member_node->multirange_dimensions[dimension] - 1; + int msb = get_struct_range_width(member_node, dimension) - 1; expr = new AstNode(AST_SUB, node_int(msb), expr); } @@ -433,7 +442,7 @@ static AstNode *normalize_struct_index(AstNode *expr, AstNode *member_node, int static AstNode *struct_index_lsb_offset(AstNode *lsb_offset, AstNode *rnode, AstNode *member_node, int dimension, int &stride) { - stride /= member_node->multirange_dimensions[dimension]; + stride /= get_struct_range_width(member_node, dimension); auto right = normalize_struct_index(rnode->children.back(), member_node, dimension); auto offset = stride > 1 ? multiply_by_const(right, stride) : right; return new AstNode(AST_ADD, lsb_offset, offset); @@ -1016,7 +1025,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, // create name resolution entries for all objects with names // also merge multiple declarations for the same wire (e.g. "output foobar; reg foobar;") - if (type == AST_MODULE) { + if (type == AST_MODULE || type == AST_INTERFACE) { current_scope.clear(); std::set<std::string> existing; int counter = 0; @@ -1701,7 +1710,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, current_filename = filename; - if (type == AST_MODULE) + if (type == AST_MODULE || type == AST_INTERFACE) current_scope.clear(); // convert defparam nodes to cell parameters @@ -2063,11 +2072,19 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage, if (name_has_dot(str, sname)) { if (current_scope.count(str) > 0) { auto item_node = current_scope[str]; - if (item_node->type == AST_STRUCT_ITEM || item_node->type == AST_STRUCT) { + if (item_node->type == AST_STRUCT_ITEM || item_node->type == AST_STRUCT || item_node->type == AST_UNION) { // structure member, rewrite this node to reference the packed struct wire auto range = make_struct_member_range(this, item_node); newNode = new AstNode(AST_IDENTIFIER, range); newNode->str = sname; + // save type and original number of dimensions for $size() etc. + newNode->attributes[ID::wiretype] = item_node->clone(); + if (!item_node->multirange_dimensions.empty() && children.size() > 0) { + if (children[0]->type == AST_RANGE) + newNode->integer = 1; + else if (children[0]->type == AST_MULTIRANGE) + newNode->integer = children[0]->children.size(); + } newNode->basic_prep = true; if (item_node->is_signed) newNode = new AstNode(AST_TO_SIGNED, newNode); @@ -3384,24 +3401,42 @@ skip_dynamic_range_lvalue_expansion:; id_ast = current_scope.at(buf->str); if (!id_ast) log_file_error(filename, location.first_line, "Failed to resolve identifier %s for width detection!\n", buf->str.c_str()); - // a slice of our identifier means we advance to the next dimension, e.g. $size(a[3]) - if (buf->children.size() > 0) { - // something is hanging below this identifier - if (buf->children[0]->type == AST_RANGE && buf->integer == 0) - // if integer == 0, this node was originally created as AST_RANGE so it's dimension is 1 - dim++; - // more than one range, e.g. $size(a[3][2]) - else // created an AST_MULTIRANGE, converted to AST_RANGE, but original dimension saved in 'integer' field - dim += buf->integer; // increment by multirange size + + // Check for item in packed struct / union + AST::AstNode *item_node; + if (id_ast->type == AST_WIRE && + buf->attributes.count(ID::wiretype) && (item_node = buf->attributes[ID::wiretype]) && + (item_node->type == AST_STRUCT_ITEM || item_node->type == AST_STRUCT || item_node->type == AST_UNION)) + { + // The dimension of the original array expression is saved in the 'integer' field + dim += buf->integer; + if (item_node->multirange_dimensions.empty()) { + if (dim != 1) + log_file_error(filename, location.first_line, "Dimension %d out of range in `%s', as it only has one dimension!\n", dim, item_node->str.c_str()); + left = high = item_node->range_left; + right = low = item_node->range_right; + } else { + int dims = GetSize(item_node->multirange_dimensions)/2; + if (dim < 1 || dim > dims) + log_file_error(filename, location.first_line, "Dimension %d out of range in `%s', as it only has dimensions 1..%d!\n", dim, item_node->str.c_str(), dims); + right = low = get_struct_range_offset(item_node, dim - 1); + left = high = low + get_struct_range_width(item_node, dim - 1) - 1; + if (item_node->multirange_swapped[dim - 1]) { + std::swap(left, right); + } + for (int i = dim; i < dims; i++) { + mem_depth *= get_struct_range_width(item_node, i); + } + } } - // We have 4 cases: + // Otherwise, we have 4 cases: // wire x; ==> AST_WIRE, no AST_RANGE children // wire [1:0]x; ==> AST_WIRE, AST_RANGE children // wire [1:0]x[1:0]; ==> AST_MEMORY, two AST_RANGE children (1st for packed, 2nd for unpacked) // wire [1:0]x[1:0][1:0]; ==> AST_MEMORY, one AST_RANGE child (0) for packed, then AST_MULTIRANGE child (1) for unpacked // (updated: actually by the time we are here, AST_MULTIRANGE is converted into one big AST_RANGE) // case 0 handled by default - if ((id_ast->type == AST_WIRE || id_ast->type == AST_MEMORY) && id_ast->children.size() > 0) { + else if ((id_ast->type == AST_WIRE || id_ast->type == AST_MEMORY) && id_ast->children.size() > 0) { // handle packed array left/right for case 1, and cases 2/3 when requesting the last dimension (packed side) AstNode *wire_range = id_ast->children[0]; left = wire_range->children[0]->integer; @@ -3410,6 +3445,17 @@ skip_dynamic_range_lvalue_expansion:; low = min(left, right); } if (id_ast->type == AST_MEMORY) { + // a slice of our identifier means we advance to the next dimension, e.g. $size(a[3]) + if (buf->children.size() > 0) { + // something is hanging below this identifier + if (buf->children[0]->type == AST_RANGE && buf->integer == 0) + // if integer == 0, this node was originally created as AST_RANGE so it's dimension is 1 + dim++; + // more than one range, e.g. $size(a[3][2]) + else // created an AST_MULTIRANGE, converted to AST_RANGE, but original dimension saved in 'integer' field + dim += buf->integer; // increment by multirange size + } + // We got here only if the argument is a memory // Otherwise $size() and $bits() return the expression width AstNode *mem_range = id_ast->children[1]; @@ -3469,7 +3515,7 @@ skip_dynamic_range_lvalue_expansion:; result = right; else if (str == "\\$size") result = width; - else { + else { // str == "\\$bits" result = width * mem_depth; } newNode = mkconst_int(result, true); @@ -4691,7 +4737,7 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg if (type == AST_MEMORY && (get_bool_attribute(ID::mem2reg) || (flags & AstNode::MEM2REG_FL_ALL) || !(is_reg || is_logic))) mem2reg_candidates[this] |= AstNode::MEM2REG_FL_FORCED; - if (type == AST_MODULE && get_bool_attribute(ID::mem2reg)) + if ((type == AST_MODULE || type == AST_INTERFACE) && get_bool_attribute(ID::mem2reg)) children_flags |= AstNode::MEM2REG_FL_ALL; dict<AstNode*, uint32_t> *proc_flags_p = NULL; @@ -4705,8 +4751,7 @@ void AstNode::mem2reg_as_needed_pass1(dict<AstNode*, pool<std::string>> &mem2reg children_flags |= AstNode::MEM2REG_FL_ASYNC; proc_flags_p = new dict<AstNode*, uint32_t>; } - - if (type == AST_INITIAL) { + else if (type == AST_INITIAL) { children_flags |= AstNode::MEM2REG_FL_INIT; proc_flags_p = new dict<AstNode*, uint32_t>; } diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 188ef2e04..cadbcaee6 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -500,8 +500,6 @@ struct LibertyFrontend : public Frontend { bool flag_ignore_miss_data_latch = false; std::vector<std::string> attributes; - log_header(design, "Executing Liberty frontend.\n"); - size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; @@ -546,6 +544,8 @@ struct LibertyFrontend : public Frontend { if (flag_wb && flag_lib) log_error("-wb and -lib cannot be specified together!\n"); + log_header(design, "Executing Liberty frontend: %s\n", filename.c_str()); + LibertyParser parser(*f); int cell_count = 0; diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index a93d79c80..ab3e55427 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -361,10 +361,16 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn for (unsigned i = 0; i < portbus->Size(); i++) { Net *net = inst->GetNet(portbus->ElementAtIndex(i)); if (net) { - if (net->IsGnd()) - sig.append(RTLIL::State::S0); - else if (net->IsPwr()) - sig.append(RTLIL::State::S1); + if (net->IsConstant()) { + if (net->IsGnd()) + sig.append(RTLIL::State::S0); + else if (net->IsPwr()) + sig.append(RTLIL::State::S1); + else if (net->IsX()) + sig.append(RTLIL::State::Sx); + else + sig.append(RTLIL::State::Sz); + } else sig.append(net_map_at(net)); } else @@ -379,6 +385,36 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn } } +RTLIL::SigSpec VerificImporter::operatorInportCase(Instance *inst, const char *portname) +{ + PortBus *portbus = inst->View()->GetPortBus(portname); + if (portbus) { + RTLIL::SigSpec sig; + for (unsigned i = 0; i < portbus->Size(); i++) { + Net *net = inst->GetNet(portbus->ElementAtIndex(i)); + if (net) { + if (net->IsConstant()) { + if (net->IsGnd()) + sig.append(RTLIL::State::S0); + else if (net->IsPwr()) + sig.append(RTLIL::State::S1); + else + sig.append(RTLIL::State::Sa); + } + else + sig.append(net_map_at(net)); + } else + sig.append(RTLIL::State::Sa); + } + return sig; + } else { + Port *port = inst->View()->GetPort(portname); + log_assert(port != NULL); + Net *net = inst->GetNet(port); + return net_map_at(net); + } +} + RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets) { RTLIL::SigSpec sig; @@ -989,6 +1025,75 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr return true; } + if (inst->Type() == OPER_WIDE_CASE_SELECT_BOX) + { + RTLIL::SigSpec sig_out_val = operatorInport(inst, "out_value"); + RTLIL::SigSpec sig_select = operatorInport(inst, "select"); + RTLIL::SigSpec sig_select_values = operatorInportCase(inst, "select_values"); + RTLIL::SigSpec sig_data_values = operatorInport(inst, "data_values"); + RTLIL::SigSpec sig_data_default = operatorInport(inst, "default_value"); + + RTLIL::Process *proc = module->addProcess(new_verific_id(inst)); + import_attributes(proc->attributes, inst); + + RTLIL::CaseRule *current_case = &proc->root_case; + current_case = &proc->root_case; + + RTLIL::SwitchRule *sw = new RTLIL::SwitchRule; + sw->signal = sig_select; + current_case->switches.push_back(sw); + + unsigned select_width = inst->InputSize(); + unsigned data_width = inst->OutputSize(); + unsigned offset_data = 0; + unsigned offset_select = 0; + + OperWideCaseSelector* selector = (OperWideCaseSelector*) inst->View(); + + for (unsigned i = 0 ; i < selector->GetNumBranches() ; ++i) { + + SigSig action(sig_out_val, sig_data_values.extract(offset_data, data_width)); + offset_data += data_width; + + for (unsigned j = 0 ; j < selector->GetNumConditions(i) ; ++j) { + Array left_bound, right_bound ; + selector->GetCondition(i, j, &left_bound, &right_bound); + + SigSpec sel_left = sig_select_values.extract(offset_select, select_width); + offset_select += select_width; + + if (right_bound.Size()) { + SigSpec sel_right = sig_select_values.extract(offset_select, select_width); + offset_select += select_width; + + log_assert(sel_right.is_fully_const() && sel_right.is_fully_def()); + log_assert(sel_left.is_fully_const() && sel_right.is_fully_def()); + + int32_t left = sel_left.as_int(); + int32_t right = sel_right.as_int(); + int width = sel_left.size(); + + for (int32_t i = right; i<left; i++) { + RTLIL::CaseRule *cs = new RTLIL::CaseRule; + cs->compare.push_back(RTLIL::Const(i,width)); + cs->actions.push_back(action); + sw->cases.push_back(cs); + } + } + + RTLIL::CaseRule *cs = new RTLIL::CaseRule; + cs->compare.push_back(sel_left); + cs->actions.push_back(action); + sw->cases.push_back(cs); + } + } + RTLIL::CaseRule *cs_default = new RTLIL::CaseRule; + cs_default->actions.push_back(SigSig(sig_out_val, sig_data_default)); + sw->cases.push_back(cs_default); + + return true; + } + #undef IN #undef IN1 #undef IN2 @@ -2317,8 +2422,8 @@ std::string verific_import(Design *design, const std::map<std::string,std::strin const char *lib_name = (prefix) ? prefix->GetName() : 0 ; if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ; } - veri_module = (lib && module_name) ? lib->GetModule(module_name->GetName(), 1) : 0; - top = veri_module->GetName(); + if (lib && module_name) + top = lib->GetModule(module_name->GetName(), 1)->GetName(); } } @@ -2344,6 +2449,7 @@ std::string verific_import(Design *design, const std::map<std::string,std::strin int i; FOREACH_ARRAY_ITEM(netlists, i, nl) { + if (!nl) continue; if (!top.empty() && nl->CellBaseName() != top) continue; nl->AddAtt(new Att(" \\top", NULL)); @@ -3297,8 +3403,8 @@ struct VerificPass : public Pass { const char *lib_name = (prefix) ? prefix->GetName() : 0 ; if (!Strings::compare("work", lib_name)) lib = veri_file::GetLibrary(lib_name, 1) ; } - veri_module = (lib && module_name) ? lib->GetModule(module_name->GetName(), 1) : 0; - top_mod_names.insert(veri_module->GetName()); + if (lib && module_name) + top_mod_names.insert(lib->GetModule(module_name->GetName(), 1)->GetName()); } } else { log("Adding Verilog module '%s' to elaboration queue.\n", name); @@ -3333,6 +3439,7 @@ struct VerificPass : public Pass { int i; FOREACH_ARRAY_ITEM(netlists, i, nl) { + if (!nl) continue; if (!top_mod_names.count(nl->CellBaseName())) continue; nl->AddAtt(new Att(" \\top", NULL)); diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index d9f0077db..44485751c 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -87,6 +87,7 @@ struct VerificImporter RTLIL::SigSpec operatorInput1(Verific::Instance *inst); RTLIL::SigSpec operatorInput2(Verific::Instance *inst); RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname); + RTLIL::SigSpec operatorInportCase(Verific::Instance *inst, const char *portname); RTLIL::SigSpec operatorOutput(Verific::Instance *inst, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr); bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name); diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 12bac2a3d..986a98643 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1777,7 +1777,7 @@ struct VerificSvaImporter if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q); if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q); - importer->import_attributes(c->attributes, root); + if (c) importer->import_attributes(c->attributes, root); return; } @@ -1822,7 +1822,7 @@ struct VerificSvaImporter if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q); if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q); - importer->import_attributes(c->attributes, root); + if (c) importer->import_attributes(c->attributes, root); } } catch (ParserErrorException) diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 70ee47561..87b50438a 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -173,6 +173,13 @@ static bool isInLocalScope(const std::string *name) static AstNode *getTypeDefinitionNode(std::string type_name) { + // check package types + if (type_name.find("::") != std::string::npos && pkg_user_types.count(type_name) > 0) { + auto typedef_node = pkg_user_types[type_name]; + log_assert(typedef_node->type == AST_TYPEDEF); + return typedef_node->children[0]; + } + // check current scope then outer scopes for a name for (auto it = user_type_stack.rbegin(); it != user_type_stack.rend(); ++it) { if (it->count(type_name) > 0) { diff --git a/kernel/constids.inc b/kernel/constids.inc index 239381f85..39211d0c7 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -259,5 +259,6 @@ X(WR_PORTS) X(WR_PRIORITY_MASK) X(WR_WIDE_CONTINUATION) X(X) +X(xprop_decoder) X(Y) X(Y_WIDTH) diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc index 1b8043f9a..65ae3426c 100644 --- a/kernel/fstdata.cc +++ b/kernel/fstdata.cc @@ -197,7 +197,7 @@ static void reconstruct_clb_attimes(void *user_data, uint64_t pnt_time, fstHandl void FstData::reconstruct_callback_attimes(uint64_t pnt_time, fstHandle pnt_facidx, const unsigned char *pnt_value, uint32_t /* plen */) { - if (pnt_time > end_time) return; + if (pnt_time > end_time || !pnt_value) return; // if we are past the timestamp bool is_clock = false; if (!all_samples) { diff --git a/kernel/json.cc b/kernel/json.cc new file mode 100644 index 000000000..738746267 --- /dev/null +++ b/kernel/json.cc @@ -0,0 +1,172 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one> + * + * 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/json.h" + +USING_YOSYS_NAMESPACE + +void PrettyJson::emit_to_log() +{ + struct LogTarget : public Target { + void emit(const char *data) override { log("%s", data); } + }; + + targets.push_back(std::unique_ptr<Target>(new LogTarget)); +} + +void PrettyJson::append_to_string(std::string &target) +{ + struct AppendStringTarget : public Target { + std::string ⌖ + AppendStringTarget(std::string &target) : target(target) {} + void emit(const char *data) override { target += data; } + }; + + targets.push_back(std::unique_ptr<Target>(new AppendStringTarget(target))); +} + +bool PrettyJson::write_to_file(const std::string &path) +{ + struct WriteFileTarget : public Target { + std::ofstream target; + void emit(const char *data) override { target << data; } + void flush() override { target.flush(); } + }; + + auto target = std::unique_ptr<WriteFileTarget>(new WriteFileTarget); + target->target.open(path); + if (target->target.fail()) + return false; + targets.push_back(std::unique_ptr<Target>(target.release())); + return true; +} + +void PrettyJson::line(bool space_if_inline) +{ + if (compact_depth != INT_MAX) { + if (space_if_inline) + raw(" "); + return; + } + int indent = state.size() - (state.empty() ? 0 : state.back() == VALUE); + newline_indent.resize(1 + 2 * indent, ' '); + raw(newline_indent.c_str()); +} + +void PrettyJson::raw(const char *raw_json) +{ + for (auto &target : targets) + target->emit(raw_json); +} + +void PrettyJson::flush() +{ + for (auto &target : targets) + target->flush(); +} + +void PrettyJson::begin_object() +{ + begin_value(); + raw("{"); + state.push_back(OBJECT_FIRST); +} + +void PrettyJson::begin_array() +{ + begin_value(); + raw("["); + state.push_back(ARRAY_FIRST); +} + +void PrettyJson::end_object() +{ + Scope top_scope = state.back(); + state.pop_back(); + if (top_scope == OBJECT) + line(false); + else + log_assert(top_scope == OBJECT_FIRST); + raw("}"); + end_value(); +} + +void PrettyJson::end_array() +{ + Scope top_scope = state.back(); + state.pop_back(); + if (top_scope == ARRAY) + line(false); + else + log_assert(top_scope == ARRAY_FIRST); + raw("]"); + end_value(); +} + +void PrettyJson::name(const char *name) +{ + if (state.back() == OBJECT_FIRST) { + state.back() = OBJECT; + line(false); + } else { + raw(","); + line(); + } + raw(Json(name).dump().c_str()); + raw(": "); + state.push_back(VALUE); +} + +void PrettyJson::begin_value() +{ + if (state.back() == ARRAY_FIRST) { + line(false); + state.back() = ARRAY; + } else if (state.back() == ARRAY) { + raw(","); + line(); + } else { + log_assert(state.back() == VALUE); + state.pop_back(); + } +} + +void PrettyJson::end_value() +{ + if (state.empty()) { + raw("\n"); + flush(); + } + if (GetSize(state) < compact_depth) + compact_depth = INT_MAX; +} + +void PrettyJson::value_json(const Json &value) +{ + begin_value(); + raw(value.dump().c_str()); + end_value(); +} + +void PrettyJson::entry_json(const char *name, const Json &value) +{ + this->name(name); + this->value(value); +} + diff --git a/kernel/json.h b/kernel/json.h new file mode 100644 index 000000000..c9aa0e045 --- /dev/null +++ b/kernel/json.h @@ -0,0 +1,104 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one> + * + * 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. + * + */ + +#ifndef JSON_H +#define JSON_H + +#include "kernel/yosys.h" +#include "libs/json11/json11.hpp" +#include <functional> + +YOSYS_NAMESPACE_BEGIN + +using json11::Json; + +class PrettyJson +{ + enum Scope { + VALUE, + OBJECT_FIRST, + OBJECT, + ARRAY_FIRST, + ARRAY, + }; + + struct Target { + virtual void emit(const char *data) = 0; + virtual void flush() {}; + virtual ~Target() {}; + }; + + std::string newline_indent = "\n"; + std::vector<std::unique_ptr<Target>> targets; + std::vector<Scope> state = {VALUE}; + int compact_depth = INT_MAX; +public: + + void emit_to_log(); + void append_to_string(std::string &target); + bool write_to_file(const std::string &path); + + bool active() { return !targets.empty(); } + + void compact() { compact_depth = GetSize(state); } + + void line(bool space_if_inline = true); + void raw(const char *raw_json); + void flush(); + void begin_object(); + void begin_array(); + void end_object(); + void end_array(); + void name(const char *name); + void begin_value(); + void end_value(); + void value_json(const Json &value); + void value(unsigned int value) { value_json(Json((int)value)); } + template<typename T> + void value(T &&value) { value_json(Json(std::forward<T>(value))); }; + + void entry_json(const char *name, const Json &value); + void entry(const char *name, unsigned int value) { entry_json(name, Json((int)value)); } + template<typename T> + void entry(const char *name, T &&value) { entry_json(name, Json(std::forward<T>(value))); }; + + template<typename T> + void object(const T &&values) + { + begin_object(); + for (auto &item : values) + entry(item.first, item.second); + end_object(); + } + + template<typename T> + void array(const T &&values) + { + begin_object(); + for (auto &item : values) + value(item); + end_object(); + } +}; + + + +YOSYS_NAMESPACE_END + +#endif diff --git a/kernel/log.cc b/kernel/log.cc index 0092871f0..75a1ffb45 100644 --- a/kernel/log.cc +++ b/kernel/log.cc @@ -707,6 +707,7 @@ void log_check_expected() if (item.second.current_count == item.second.expected_count) { log_warn_regexes.clear(); log("Expected error pattern '%s' found !!!\n", item.first.c_str()); + yosys_shutdown(); #ifdef EMSCRIPTEN throw 0; #elif defined(_MSC_VER) diff --git a/kernel/register.cc b/kernel/register.cc index 0e4d503be..9ffb17c1a 100644 --- a/kernel/register.cc +++ b/kernel/register.cc @@ -531,10 +531,11 @@ void Frontend::extra_args(std::istream *&f, std::string &filename, std::vector<s std::ifstream *ff = new std::ifstream; ff->open(filename.c_str(), bin_input ? std::ifstream::binary : std::ifstream::in); yosys_input_files.insert(filename); - if (ff->fail()) + if (ff->fail()) { delete ff; - else - f = ff; + ff = nullptr; + } + f = ff; if (f != NULL) { // Check for gzip magic unsigned char magic[3]; diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index eee014c54..7f3508b2f 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -370,6 +370,17 @@ bool RTLIL::Const::is_fully_undef() const return true; } +bool RTLIL::Const::is_fully_undef_x_only() const +{ + cover("kernel.rtlil.const.is_fully_undef_x_only"); + + for (const auto &bit : bits) + if (bit != RTLIL::State::Sx) + return false; + + return true; +} + bool RTLIL::Const::is_onehot(int *pos) const { cover("kernel.rtlil.const.is_onehot"); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 42bb66da8..7c7669caa 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -686,6 +686,7 @@ struct RTLIL::Const bool is_fully_ones() const; bool is_fully_def() const; bool is_fully_undef() const; + bool is_fully_undef_x_only() const; bool is_onehot(int *pos = nullptr) const; inline RTLIL::Const extract(int offset, int len = 1, RTLIL::State padding = RTLIL::State::S0) const { diff --git a/kernel/yosys.cc b/kernel/yosys.cc index 333faae6a..bd8dded4b 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -469,8 +469,8 @@ std::string make_temp_dir(std::string template_str) # endif char *p = strdup(template_str.c_str()); - p = mkdtemp(p); - log_assert(p != NULL); + char *res = mkdtemp(p); + log_assert(res != NULL); template_str = p; free(p); diff --git a/kernel/yw.cc b/kernel/yw.cc new file mode 100644 index 000000000..73e7710db --- /dev/null +++ b/kernel/yw.cc @@ -0,0 +1,209 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one> + * + * 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/yw.h" +#include "libs/json11/json11.hpp" + +USING_YOSYS_NAMESPACE + +// Use the same formatting as witness.py uses +static const char *pretty_name(IdString id) +{ + const char *c_str = id.c_str(); + const char *p = c_str; + + if (*p != '\\') + return c_str; + p++; + + if (*p == '[') { + p++; + while (*p >= '0' && *p <= '9') + p++; + if (p[0] != ']' || p[1] != 0) + return c_str; + return c_str + 1; + } + + if (!(*p >= 'a' && *p <= 'z') && !(*p >= 'A' && *p <= 'Z') && *p != '_') + return c_str; + p++; + while ((*p >= '0' && *p <= '9') || (*p >= 'a' && *p <= 'z') || (*p >= 'A' && *p <= 'Z') || *p == '_') + p++; + + if (*p != 0) + return c_str; + return c_str + 1; +} + +std::string IdPath::str() const +{ + std::string result; + + for (auto &item : *this) { + const char *pretty = pretty_name(item); + if (pretty[0] == '[') { + result += pretty; + continue; + } + if (!result.empty()) + result += '.'; + result += pretty; + if (pretty[0] == '\\' || pretty[0] == '$') + result += ' '; + } + + return result; +} + +bool IdPath::get_address(int &addr) const +{ + if (empty()) + return false; + auto &last = back(); + if (!last.begins_with("\\[")) + return false; + if (last == "\\[0]") { + addr = 0; + return true; + } + char first = last.c_str()[2]; + if (first < '1' || first > '9') + return false; + char *endptr; + addr = std::strtol(last.c_str() + 2, &endptr, 10); + return endptr[0] == ']' && endptr[1] == 0; +} + +static std::vector<IdString> get_path(const json11::Json &json) +{ + std::vector<IdString> result; + for (auto &path_item : json.array_items()) { + auto const &path_item_str = path_item.string_value(); + if (path_item_str.empty()) + return {};; + result.push_back(path_item_str); + } + return result; +} + +ReadWitness::ReadWitness(const std::string &filename) : + filename(filename) +{ + std::ifstream f(filename.c_str()); + if (f.fail() || GetSize(filename) == 0) + log_error("Cannot open file `%s`\n", filename.c_str()); + std::stringstream buf; + buf << f.rdbuf(); + std::string err; + json11::Json json = json11::Json::parse(buf.str(), err); + if (!err.empty()) + log_error("Failed to parse `%s`: %s\n", filename.c_str(), err.c_str()); + + std::string format = json["format"].string_value(); + + if (format.empty()) + log_error("Failed to parse `%s`: Unknown format\n", filename.c_str()); + if (format != "Yosys Witness Trace") + log_error("Failed to parse `%s`: Unsupported format `%s`\n", filename.c_str(), format.c_str()); + + for (auto &clock_json : json["clocks"].array_items()) { + Clock clock; + clock.path = get_path(clock_json["path"]); + if (clock.path.empty()) + log_error("Failed to parse `%s`: Missing path for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + auto edge_str = clock_json["edge"]; + if (edge_str.string_value() == "posedge") + clock.is_posedge = true; + else if (edge_str.string_value() == "negedge") + clock.is_negedge = true; + else + log_error("Failed to parse `%s`: Unknown edge type for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + if (!clock_json["offset"].is_number()) + log_error("Failed to parse `%s`: Unknown offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + clock.offset = clock_json["offset"].int_value(); + if (clock.offset < 0) + log_error("Failed to parse `%s`: Invalid offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + clocks.push_back(clock); + } + + int bits_offset = 0; + for (auto &signal_json : json["signals"].array_items()) { + Signal signal; + signal.bits_offset = bits_offset; + signal.path = get_path(signal_json["path"]); + if (signal.path.empty()) + log_error("Failed to parse `%s`: Missing path for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + if (!signal_json["width"].is_number()) + log_error("Failed to parse `%s`: Unknown width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + signal.width = signal_json["width"].int_value(); + if (signal.width < 0) + log_error("Failed to parse `%s`: Invalid width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + bits_offset += signal.width; + if (!signal_json["offset"].is_number()) + log_error("Failed to parse `%s`: Unknown offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + signal.offset = signal_json["offset"].int_value(); + if (signal.offset < 0) + log_error("Failed to parse `%s`: Invalid offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + signal.init_only = signal_json["init_only"].bool_value(); + signals.push_back(signal); + } + + for (auto &step_json : json["steps"].array_items()) { + Step step; + if (!step_json["bits"].is_string()) + log_error("Failed to parse `%s`: Expected string as bits value for step %d\n", filename.c_str(), GetSize(steps)); + step.bits = step_json["bits"].string_value(); + for (char c : step.bits) { + if (c != '0' && c != '1' && c != 'x' && c != '?') + log_error("Failed to parse `%s`: Invalid bit '%c' value for step %d\n", filename.c_str(), c, GetSize(steps)); + } + steps.push_back(step); + } +} + +RTLIL::Const ReadWitness::get_bits(int t, int bits_offset, int width) const +{ + log_assert(t >= 0 && t < GetSize(steps)); + + const std::string &bits = steps[t].bits; + + RTLIL::Const result(State::Sa, width); + result.bits.reserve(width); + + int read_begin = GetSize(bits) - 1 - bits_offset; + int read_end = max(-1, read_begin - width); + + min(width, GetSize(bits) - bits_offset); + + for (int i = read_begin, j = 0; i > read_end; i--, j++) { + RTLIL::State bit = State::Sa; + switch (bits[i]) { + case '0': bit = State::S0; break; + case '1': bit = State::S1; break; + case 'x': bit = State::Sx; break; + case '?': bit = State::Sa; break; + default: + log_abort(); + } + result.bits[j] = bit; + } + + return result; +} diff --git a/kernel/yw.h b/kernel/yw.h new file mode 100644 index 000000000..c2f5921b1 --- /dev/null +++ b/kernel/yw.h @@ -0,0 +1,182 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one> + * + * 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. + * + */ + +#ifndef YW_H +#define YW_H + +#include "kernel/yosys.h" +#include "kernel/mem.h" + +YOSYS_NAMESPACE_BEGIN + +struct IdPath : public std::vector<RTLIL::IdString> +{ + template<typename... T> + IdPath(T&&... args) : std::vector<RTLIL::IdString>(std::forward<T>(args)...) { } + IdPath prefix() const { return {begin(), end() - !empty()}; } + std::string str() const; + + bool has_address() const { int tmp; return get_address(tmp); }; + bool get_address(int &addr) const; + + int hash() const { return hashlib::hash_ops<std::vector<RTLIL::IdString>>::hash(*this); } +}; + +struct WitnessHierarchyItem { + RTLIL::Module *module; + RTLIL::Wire *wire = nullptr; + RTLIL::Cell *cell = nullptr; + Mem *mem = nullptr; + + WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Wire *wire) : module(module), wire(wire) {} + WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Cell *cell) : module(module), cell(cell) {} + WitnessHierarchyItem(RTLIL::Module *module, Mem *mem) : module(module), mem(mem) {} +}; + +template<typename D, typename T> +void witness_hierarchy(RTLIL::Module *module, D data, T callback); + +template<class T> static std::vector<std::string> witness_path(T *obj) { + std::vector<std::string> path; + if (obj->name.isPublic()) { + auto hdlname = obj->get_string_attribute(ID::hdlname); + for (auto token : split_tokens(hdlname)) + path.push_back("\\" + token); + } + if (path.empty()) + path.push_back(obj->name.str()); + return path; +} + +struct ReadWitness +{ + struct Clock { + IdPath path; + int offset; + bool is_posedge = false; + bool is_negedge = false; + }; + + struct Signal { + IdPath path; + int offset; + int width; + bool init_only; + + int bits_offset; + }; + + struct Step { + std::string bits; + }; + + std::string filename; + std::vector<Clock> clocks; + std::vector<Signal> signals; + std::vector<Step> steps; + + ReadWitness(const std::string &filename); + + RTLIL::Const get_bits(int t, int bits_offset, int width) const; +}; + +template<typename D, typename T> +void witness_hierarchy_recursion(IdPath &path, int hdlname_mode, RTLIL::Module *module, D data, T &callback) +{ + auto const &const_path = path; + size_t path_size = path.size(); + for (auto wire : module->wires()) + { + auto hdlname = hdlname_mode < 0 ? std::vector<std::string>() : wire->get_hdlname_attribute(); + for (auto item : hdlname) + path.push_back("\\" + item); + if (hdlname.size() == 1 && path.back() == wire->name) + hdlname.clear(); + if (!hdlname.empty()) + callback(const_path, WitnessHierarchyItem(module, wire), data); + path.resize(path_size); + if (hdlname.empty() || hdlname_mode <= 0) { + path.push_back(wire->name); + callback(const_path, WitnessHierarchyItem(module, wire), data); + path.pop_back(); + } + } + + for (auto cell : module->cells()) + { + Module *child = module->design->module(cell->type); + if (child == nullptr) + continue; + + auto hdlname = hdlname_mode < 0 ? std::vector<std::string>() : cell->get_hdlname_attribute(); + for (auto item : hdlname) + path.push_back("\\" + item); + if (hdlname.size() == 1 && path.back() == cell->name) + hdlname.clear(); + if (!hdlname.empty()) { + D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data); + witness_hierarchy_recursion<D, T>(path, 1, child, child_data, callback); + } + path.resize(path_size); + if (hdlname.empty() || hdlname_mode <= 0) { + path.push_back(cell->name); + D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data); + witness_hierarchy_recursion<D, T>(path, hdlname.empty() ? hdlname_mode : -1, child, child_data, callback); + path.pop_back(); + } + } + + for (auto mem : Mem::get_all_memories(module)) { + std::vector<std::string> hdlname; + + if (hdlname_mode >= 0 && mem.cell != nullptr) + hdlname = mem.cell->get_hdlname_attribute(); + for (auto item : hdlname) + path.push_back("\\" + item); + if (hdlname.size() == 1 && path.back() == mem.cell->name) + hdlname.clear(); + if (!hdlname.empty()) { + callback(const_path, WitnessHierarchyItem(module, &mem), data); + } + path.resize(path_size); + + if (hdlname.empty() || hdlname_mode <= 0) { + path.push_back(mem.memid); + callback(const_path, WitnessHierarchyItem(module, &mem), data); + path.pop_back(); + + if (mem.cell != nullptr && mem.cell->name != mem.memid) { + path.push_back(mem.cell->name); + callback(const_path, WitnessHierarchyItem(module, &mem), data); + path.pop_back(); + } + } + } +} + +template<typename D, typename T> +void witness_hierarchy(RTLIL::Module *module, D data, T callback) +{ + IdPath path; + witness_hierarchy_recursion<D, T>(path, 0, module, data, callback); +} + +YOSYS_NAMESPACE_END + +#endif diff --git a/passes/cmds/bugpoint.cc b/passes/cmds/bugpoint.cc index e666023fa..c398afffa 100644 --- a/passes/cmds/bugpoint.cc +++ b/passes/cmds/bugpoint.cc @@ -393,6 +393,7 @@ struct BugpointPass : public Pass { } } } + delete design_copy; return nullptr; } diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index 66044b161..da97ff71d 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -55,6 +55,14 @@ struct ChformalPass : public Pass { log(" -skip <N>\n"); log(" ignore activation of the constraint in the first <N> clock cycles\n"); log("\n"); + log(" -coverenable\n"); + log(" add cover statements for the enable signals of the constraints\n"); + log("\n"); +#ifdef YOSYS_ENABLE_VERIFIC + log(" Note: For the Verific frontend it is currently not guaranteed that a\n"); + log(" reachable SVA statement corresponds to an active enable signal.\n"); + log("\n"); +#endif log(" -assert2assume\n"); log(" -assume2assert\n"); log(" -live2fair\n"); @@ -114,6 +122,10 @@ struct ChformalPass : public Pass { mode_arg = atoi(args[++argidx].c_str()); continue; } + if (mode == 0 && args[argidx] == "-coverenable") { + mode = 'p'; + continue; + } if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") { assert2assume = true; mode = 'c'; @@ -263,6 +275,13 @@ struct ChformalPass : public Pass { cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN))); } else + if (mode =='p') + { + for (auto cell : constr_cells) + module->addCover(NEW_ID_SUFFIX("coverenable"), + cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); + } + else if (mode == 'c') { for (auto cell : constr_cells) diff --git a/passes/cmds/design.cc b/passes/cmds/design.cc index 169f7cc4a..168d38563 100644 --- a/passes/cmds/design.cc +++ b/passes/cmds/design.cc @@ -118,6 +118,9 @@ struct DesignPass : public Pass { std::string save_name, load_name, as_name, delete_name; std::vector<RTLIL::Module*> copy_src_modules; + if (!design) + log_cmd_error("No default design.\n"); + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -280,7 +283,7 @@ struct DesignPass : public Pass { done[mod->name] = prefix; } - while (!queue.empty()) + while (!queue.empty() && copy_from_design) { pool<Module*> old_queue; old_queue.swap(queue); diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc index 590a7eb1d..7293002f3 100644 --- a/passes/cmds/setundef.cc +++ b/passes/cmds/setundef.cc @@ -502,7 +502,15 @@ struct SetundefPass : public Pass { } } - module->rewrite_sigspecs(worker); + for (auto &it : module->cells_) + if (!it.second->get_bool_attribute(ID::xprop_decoder)) + it.second->rewrite_sigspecs(worker); + for (auto &it : module->processes) + it.second->rewrite_sigspecs(worker); + for (auto &it : module->connections_) { + worker(it.first); + worker(it.second); + } if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) { diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index b186e5db2..dd7de8273 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -233,77 +233,101 @@ struct ShowWorker return std::string(); } + // Return the pieces of a label joined by a '|' separator + std::string join_label_pieces(std::vector<std::string> pieces) + { + std::string ret = ""; + bool first_piece = true; + + for (auto &piece : pieces) { + if (!first_piece) + ret += "|"; + ret += piece; + first_piece = false; + } + + return ret; + } + std::string gen_portbox(std::string port, RTLIL::SigSpec sig, bool driver, std::string *node = nullptr) { std::string code; std::string net = gen_signode_simple(sig); if (net.empty()) { - std::string label_string; - int pos = sig.size()-1; - int idx = single_idx_count++; - for (int rep, i = int(sig.chunks().size())-1; i >= 0; i -= rep) { - const RTLIL::SigChunk &c = sig.chunks().at(i); + int dot_idx = single_idx_count++; + std::vector<std::string> label_pieces; + int bitpos = sig.size()-1; + + for (int rep, chunk_idx = ((int) sig.chunks().size()) - 1; chunk_idx >= 0; chunk_idx -= rep) { + const RTLIL::SigChunk &c = sig.chunks().at(chunk_idx); + + // Find the number of times this chunk is repeating + for (rep = 1; chunk_idx - rep >= 0 && c == sig.chunks().at(chunk_idx - rep); rep++); + int cl, cr; - if (c.wire) { + cl = c.offset + c.width - 1; + cr = c.offset; + + if (c.is_wire()) { if (c.wire->upto) { - cr = c.wire->start_offset + (c.wire->width - c.offset - 1); + cr = (c.wire->width - 1) - c.offset; cl = cr - (c.width - 1); - } else { - cr = c.wire->start_offset + c.offset; - cl = cr + c.width - 1; } - } else { - cl = c.offset + c.width - 1; - cr = c.offset; + + cl += c.wire->start_offset; + cr += c.wire->start_offset; } - if (!driver && c.wire == nullptr) { - RTLIL::State s1 = c.data.front(); - for (auto s2 : c.data) - if (s1 != s2) - goto not_const_stream; - net.clear(); - } else { - not_const_stream: + + // Is this chunk a constant filled with one kind of bit state? + bool no_signode = !driver && !c.is_wire() \ + && std::equal(c.data.begin() + 1, c.data.end(), c.data.begin()); + + if (!no_signode) { net = gen_signode_simple(c, false); log_assert(!net.empty()); } - for (rep = 1; i-rep >= 0 && c == sig.chunks().at(i-rep); rep++) {} + std::string repinfo = rep > 1 ? stringf("%dx ", rep) : ""; + std::string portside = stringf("%d:%d", bitpos, bitpos - rep*c.width + 1); + std::string remoteside = stringf("%s%d:%d", repinfo.c_str(), cl, cr); + if (driver) { log_assert(!net.empty()); - label_string += stringf("<s%d> %d:%d - %s%d:%d |", i, pos, pos-c.width+1, repinfo.c_str(), cl, cr); - net_conn_map[net].in.insert({stringf("x%d:s%d", idx, i), rep*c.width}); + label_pieces.push_back(stringf("<s%d> %s - %s ", chunk_idx, portside.c_str(), remoteside.c_str())); + net_conn_map[net].in.insert({stringf("x%d:s%d", dot_idx, chunk_idx), rep*c.width}); net_conn_map[net].color = nextColor(c, net_conn_map[net].color); - } else - if (net.empty()) { - log_assert(rep == 1); - label_string += stringf("%c -> %d:%d |", - c.data.front() == State::S0 ? '0' : - c.data.front() == State::S1 ? '1' : - c.data.front() == State::Sx ? 'X' : - c.data.front() == State::Sz ? 'Z' : '?', - pos, pos-rep*c.width+1); } else { - label_string += stringf("<s%d> %s%d:%d - %d:%d |", i, repinfo.c_str(), cl, cr, pos, pos-rep*c.width+1); - net_conn_map[net].out.insert({stringf("x%d:s%d", idx, i), rep*c.width}); - net_conn_map[net].color = nextColor(c, net_conn_map[net].color); + if (no_signode) { + log_assert(rep == 1); + label_pieces.push_back(stringf("%c -> %d:%d ", + c.data.front() == State::S0 ? '0' : + c.data.front() == State::S1 ? '1' : + c.data.front() == State::Sx ? 'X' : + c.data.front() == State::Sz ? 'Z' : '?', + bitpos, bitpos-rep*c.width+1)); + } else { + label_pieces.push_back(stringf("<s%d> %s - %s ", chunk_idx, remoteside.c_str(), portside.c_str())); + net_conn_map[net].out.insert({stringf("x%d:s%d", dot_idx, chunk_idx), rep*c.width}); + net_conn_map[net].color = nextColor(c, net_conn_map[net].color); + } } - pos -= rep * c.width; + + bitpos -= rep * c.width; } - if (label_string[label_string.size()-1] == '|') - label_string = label_string.substr(0, label_string.size()-1); - code += stringf("x%d [ shape=record, style=rounded, label=\"%s\" ];\n", idx, label_string.c_str()); + + code += stringf("x%d [ shape=record, style=rounded, label=\"", dot_idx) \ + + join_label_pieces(label_pieces) + "\" ];\n"; + if (!port.empty()) { currentColor = xorshift32(currentColor); - log_warning("WIDTHLABEL %s %d\n", log_signal(sig), GetSize(sig)); if (driver) - code += stringf("%s:e -> x%d:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", port.c_str(), idx, nextColor(sig).c_str(), widthLabel(sig.size()).c_str()); + code += stringf("%s:e -> x%d:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", port.c_str(), dot_idx, nextColor(sig).c_str(), widthLabel(sig.size()).c_str()); else - code += stringf("x%d:e -> %s:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", idx, port.c_str(), nextColor(sig).c_str(), widthLabel(sig.size()).c_str()); + code += stringf("x%d:e -> %s:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, %s, %s];\n", dot_idx, port.c_str(), nextColor(sig).c_str(), widthLabel(sig.size()).c_str()); } if (node != nullptr) - *node = stringf("x%d", idx); + *node = stringf("x%d", dot_idx); } else { @@ -418,6 +442,7 @@ struct ShowWorker for (auto cell : module->selected_cells()) { std::vector<RTLIL::IdString> in_ports, out_ports; + std::vector<std::string> in_label_pieces, out_label_pieces; for (auto &conn : cell->connections()) { if (!ct.cell_output(cell->type, conn.first)) @@ -429,23 +454,23 @@ struct ShowWorker std::sort(in_ports.begin(), in_ports.end(), RTLIL::sort_by_id_str()); std::sort(out_ports.begin(), out_ports.end(), RTLIL::sort_by_id_str()); - std::string label_string = "{{"; + for (auto &p : in_ports) { + bool signed_suffix = genSignedLabels && cell->hasParam(p.str() + "_SIGNED") + && cell->getParam(p.str() + "_SIGNED").as_bool(); - for (auto &p : in_ports) - label_string += stringf("<p%d> %s%s|", id2num(p), escape(p.str()), - genSignedLabels && cell->hasParam(p.str() + "_SIGNED") && - cell->getParam(p.str() + "_SIGNED").as_bool() ? "*" : ""); - if (label_string[label_string.size()-1] == '|') - label_string = label_string.substr(0, label_string.size()-1); - - label_string += stringf("}|%s\\n%s|{", findLabel(cell->name.str()), escape(cell->type.str())); + in_label_pieces.push_back(stringf("<p%d> %s%s", id2num(p), escape(p.str()), + signed_suffix ? "*" : "")); + } for (auto &p : out_ports) - label_string += stringf("<p%d> %s|", id2num(p), escape(p.str())); - if (label_string[label_string.size()-1] == '|') - label_string = label_string.substr(0, label_string.size()-1); + out_label_pieces.push_back(stringf("<p%d> %s", id2num(p), escape(p.str()))); + + std::string in_label = join_label_pieces(in_label_pieces); + std::string out_label = join_label_pieces(out_label_pieces); - label_string += "}}"; + std::string label_string = stringf("{{%s}|%s\\n%s|{%s}}", in_label.c_str(), + findLabel(cell->name.str()), escape(cell->type.str()), + out_label.c_str()); std::string code; for (auto &conn : cell->connections()) { diff --git a/passes/cmds/splitcells.cc b/passes/cmds/splitcells.cc index de6df6142..82ed49074 100644 --- a/passes/cmds/splitcells.cc +++ b/passes/cmds/splitcells.cc @@ -68,70 +68,132 @@ struct SplitcellsWorker int split(Cell *cell, const std::string &format) { - if (!cell->type.in("$and", "$mux", "$not", "$or", "$pmux", "$xnor", "$xor")) return 0; + if (cell->type.in("$and", "$mux", "$not", "$or", "$pmux", "$xnor", "$xor")) + { + SigSpec outsig = sigmap(cell->getPort(ID::Y)); + if (GetSize(outsig) <= 1) return 0; + + std::vector<int> slices; + slices.push_back(0); + + int width = GetSize(outsig); + width = std::min(width, GetSize(cell->getPort(ID::A))); + if (cell->hasPort(ID::B)) + width = std::min(width, GetSize(cell->getPort(ID::B))); + + for (int i = 1; i < width; i++) { + auto &last_users = bit_users_db[outsig[slices.back()]]; + auto &this_users = bit_users_db[outsig[i]]; + if (last_users != this_users) slices.push_back(i); + } + if (GetSize(slices) <= 1) return 0; + slices.push_back(GetSize(outsig)); + + log("Splitting %s cell %s/%s into %d slices:\n", log_id(cell->type), log_id(module), log_id(cell), GetSize(slices)-1); + for (int i = 1; i < GetSize(slices); i++) + { + int slice_msb = slices[i]-1; + int slice_lsb = slices[i-1]; - SigSpec outsig = sigmap(cell->getPort(ID::Y)); - if (GetSize(outsig) <= 1) return 0; + IdString slice_name = module->uniquify(cell->name.str() + (slice_msb == slice_lsb ? + stringf("%c%d%c", format[0], slice_lsb, format[1]) : + stringf("%c%d%c%d%c", format[0], slice_msb, format[2], slice_lsb, format[1]))); + + Cell *slice = module->addCell(slice_name, cell); + + auto slice_signal = [&](SigSpec old_sig) -> SigSpec { + SigSpec new_sig; + for (int i = 0; i < GetSize(old_sig); i += GetSize(outsig)) { + int offset = i+slice_lsb; + int length = std::min(GetSize(old_sig)-offset, slice_msb-slice_lsb+1); + new_sig.append(old_sig.extract(offset, length)); + } + return new_sig; + }; + + slice->setPort(ID::A, slice_signal(slice->getPort(ID::A))); + if (slice->hasParam(ID::A_WIDTH)) + slice->setParam(ID::A_WIDTH, GetSize(slice->getPort(ID::A))); + + if (slice->hasPort(ID::B)) { + slice->setPort(ID::B, slice_signal(slice->getPort(ID::B))); + if (slice->hasParam(ID::B_WIDTH)) + slice->setParam(ID::B_WIDTH, GetSize(slice->getPort(ID::B))); + } - std::vector<int> slices; - slices.push_back(0); + slice->setPort(ID::Y, slice_signal(slice->getPort(ID::Y))); + if (slice->hasParam(ID::Y_WIDTH)) + slice->setParam(ID::Y_WIDTH, GetSize(slice->getPort(ID::Y))); + if (slice->hasParam(ID::WIDTH)) + slice->setParam(ID::WIDTH, GetSize(slice->getPort(ID::Y))); - int width = GetSize(outsig); - width = std::min(width, GetSize(cell->getPort(ID::A))); - if (cell->hasPort(ID::B)) - width = std::min(width, GetSize(cell->getPort(ID::B))); + log(" slice %d: %s => %s\n", i, log_id(slice_name), log_signal(slice->getPort(ID::Y))); + } - for (int i = 1; i < width; i++) { - auto &last_users = bit_users_db[outsig[slices.back()]]; - auto &this_users = bit_users_db[outsig[i]]; - if (last_users != this_users) slices.push_back(i); + module->remove(cell); + return GetSize(slices)-1; } - if (GetSize(slices) <= 1) return 0; - slices.push_back(GetSize(outsig)); - log("Splitting %s cell %s/%s into %d slices:\n", log_id(cell->type), log_id(module), log_id(cell), GetSize(slices)-1); - for (int i = 1; i < GetSize(slices); i++) + if (cell->type.in("$ff", "$dff", "$dffe", "$dffsr", "$dffsre", "$adff", "$adffe", "$aldffe", + "$sdff", "$sdffce", "$sdffe", "$dlatch", "$dlatchsr", "$adlatch")) { - int slice_msb = slices[i]-1; - int slice_lsb = slices[i-1]; + auto splitports = {ID::D, ID::Q, ID::AD, ID::SET, ID::CLR}; + auto splitparams = {ID::ARST_VALUE, ID::SRST_VALUE}; + + SigSpec outsig = sigmap(cell->getPort(ID::Q)); + if (GetSize(outsig) <= 1) return 0; + int width = GetSize(outsig); + + std::vector<int> slices; + slices.push_back(0); + + for (int i = 1; i < width; i++) { + auto &last_users = bit_users_db[outsig[slices.back()]]; + auto &this_users = bit_users_db[outsig[i]]; + if (last_users != this_users) slices.push_back(i); + } + + if (GetSize(slices) <= 1) return 0; + slices.push_back(GetSize(outsig)); - IdString slice_name = module->uniquify(cell->name.str() + (slice_msb == slice_lsb ? - stringf("%c%d%c", format[0], slice_lsb, format[1]) : - stringf("%c%d%c%d%c", format[0], slice_msb, format[2], slice_lsb, format[1]))); + log("Splitting %s cell %s/%s into %d slices:\n", log_id(cell->type), log_id(module), log_id(cell), GetSize(slices)-1); + for (int i = 1; i < GetSize(slices); i++) + { + int slice_msb = slices[i]-1; + int slice_lsb = slices[i-1]; - Cell *slice = module->addCell(slice_name, cell); + IdString slice_name = module->uniquify(cell->name.str() + (slice_msb == slice_lsb ? + stringf("%c%d%c", format[0], slice_lsb, format[1]) : + stringf("%c%d%c%d%c", format[0], slice_msb, format[2], slice_lsb, format[1]))); - auto slice_signal = [&](SigSpec old_sig) -> SigSpec { - SigSpec new_sig; - for (int i = 0; i < GetSize(old_sig); i += GetSize(outsig)) { - int offset = i+slice_lsb; - int length = std::min(GetSize(old_sig)-offset, slice_msb-slice_lsb+1); - new_sig.append(old_sig.extract(offset, length)); + Cell *slice = module->addCell(slice_name, cell); + + for (IdString portname : splitports) { + if (slice->hasPort(portname)) { + SigSpec sig = slice->getPort(portname); + sig = sig.extract(slice_lsb, slice_msb-slice_lsb+1); + slice->setPort(portname, sig); + } } - return new_sig; - }; - slice->setPort(ID::A, slice_signal(slice->getPort(ID::A))); - if (slice->hasParam(ID::A_WIDTH)) - slice->setParam(ID::A_WIDTH, GetSize(slice->getPort(ID::A))); + for (IdString paramname : splitparams) { + if (slice->hasParam(paramname)) { + Const val = slice->getParam(paramname); + val = val.extract(slice_lsb, slice_msb-slice_lsb+1); + slice->setParam(paramname, val); + } + } - if (slice->hasPort(ID::B)) { - slice->setPort(ID::B, slice_signal(slice->getPort(ID::B))); - if (slice->hasParam(ID::B_WIDTH)) - slice->setParam(ID::B_WIDTH, GetSize(slice->getPort(ID::B))); - } + slice->setParam(ID::WIDTH, GetSize(slice->getPort(ID::Q))); - slice->setPort(ID::Y, slice_signal(slice->getPort(ID::Y))); - if (slice->hasParam(ID::Y_WIDTH)) - slice->setParam(ID::Y_WIDTH, GetSize(slice->getPort(ID::Y))); - if (slice->hasParam(ID::WIDTH)) - slice->setParam(ID::WIDTH, GetSize(slice->getPort(ID::Y))); + log(" slice %d: %s => %s\n", i, log_id(slice_name), log_signal(slice->getPort(ID::Q))); + } - log(" slice %d: %s => %s\n", i, log_id(slice_name), log_signal(slice->getPort(ID::Y))); + module->remove(cell); + return GetSize(slices)-1; } - module->remove(cell); - return GetSize(slices)-1; + return 0; } }; @@ -179,14 +241,20 @@ struct SplitcellsPass : public Pass { for (auto module : design->selected_modules()) { - SplitcellsWorker worker(module); int count_split_pre = 0; int count_split_post = 0; - for (auto cell : module->selected_cells()) { - int n = worker.split(cell, format); - count_split_pre += (n != 0); - count_split_post += n; + while (1) { + SplitcellsWorker worker(module); + bool did_something = false; + for (auto cell : module->selected_cells()) { + int n = worker.split(cell, format); + did_something |= (n != 0); + count_split_pre += (n != 0); + count_split_post += n; + } + if (!did_something) + break; } if (count_split_pre) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index 10e98952e..522957f39 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -275,6 +275,9 @@ struct statdata_t log(" \"num_memory_bits\": %u,\n", num_memory_bits); log(" \"num_processes\": %u,\n", num_processes); log(" \"num_cells\": %u,\n", num_cells); + if (area != 0) { + log(" \"area\": %f,\n", area); + } log(" \"num_cells_by_type\": {\n"); bool first_line = true; for (auto &it : num_cells_by_type) diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc index 5dee72e1b..5e78ff9fc 100644 --- a/passes/cmds/xprop.cc +++ b/passes/cmds/xprop.cc @@ -252,7 +252,8 @@ struct XpropWorker } if (!driven_orig.empty()) { - module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig); + auto decoder = module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig); + decoder->set_bool_attribute(ID::xprop_decoder); } if (!driven_never_x.first.empty()) { module->connect(driven_never_x); diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 27cec7549..e15e510be 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -33,6 +33,7 @@ struct EquivMakeWorker bool inames; vector<string> blacklists; vector<string> encfiles; + bool make_assert; pool<IdString> blacklist_names; dict<IdString, dict<Const, Const>> encdata; @@ -133,6 +134,12 @@ struct EquivMakeWorker delete gate_clone; } + void add_eq_assertion(const SigSpec &gold_sig, const SigSpec &gate_sig) + { + auto eq_wire = equiv_mod->Eqx(NEW_ID, gold_sig, gate_sig); + equiv_mod->addAssert(NEW_ID_SUFFIX("assert"), eq_wire, State::S1); + } + void find_same_wires() { SigMap assign_map(equiv_mod); @@ -231,15 +238,24 @@ struct EquivMakeWorker if (gold_wire->port_output || gate_wire->port_output) { - Wire *wire = equiv_mod->addWire(id, gold_wire->width); - wire->port_output = true; gold_wire->port_input = false; gate_wire->port_input = false; gold_wire->port_output = false; gate_wire->port_output = false; - for (int i = 0; i < wire->width; i++) - equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + wire->port_output = true; + + if (make_assert) + { + add_eq_assertion(gold_wire, gate_wire); + equiv_mod->connect(wire, gold_wire); + } + else + { + for (int i = 0; i < wire->width; i++) + equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + } rd_signal_map.add(assign_map(gold_wire), wire); rd_signal_map.add(assign_map(gate_wire), wire); @@ -259,26 +275,31 @@ struct EquivMakeWorker } else { - Wire *wire = equiv_mod->addWire(id, gold_wire->width); - SigSpec rdmap_gold, rdmap_gate, rdmap_equiv; + if (make_assert) + add_eq_assertion(gold_wire, gate_wire); - for (int i = 0; i < wire->width; i++) { - if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) { - log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i); - continue; - } - if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) { - log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i); - continue; + else { + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + SigSpec rdmap_gold, rdmap_gate, rdmap_equiv; + + for (int i = 0; i < wire->width; i++) { + if (undriven_bits.count(assign_map(SigBit(gold_wire, i)))) { + log(" Skipping signal bit %s [%d]: undriven on gold side.\n", id2cstr(gold_wire->name), i); + continue; + } + if (undriven_bits.count(assign_map(SigBit(gate_wire, i)))) { + log(" Skipping signal bit %s [%d]: undriven on gate side.\n", id2cstr(gate_wire->name), i); + continue; + } + equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + rdmap_gold.append(SigBit(gold_wire, i)); + rdmap_gate.append(SigBit(gate_wire, i)); + rdmap_equiv.append(SigBit(wire, i)); } - equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); - rdmap_gold.append(SigBit(gold_wire, i)); - rdmap_gate.append(SigBit(gate_wire, i)); - rdmap_equiv.append(SigBit(wire, i)); - } - rd_signal_map.add(rdmap_gold, rdmap_equiv); - rd_signal_map.add(rdmap_gate, rdmap_equiv); + rd_signal_map.add(rdmap_gold, rdmap_equiv); + rd_signal_map.add(rdmap_gate, rdmap_equiv); + } } } @@ -335,12 +356,20 @@ struct EquivMakeWorker continue; } - for (int i = 0; i < GetSize(gold_sig); i++) - if (gold_sig[i] != gate_sig[i]) { - Wire *w = equiv_mod->addWire(NEW_ID); - equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w); - gold_sig[i] = w; - } + if (make_assert) + { + if (gold_sig != gate_sig) + add_eq_assertion(gold_sig, gate_sig); + } + else + { + for (int i = 0; i < GetSize(gold_sig); i++) + if (gold_sig[i] != gate_sig[i]) { + Wire *w = equiv_mod->addWire(NEW_ID); + equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w); + gold_sig[i] = w; + } + } gold_cell->setPort(gold_conn.first, gold_sig); } @@ -417,6 +446,10 @@ struct EquivMakePass : public Pass { log(" Match FSM encodings using the description from the file.\n"); log(" See 'help fsm_recode' for details.\n"); log("\n"); + log(" -make_assert\n"); + log(" Check equivalence with $assert cells instead of $equiv.\n"); + log(" $eqx (===) is used to compare signals."); + log("\n"); log("Note: The circuit created by this command is not a miter (with something like\n"); log("a trigger output), but instead uses $equiv cells to encode the equivalence\n"); log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n"); @@ -427,6 +460,7 @@ struct EquivMakePass : public Pass { EquivMakeWorker worker; worker.ct.setup(design); worker.inames = false; + worker.make_assert = false; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) @@ -443,6 +477,10 @@ struct EquivMakePass : public Pass { worker.encfiles.push_back(args[++argidx]); continue; } + if (args[argidx] == "-make_assert") { + worker.make_assert = true; + continue; + } break; } diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc index 5378ec89e..86d654cc4 100644 --- a/passes/fsm/fsm_detect.cc +++ b/passes/fsm/fsm_detect.cc @@ -118,7 +118,7 @@ static bool check_state_users(RTLIL::SigSpec sig) return true; } -static void detect_fsm(RTLIL::Wire *wire) +static void detect_fsm(RTLIL::Wire *wire, bool ignore_self_reset=false) { bool has_fsm_encoding_attr = wire->attributes.count(ID::fsm_encoding) > 0 && wire->attributes.at(ID::fsm_encoding).decode_string() != "none"; bool has_fsm_encoding_none = wire->attributes.count(ID::fsm_encoding) > 0 && wire->attributes.at(ID::fsm_encoding).decode_string() == "none"; @@ -199,7 +199,7 @@ static void detect_fsm(RTLIL::Wire *wire) } SigSpec sig_y = sig_d, sig_undef; - if (ce.eval(sig_y, sig_undef)) + if (!ignore_self_reset && ce.eval(sig_y, sig_undef)) is_self_resetting = true; } @@ -261,12 +261,15 @@ struct FsmDetectPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" fsm_detect [selection]\n"); + log(" fsm_detect [options] [selection]\n"); log("\n"); log("This pass detects finite state machines by identifying the state signal.\n"); log("The state signal is then marked by setting the attribute 'fsm_encoding'\n"); log("on the state signal to \"auto\".\n"); log("\n"); + log(" -ignore-self-reset\n"); + log(" Mark FSMs even if they are self-resetting\n"); + log("\n"); log("Existing 'fsm_encoding' attributes are not changed by this pass.\n"); log("\n"); log("Signals can be protected from being detected by this pass by setting the\n"); @@ -276,16 +279,28 @@ struct FsmDetectPass : public Pass { log("before this pass to prepare the design for fsm_detect.\n"); log("\n"); #ifdef YOSYS_ENABLE_VERIFIC - log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n"); + log("The Verific frontend may optimize the design in a way that interferes with FSM\n"); log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n"); - log("reading the source, and 'bmuxmap' after 'proc' for best results.\n"); + log("reading the source, and 'bmuxmap -pmux' after 'proc' for best results.\n"); log("\n"); #endif } void execute(std::vector<std::string> args, RTLIL::Design *design) override { log_header(design, "Executing FSM_DETECT pass (finding FSMs in design).\n"); - extra_args(args, 1, design); + + bool ignore_self_reset = false; + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-ignore-self-reset") { + ignore_self_reset = true; + continue; + } + break; + } + extra_args(args, argidx, design); CellTypes ct; ct.setup_internals(); @@ -321,7 +336,7 @@ struct FsmDetectPass : public Pass { sig_at_port.add(assign_map(wire)); for (auto wire : module->selected_wires()) - detect_fsm(wire); + detect_fsm(wire, ignore_self_reset); } assign_map.clear(); diff --git a/passes/opt/opt_ffinv.cc b/passes/opt/opt_ffinv.cc index 5d989dafd..3f7b4bc4a 100644 --- a/passes/opt/opt_ffinv.cc +++ b/passes/opt/opt_ffinv.cc @@ -64,6 +64,7 @@ struct OptFfInvWorker log_assert(d_inv == nullptr); d_inv = port.cell; } + if (!d_inv) return false; if (index.query_is_output(ff.sig_q)) return false; @@ -140,6 +141,7 @@ struct OptFfInvWorker log_assert(d_lut == nullptr); d_lut = port.cell; } + if (!d_lut) return false; if (index.query_is_output(ff.sig_q)) return false; @@ -167,6 +169,7 @@ struct OptFfInvWorker log_assert(q_inv == nullptr); q_inv = port.cell; } + if (!q_inv) return false; ff.flip_rst_bits({0}); ff.sig_q = q_inv->getPort(ID::Y); diff --git a/passes/proc/proc_dff.cc b/passes/proc/proc_dff.cc index 234671df5..fd56786f2 100644 --- a/passes/proc/proc_dff.cc +++ b/passes/proc/proc_dff.cc @@ -302,7 +302,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce) ce.assign_map.apply(rstval); ce.assign_map.apply(sig); - if (rstval == sig) { + if (rstval == sig && sync_level) { if (sync_level->type == RTLIL::SyncType::ST1) insig = mod->Mux(NEW_ID, insig, sig, sync_level->signal); else diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index e36379096..264a9fb3b 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -317,6 +317,172 @@ struct InitValWorker } }; +struct ReplacedPort { + IdString name; + int offset; + bool clk_pol; +}; + +struct HierarchyWorker +{ + Design *design; + pool<Module *> pending; + + dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs; + + HierarchyWorker(Design *design) : + design(design) + { + for (auto module : design->modules()) + pending.insert(module); + } + + void propagate(); + + const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type); +}; + +// Propagates replaced clock signals +struct PropagateWorker +{ + HierarchyWorker &hierarchy; + + Module *module; + SigMap sigmap; + + dict<SigBit, bool> replaced_clk_bits; + dict<SigBit, SigBit> not_drivers; + + std::vector<ReplacedPort> replaced_clk_inputs; + std::vector<std::pair<SigBit, bool>> pending; + + PropagateWorker(Module *module, HierarchyWorker &hierarchy) : + hierarchy(hierarchy), module(module), sigmap(module) + { + hierarchy.pending.erase(module); + + for (auto wire : module->wires()) + if (wire->has_attribute(ID::replaced_by_gclk)) + replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false); + + for (auto cell : module->cells()) { + if (cell->type.in(ID($not), ID($_NOT_))) { + auto sig_a = cell->getPort(ID::A); + auto &sig_y = cell->getPort(ID::Y); + sig_a.extend_u0(GetSize(sig_y), cell->hasParam(ID::A_SIGNED) && cell->parameters.at(ID::A_SIGNED).as_bool()); + + for (int i = 0; i < GetSize(sig_a); i++) + if (sig_a[i].is_wire()) + not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i])); + } else { + for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type)) + replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true); + } + } + + while (!pending.empty()) { + auto current = pending.back(); + pending.pop_back(); + auto it = not_drivers.find(current.first); + if (it == not_drivers.end()) + continue; + + replace_clk_bit(it->second, !current.second, true); + } + + for (auto cell : module->cells()) { + if (cell->type.in(ID($not), ID($_NOT_))) + continue; + for (auto &conn : cell->connections()) { + if (!cell->output(conn.first)) + continue; + for (SigBit bit : conn.second) { + sigmap.apply(bit); + if (replaced_clk_bits.count(bit)) + log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n", + log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module)); + } + } + } + + for (auto port : module->ports) { + auto wire = module->wire(port); + if (!wire->port_input) + continue; + for (int i = 0; i < GetSize(wire); i++) { + SigBit bit(wire, i); + sigmap.apply(bit); + auto it = replaced_clk_bits.find(bit); + if (it == replaced_clk_bits.end()) + continue; + replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second}); + + if (it->second) { + bit = module->Not(NEW_ID, bit); + } + } + } + } + + void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute) + { + sigmap.apply(bit); + if (!bit.is_wire()) + log_error("XXX todo\n"); + + auto it = replaced_clk_bits.find(bit); + if (it != replaced_clk_bits.end()) { + if (it->second != polarity) + log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n", + log_signal(bit), log_id(module)); + return; + } + + replaced_clk_bits.emplace(bit, polarity); + + if (add_attribute) { + Wire *clk_wire = bit.wire; + if (bit.offset != 0 || GetSize(bit.wire) != 1) { + clk_wire = module->addWire(NEW_ID); + module->connect(RTLIL::SigBit(clk_wire), bit); + } + clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0; + clk_wire->set_bool_attribute(ID::keep); + } + + pending.emplace_back(bit, polarity); + } +}; + +const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type) +{ + static const std::vector<ReplacedPort> empty; + if (!cell_type.isPublic()) + return empty; + + Module *module = design->module(cell_type); + if (module == nullptr) + return empty; + + auto it = replaced_clk_inputs.find(module); + if (it != replaced_clk_inputs.end()) + return it->second; + + if (pending.count(module)) { + PropagateWorker worker(module, *this); + return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second; + } + + return empty; +} + + +void HierarchyWorker::propagate() +{ + while (!pending.empty()) + PropagateWorker worker(pending.pop(), *this); +} + struct FormalFfPass : public Pass { FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } void help() override @@ -362,6 +528,15 @@ struct FormalFfPass : public Pass { log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n"); log(" cells that drive wires with private names.\n"); log("\n"); + log(" -hierarchy\n"); + log(" Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n"); + log(" through the design hierarchy towards the toplevel inputs. This option\n"); + log(" works on the whole design and ignores the selection.\n"); + log("\n"); + log(" -assume\n"); + log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n"); + log(" attribute to the value they would have before an active clock edge.\n"); + log("\n"); // TODO: An option to check whether all FFs use the same clock before changing it to the global clock } @@ -372,6 +547,8 @@ struct FormalFfPass : public Pass { bool flag_anyinit2ff = false; bool flag_fine = false; bool flag_setundef = false; + bool flag_hierarchy = false; + bool flag_assume = false; log_header(design, "Executing FORMALFF pass.\n"); @@ -398,12 +575,20 @@ struct FormalFfPass : public Pass { flag_setundef = true; continue; } + if (args[argidx] == "-hierarchy") { + flag_hierarchy = true; + continue; + } + if (args[argidx] == "-assume") { + flag_assume = true; + continue; + } break; } extra_args(args, argidx, design); - if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff)) - log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n"); + if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume)) + log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n"); if (flag_ff2anyinit && flag_anyinit2ff) log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n"); @@ -548,6 +733,33 @@ struct FormalFfPass : public Pass { ff.emit(); } } + + if (flag_hierarchy) { + HierarchyWorker worker(design); + worker.propagate(); + } + + if (flag_assume) { + for (auto module : design->selected_modules()) { + std::vector<pair<SigBit, bool>> found; + for (auto wire : module->wires()) { + if (!wire->has_attribute(ID::replaced_by_gclk)) + continue; + bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1; + + found.emplace_back(SigSpec(wire), clk_pol); + } + for (auto pair : found) { + SigBit clk = pair.first; + + if (pair.second) + clk = module->Not(NEW_ID, clk); + + module->addAssume(NEW_ID, clk, State::S1); + + } + } + } } } FormalFfPass; diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 0084a1f28..7c209f516 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -23,6 +23,8 @@ #include "kernel/mem.h" #include "kernel/fstdata.h" #include "kernel/ff.h" +#include "kernel/yw.h" +#include "kernel/json.h" #include <ctime> @@ -74,6 +76,17 @@ struct OutputWriter SimWorker *worker; }; +struct SimInstance; +struct TriggeredAssertion { + int step; + SimInstance *instance; + Cell *cell; + + TriggeredAssertion(int step, SimInstance *instance, Cell *cell) : + step(step), instance(instance), cell(cell) + { } +}; + struct SimShared { bool debug = false; @@ -93,6 +106,9 @@ struct SimShared bool ignore_x = false; bool date = false; bool multiclock = false; + int next_output_id = 0; + int step = 0; + std::vector<TriggeredAssertion> triggered_assertions; }; void zinit(State &v) @@ -123,6 +139,8 @@ struct SimInstance dict<SigBit, pool<Cell*>> upd_cells; dict<SigBit, pool<Wire*>> upd_outports; + dict<SigBit, SigBit> in_parent_drivers; + pool<SigBit> dirty_bits; pool<Cell*> dirty_cells; pool<IdString> dirty_memories; @@ -152,11 +170,14 @@ struct SimInstance dict<Cell*, ff_state_t> ff_database; dict<IdString, mem_state_t> mem_database; pool<Cell*> formal_database; + pool<Cell*> initstate_database; dict<Cell*, IdString> mem_cells; std::vector<Mem> memories; dict<Wire*, pair<int, Const>> signal_database; + dict<IdString, std::map<int, pair<int, Const>>> trace_mem_database; + dict<std::pair<IdString, int>, Const> trace_mem_init_database; dict<Wire*, fstHandle> fst_handles; dict<Wire*, fstHandle> fst_inputs; dict<IdString, dict<int,fstHandle>> fst_memories; @@ -199,6 +220,12 @@ struct SimInstance dirty_bits.insert(sig[i]); } } + + if (wire->port_input && instance != nullptr && parent != nullptr) { + for (int i = 0; i < GetSize(sig); i++) { + in_parent_drivers.emplace(sig[i], parent->sigmap(instance->getPort(wire->name)[i])); + } + } } memories = Mem::get_all_memories(module); @@ -254,6 +281,8 @@ struct SimInstance if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); } + if (cell->type == ID($initstate)) + initstate_database.insert(cell); } if (shared->zinit) @@ -300,6 +329,21 @@ struct SimInstance return log_id(module->name); } + vector<std::string> witness_full_path() const + { + if (instance != nullptr) + return parent->witness_full_path(instance); + return vector<std::string>(); + } + + vector<std::string> witness_full_path(Cell *cell) const + { + auto result = witness_full_path(); + auto cell_path = witness_path(cell); + result.insert(result.end(), cell_path.begin(), cell_path.end()); + return result; + } + Const get_state(SigSpec sig) { Const value; @@ -325,7 +369,7 @@ struct SimInstance log_assert(GetSize(sig) <= GetSize(value)); for (int i = 0; i < GetSize(sig); i++) - if (state_nets.at(sig[i]) != value[i]) { + if (value[i] != State::Sa && state_nets.at(sig[i]) != value[i]) { state_nets.at(sig[i]) = value[i]; dirty_bits.insert(sig[i]); did_something = true; @@ -336,14 +380,41 @@ struct SimInstance return did_something; } + void set_state_parent_drivers(SigSpec sig, Const value) + { + sigmap.apply(sig); + + for (int i = 0; i < GetSize(sig); i++) { + auto sigbit = sig[i]; + auto sigval = value[i]; + + auto in_parent_driver = in_parent_drivers.find(sigbit); + if (in_parent_driver == in_parent_drivers.end()) + set_state(sigbit, sigval); + else + parent->set_state_parent_drivers(in_parent_driver->second, sigval); + } + } + void set_memory_state(IdString memid, Const addr, Const data) { + set_memory_state(memid, addr.as_int(), data); + } + + void set_memory_state(IdString memid, int addr, Const data) + { auto &state = mem_database[memid]; - int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width; + bool dirty = false; + + int offset = (addr - state.mem->start_offset) * state.mem->width; for (int i = 0; i < GetSize(data); i++) - if (0 <= i+offset && i+offset < state.mem->size * state.mem->width) - state.data.bits[i+offset] = data.bits[i]; + if (0 <= i+offset && i+offset < state.mem->size * state.mem->width && data.bits[i] != State::Sa) + if (state.data.bits[i+offset] != data.bits[i]) + dirty = true, state.data.bits[i+offset] = data.bits[i]; + + if (dirty) + dirty_memories.insert(memid); } void set_memory_state_bit(IdString memid, int offset, State data) @@ -351,7 +422,10 @@ struct SimInstance auto &state = mem_database[memid]; if (offset >= state.mem->size * state.mem->width) log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid)); - state.data.bits[offset] = data; + if (state.data.bits[offset] != data) { + state.data.bits[offset] = data; + dirty_memories.insert(memid); + } } void update_cell(Cell *cell) @@ -447,9 +521,14 @@ struct SimInstance log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid)); if (addr.is_fully_def()) { - int index = addr.as_int() - mem.start_offset; + int addr_int = addr.as_int(); + int index = addr_int - mem.start_offset; if (index >= 0 && index < mem.size) data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2); + + for (int offset = 0; offset < 1 << port.wide_log2; offset++) { + register_memory_addr(id, addr_int + offset); + } } set_state(port.data, data); @@ -604,7 +683,8 @@ struct SimInstance if (addr.is_fully_def()) { - int index = addr.as_int() - mem.start_offset; + int addr_int = addr.as_int(); + int index = addr_int - mem.start_offset; if (index >= 0 && index < mem.size) for (int i = 0; i < (mem.width << port.wide_log2); i++) if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) { @@ -612,6 +692,9 @@ struct SimInstance dirty_memories.insert(mem.memid); did_something = true; } + + for (int i = 0; i < 1 << port.wide_log2; i++) + register_memory_addr(it.first, addr_int + i); } } } @@ -625,7 +708,7 @@ struct SimInstance return did_something; } - void update_ph3() + void update_ph3(bool check_assertions) { for (auto &it : ff_database) { @@ -660,27 +743,42 @@ struct SimInstance } } - for (auto cell : formal_database) + if (check_assertions) { - string label = log_id(cell); - if (cell->attributes.count(ID::src)) - label = cell->attributes.at(ID::src).decode_string(); + for (auto cell : formal_database) + { + string label = log_id(cell); + if (cell->attributes.count(ID::src)) + label = cell->attributes.at(ID::src).decode_string(); + + State a = get_state(cell->getPort(ID::A))[0]; + State en = get_state(cell->getPort(ID::EN))[0]; - State a = get_state(cell->getPort(ID::A))[0]; - State en = get_state(cell->getPort(ID::EN))[0]; + if (en == State::S1 && (cell->type == ID($cover) ? a == State::S1 : a != State::S1)) { + shared->triggered_assertions.emplace_back(shared->step, this, cell); + } - if (cell->type == ID($cover) && en == State::S1 && a != State::S1) - log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($cover) && en == State::S1 && a == State::S1) + log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assume) && en == State::S1 && a != State::S1) - log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assume) && en == State::S1 && a != State::S1) + log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assert) && en == State::S1 && a != State::S1) - log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assert) && en == State::S1 && a != State::S1) + log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + } } for (auto it : children) - it.second->update_ph3(); + it.second->update_ph3(check_assertions); + } + + void set_initstate_outputs(State state) + { + for (auto cell : initstate_database) + set_state(cell->getPort(ID::Y), state); + for (auto child : children) + child.second->set_initstate_outputs(state); } void writeback(pool<Module*> &wbmods) @@ -741,7 +839,7 @@ struct SimInstance child.second->register_signals(id); } - void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, Wire*, int, bool)> register_signal) + void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, int, Wire*, int, bool)> register_signal) { int exit_scopes = 1; if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) { @@ -774,11 +872,45 @@ struct SimInstance hdlname.pop_back(); for (auto name : hdlname) enter_scope("\\" + name); - register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0); + register_signal(signal_name.c_str(), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0); for (auto name : hdlname) exit_scope(); } else - register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0); + register_signal(log_id(signal.first->name), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0); + } + + for (auto &trace_mem : trace_mem_database) + { + auto memid = trace_mem.first; + auto &mdb = mem_database.at(memid); + Cell *cell = mdb.mem->cell; + + std::vector<std::string> hdlname; + std::string signal_name; + bool has_hdlname = shared->hdlname && cell != nullptr && cell->name.isPublic() && cell->has_attribute(ID::hdlname); + + if (has_hdlname) { + hdlname = cell->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + signal_name = std::move(hdlname.back()); + hdlname.pop_back(); + for (auto name : hdlname) + enter_scope("\\" + name); + } else { + signal_name = log_id(memid); + } + + for (auto &trace_index : trace_mem.second) { + int output_id = trace_index.second.first; + int index = trace_index.first; + register_signal( + stringf("%s[%d]", signal_name.c_str(), (index + mdb.mem->start_offset)).c_str(), + mdb.mem->width, nullptr, output_id, true); + } + + if (has_hdlname) + for (auto name : hdlname) + exit_scope(); } for (auto child : children) @@ -788,6 +920,30 @@ struct SimInstance exit_scope(); } + void register_memory_addr(IdString memid, int addr) + { + auto &mdb = mem_database.at(memid); + auto &mem = *mdb.mem; + int index = addr - mem.start_offset; + if (index < 0 || index >= mem.size) + return; + auto it = trace_mem_database.find(memid); + if (it != trace_mem_database.end() && it->second.count(index)) + return; + int output_id = shared->next_output_id++; + Const data; + if (!shared->output_data.empty()) { + auto init_it = trace_mem_init_database.find(std::make_pair(memid, addr)); + if (init_it != trace_mem_init_database.end()) + data = init_it->second; + else + data = mem.get_init_data().extract(index * mem.width, mem.width); + shared->output_data.front().second.emplace(output_id, data); + } + trace_mem_database[memid].emplace(index, make_pair(output_id, data)); + + } + void register_output_step_values(std::map<int,Const> *data) { for (auto &it : signal_database) @@ -803,6 +959,26 @@ struct SimInstance data->emplace(id, value); } + for (auto &trace_mem : trace_mem_database) + { + auto memid = trace_mem.first; + auto &mdb = mem_database.at(memid); + auto &mem = *mdb.mem; + for (auto &trace_index : trace_mem.second) + { + int output_id = trace_index.second.first; + int index = trace_index.first; + + auto value = mdb.data.extract(index * mem.width, mem.width); + + if (trace_index.second.second == value) + continue; + + trace_index.second.second = value; + data->emplace(output_id, value); + } + } + for (auto child : children) child.second->register_output_step_values(data); } @@ -946,6 +1122,7 @@ struct SimWorker : SimShared std::string timescale; std::string sim_filename; std::string map_filename; + std::string summary_filename; std::string scope; ~SimWorker() @@ -956,8 +1133,8 @@ struct SimWorker : SimShared void register_signals() { - int id = 1; - top->register_signals(id); + next_output_id = 1; + top->register_signals(top->shared->next_output_id); } void register_output_step(int t) @@ -989,6 +1166,9 @@ struct SimWorker : SimShared void update(bool gclk) { + if (gclk) + step += 1; + while (1) { if (debug) @@ -1006,7 +1186,7 @@ struct SimWorker : SimShared if (debug) log("\n-- ph3 --\n"); - top->update_ph3(); + top->update_ph3(gclk); } void initialize_stable_past() @@ -1016,7 +1196,7 @@ struct SimWorker : SimShared top->update_ph1(); if (debug) log("\n-- ph3 (initialize) --\n"); - top->update_ph3(); + top->update_ph3(true); } void set_inports(pool<IdString> ports, State value) @@ -1490,6 +1670,242 @@ struct SimWorker : SimShared write_output_files(); } + struct FoundYWPath + { + SimInstance *instance; + Wire *wire; + IdString memid; + int addr; + }; + + struct YwHierarchy { + dict<IdPath, FoundYWPath> paths; + }; + + YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw) + { + YwHierarchy hierarchy; + pool<IdPath> paths; + dict<IdPath, pool<IdString>> mem_paths; + + for (auto &signal : yw.signals) + paths.insert(signal.path); + + for (auto &clock : yw.clocks) + paths.insert(clock.path); + + for (auto &path : paths) + if (path.has_address()) + mem_paths[path.prefix()].insert(path.back()); + + witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) { + if (item.cell != nullptr) + return instance->children.at(item.cell); + if (item.wire != nullptr) { + if (paths.count(path)) { + if (debug) + log("witness hierarchy: found wire %s\n", path.str().c_str()); + bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second; + if (!inserted) + log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); + } + } else if (item.mem) { + auto it = mem_paths.find(path); + if (it != mem_paths.end()) { + if (debug) + log("witness hierarchy: found mem %s\n", path.str().c_str()); + IdPath word_path = path; + word_path.emplace_back(); + for (auto addr_part : it->second) { + word_path.back() = addr_part; + int addr; + word_path.get_address(addr); + if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size) + continue; + bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second; + if (!inserted) + log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); + } + } + } + return instance; + }); + + for (auto &path : paths) + if (!hierarchy.paths.count(path)) + log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str()); + + dict<IdPath, dict<int, bool>> clock_inputs; + + for (auto &clock : yw.clocks) { + if (clock.is_negedge == clock.is_posedge) + continue; + clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge); + } + for (auto &signal : yw.signals) { + auto it = clock_inputs.find(signal.path); + if (it == clock_inputs.end()) + continue; + + for (auto &clock_input : it->second) { + int offset = clock_input.first; + if (offset >= signal.offset && (offset - signal.offset) < signal.width) { + int clock_bits_offset = signal.bits_offset + (offset - signal.offset); + + State expected = clock_input.second ? State::S0 : State::S1; + + for (int t = 0; t < GetSize(yw.steps); t++) { + if (yw.get_bits(t, clock_bits_offset, 1) != expected) + log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t); + } + } + } + } + // TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file + + return hierarchy; + } + + void set_yw_state(const ReadWitness &yw, const YwHierarchy &hierarchy, int t) + { + log_assert(t >= 0 && t < GetSize(yw.steps)); + + for (auto &signal : yw.signals) { + if (signal.init_only && t >= 1) + continue; + auto found_path_it = hierarchy.paths.find(signal.path); + if (found_path_it == hierarchy.paths.end()) + continue; + auto &found_path = found_path_it->second; + + Const value = yw.get_bits(t, signal.bits_offset, signal.width); + + if (debug) + log("yw: set %s to %s\n", signal.path.str().c_str(), log_const(value)); + + if (found_path.wire != nullptr) { + found_path.instance->set_state_parent_drivers( + SigChunk(found_path.wire, signal.offset, signal.width), + value); + } else if (!found_path.memid.empty()) { + if (t >= 1) + found_path.instance->register_memory_addr(found_path.memid, found_path.addr); + else + found_path.instance->trace_mem_init_database.emplace(make_pair(found_path.memid, found_path.addr), value); + found_path.instance->set_memory_state( + found_path.memid, found_path.addr, + value); + } + } + } + + void set_yw_clocks(const ReadWitness &yw, const YwHierarchy &hierarchy, bool active_edge) + { + for (auto &clock : yw.clocks) { + if (clock.is_negedge == clock.is_posedge) + continue; + auto found_path_it = hierarchy.paths.find(clock.path); + if (found_path_it == hierarchy.paths.end()) + continue; + auto &found_path = found_path_it->second; + + if (found_path.wire != nullptr) { + found_path.instance->set_state( + SigChunk(found_path.wire, clock.offset, 1), + active_edge == clock.is_posedge ? State::S1 : State::S0); + } + } + } + + void run_cosim_yw_witness(Module *topmod, int append) + { + if (!clock.empty()) + log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n"); + if (!reset.empty()) + log_cmd_error("The -reset option is not required nor supported when reading a Yosys witness file.\n"); + if (multiclock) + log_warning("The -multiclock option is not required and ignored when reading a Yosys witness file.\n"); + + ReadWitness yw(sim_filename); + + top = new SimInstance(this, scope, topmod); + register_signals(); + + YwHierarchy hierarchy = prepare_yw_hierarchy(yw); + + if (yw.steps.empty()) { + log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str()); + } else { + top->set_initstate_outputs(State::S1); + set_yw_state(yw, hierarchy, 0); + set_yw_clocks(yw, hierarchy, true); + initialize_stable_past(); + register_output_step(0); + + if (!yw.clocks.empty()) { + if (debug) + log("Simulating non-active clock edge.\n"); + set_yw_clocks(yw, hierarchy, false); + update(false); + register_output_step(5); + } + top->set_initstate_outputs(State::S0); + } + + for (int cycle = 1; cycle < GetSize(yw.steps) + append; cycle++) + { + if (verbose) + log("Simulating cycle %d.\n", cycle); + if (cycle < GetSize(yw.steps)) + set_yw_state(yw, hierarchy, cycle); + set_yw_clocks(yw, hierarchy, true); + update(true); + register_output_step(10 * cycle); + + if (!yw.clocks.empty()) { + if (debug) + log("Simulating non-active clock edge.\n"); + set_yw_clocks(yw, hierarchy, false); + update(false); + register_output_step(5 + 10 * cycle); + } + } + + register_output_step(10 * (GetSize(yw.steps) + append)); + write_output_files(); + } + + void write_summary() + { + if (summary_filename.empty()) + return; + + PrettyJson json; + if (!json.write_to_file(summary_filename)) + log_error("Can't open file `%s' for writing: %s\n", summary_filename.c_str(), strerror(errno)); + + json.begin_object(); + json.entry("version", "Yosys sim summary"); + json.entry("generator", yosys_version_str); + json.entry("steps", step); + json.entry("top", log_id(top->module->name)); + json.name("assertions"); + json.begin_array(); + for (auto &assertion : triggered_assertions) { + json.begin_object(); + json.entry("step", assertion.step); + json.entry("type", log_id(assertion.cell->type)); + json.entry("path", assertion.instance->witness_full_path(assertion.cell)); + auto src = assertion.cell->get_string_attribute(ID::src); + if (!src.empty()) { + json.entry("src", src); + } + json.end_object(); + } + json.end_array(); + json.end_object(); + } + std::string define_signal(Wire *wire) { std::stringstream f; @@ -1734,9 +2150,15 @@ struct VCDWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); }, [this]() { vcdfile << stringf("$upscope $end\n");}, - [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { + [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) { if (use_signal.at(id)) { - vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name); + // Works around gtkwave trying to parse everything past the last [ in a signal + // name. While the emitted range doesn't necessarily match the wire's range, + // this is consistent with the range gtkwave makes up if it doesn't find a + // range + std::string range = strchr(name, '[') ? stringf("[%d:0]", size - 1) : std::string(); + vcdfile << stringf("$var %s %d n%d %s%s%s $end\n", is_reg ? "reg" : "wire", size, id, name[0] == '$' ? "\\" : "", name, range.c_str()); + } } ); @@ -1796,9 +2218,9 @@ struct FSTWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); }, [this]() { fstWriterSetUpscope(fstfile); }, - [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { + [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) { if (!use_signal.at(id)) return; - fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire), + fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, size, name, 0); mapping.emplace(id, fst_id); } @@ -1881,7 +2303,7 @@ struct AIWWriter : public OutputWriter worker->top->write_output_header( [](IdString) {}, []() {}, - [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; } + [this](const char */*name*/, int /*size*/, Wire *wire, int id, bool) { if (wire != nullptr) mapping[wire] = id; } ); std::map<int, Yosys::RTLIL::Const> current; @@ -2013,11 +2435,17 @@ struct SimPass : public Pass { log(" -w\n"); log(" writeback mode: use final simulation state as new init state\n"); log("\n"); - log(" -r\n"); - log(" read simulation results file\n"); - log(" File formats supported: FST, VCD, AIW and WIT\n"); + log(" -r <filename>\n"); + log(" read simulation or formal results file\n"); + log(" File formats supported: FST, VCD, AIW, WIT and .yw\n"); log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); + log(" -append <integer>\n"); + log(" number of extra clock cycles to simulate for a Yosys witness input\n"); + log("\n"); + log(" -summary <filename>\n"); + log(" write a JSON summary to the given file\n"); + log("\n"); log(" -map <filename>\n"); log(" read file with port and latch symbols, needed for AIGER witness input\n"); log("\n"); @@ -2063,6 +2491,7 @@ struct SimPass : public Pass { { SimWorker worker; int numcycles = 20; + int append = 0; bool start_set = false, stop_set = false, at_set = false; log_header(design, "Executing SIM pass (simulate the circuit).\n"); @@ -2146,12 +2575,22 @@ struct SimPass : public Pass { worker.sim_filename = sim_filename; continue; } + if (args[argidx] == "-append" && argidx+1 < args.size()) { + append = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-map" && argidx+1 < args.size()) { std::string map_filename = args[++argidx]; rewrite_filename(map_filename); worker.map_filename = map_filename; continue; } + if (args[argidx] == "-summary" && argidx+1 < args.size()) { + std::string summary_filename = args[++argidx]; + rewrite_filename(summary_filename); + worker.summary_filename = summary_filename; + continue; + } if (args[argidx] == "-scope" && argidx+1 < args.size()) { worker.scope = args[++argidx]; continue; @@ -2235,10 +2674,14 @@ struct SimPass : public Pass { worker.run_cosim_aiger_witness(top_mod); } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) { worker.run_cosim_btor2_witness(top_mod); + } else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) { + worker.run_cosim_yw_witness(top_mod, append); } else { log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); } } + + worker.write_summary(); } } SimPass; diff --git a/passes/techmap/bmuxmap.cc b/passes/techmap/bmuxmap.cc index 03673c278..7aa67d3c0 100644 --- a/passes/techmap/bmuxmap.cc +++ b/passes/techmap/bmuxmap.cc @@ -33,13 +33,22 @@ struct BmuxmapPass : public Pass { log("\n"); log("This pass transforms $bmux cells to trees of $mux cells.\n"); log("\n"); + log(" -pmux\n"); + log(" transform to $pmux instead of $mux cells.\n"); + log("\n"); } void execute(std::vector<std::string> args, RTLIL::Design *design) override { + bool pmux_mode = false; + log_header(design, "Executing BMUXMAP pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-pmux") { + pmux_mode = true; + continue; + } break; } extra_args(args, argidx, design); @@ -53,18 +62,36 @@ struct BmuxmapPass : public Pass { SigSpec sel = cell->getPort(ID::S); SigSpec data = cell->getPort(ID::A); int width = GetSize(cell->getPort(ID::Y)); + int s_width = GetSize(cell->getPort(ID::S)); - for (int idx = 0; idx < GetSize(sel); idx++) { - SigSpec new_data = module->addWire(NEW_ID, GetSize(data)/2); - for (int i = 0; i < GetSize(new_data); i += width) { - RTLIL::Cell *mux = module->addMux(NEW_ID, + if(pmux_mode) + { + int num_cases = 1 << s_width; + SigSpec new_a = SigSpec(State::Sx, width); + SigSpec new_s = module->addWire(NEW_ID, num_cases); + SigSpec new_data = module->addWire(NEW_ID, width); + for (int val = 0; val < num_cases; val++) + { + module->addEq(NEW_ID, sel, SigSpec(val, GetSize(sel)), new_s[val]); + } + RTLIL::Cell *pmux = module->addPmux(NEW_ID, new_a, data, new_s, new_data); + pmux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src)); + data = new_data; + } + else + { + for (int idx = 0; idx < GetSize(sel); idx++) { + SigSpec new_data = module->addWire(NEW_ID, GetSize(data)/2); + for (int i = 0; i < GetSize(new_data); i += width) { + RTLIL::Cell *mux = module->addMux(NEW_ID, data.extract(i*2, width), data.extract(i*2+width, width), sel[idx], new_data.extract(i, width)); - mux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src)); + mux->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src)); + } + data = new_data; } - data = new_data; } module->connect(cell->getPort(ID::Y), data); diff --git a/techlibs/fabulous/Makefile.inc b/techlibs/fabulous/Makefile.inc index 44d57542b..28b0d5ef0 100644 --- a/techlibs/fabulous/Makefile.inc +++ b/techlibs/fabulous/Makefile.inc @@ -8,3 +8,4 @@ $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/ff_map.v)) $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/ram_regfile.txt)) $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/regfile_map.v)) $(eval $(call add_share_file,share/fabulous,techlibs/fabulous/io_map.v)) +$(eval $(call add_share_file,share/fabulous,techlibs/fabulous/arith_map.v)) diff --git a/techlibs/fabulous/arith_map.v b/techlibs/fabulous/arith_map.v new file mode 100644 index 000000000..eca968556 --- /dev/null +++ b/techlibs/fabulous/arith_map.v @@ -0,0 +1,65 @@ +`default_nettype none + +`ifdef ARITH_ha +(* techmap_celltype = "$alu" *) +module _80_fabulous_ha_alu (A, B, CI, BI, X, Y, CO); + +parameter A_SIGNED = 0; +parameter B_SIGNED = 0; +parameter A_WIDTH = 1; +parameter B_WIDTH = 1; +parameter Y_WIDTH = 1; + +parameter _TECHMAP_CONSTMSK_CI_ = 0; +parameter _TECHMAP_CONSTVAL_CI_ = 0; + +(* force_downto *) +input [A_WIDTH-1:0] A; +(* force_downto *) +input [B_WIDTH-1:0] B; +input CI, BI; +(* force_downto *) +output [Y_WIDTH-1:0] X, Y, CO; + +(* force_downto *) +wire [Y_WIDTH-1:0] A_buf, B_buf; +\$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(A_buf)); +\$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(B_buf)); + +(* force_downto *) +wire [Y_WIDTH-1:0] AA = A_buf; +(* force_downto *) +wire [Y_WIDTH-1:0] BB = BI ? ~B_buf : B_buf; +wire [Y_WIDTH:0] CARRY; + + +LUT4_HA #( + .INIT(16'b0), + .I0MUX(1'b1) +) carry_statrt ( + .I0(), .I1(CI), .I2(CI), .I3(), + .Ci(), + .Co(CARRY[0]) +); + +// Carry chain +genvar i; +generate for (i = 0; i < Y_WIDTH; i = i + 1) begin:slice + LUT4_HA #( + .INIT(16'b1001_0110_1001_0110), // full adder sum over (I2, I1, I0) + .I0MUX(1'b1) + ) lut_i ( + .I0(), .I1(AA[i]), .I2(BB[i]), .I3(), + .Ci(CARRY[i]), + .O(Y[i]), + .Co(CARRY[i+1]) + ); + + assign CO[i] = (AA[i] && BB[i]) || ((Y[i] ^ AA[i] ^ BB[i]) && (AA[i] || BB[i])); +end endgenerate + +assign X = AA ^ BB; + +endmodule +`endif + diff --git a/techlibs/fabulous/prims.v b/techlibs/fabulous/prims.v index 8ddae5beb..fe3e8536a 100644 --- a/techlibs/fabulous/prims.v +++ b/techlibs/fabulous/prims.v @@ -24,6 +24,20 @@ module LUT4(output O, input I0, I1, I2, I3); assign O = I0 ? s1[1] : s1[0]; endmodule +module LUT4_HA(output O, Co, input I0, I1, I2, I3, Ci); + parameter [15:0] INIT = 0; + parameter I0MUX = 1'b1; + + wire [ 7: 0] s3 = I3 ? INIT[15: 8] : INIT[ 7: 0]; + wire [ 3: 0] s2 = I2 ? s3[ 7: 4] : s3[ 3: 0]; + wire [ 1: 0] s1 = I1 ? s2[ 3: 2] : s2[ 1: 0]; + + wire I0_sel = I0MUX ? Ci : I0; + assign O = I0_sel ? s1[1] : s1[0]; + + assign Co = (Ci & I1) | (Ci & I2) | (I1 & I2); +endmodule + module LUTFF(input CLK, D, output reg O); initial O = 1'b0; always @ (posedge CLK) begin @@ -93,13 +107,13 @@ module Global_Clock (output CLK); endmodule (* blackbox, keep *) -module InPass4_frame_config (output O0, O1, O2, O3); +module InPass4_frame_config (input CLK, output O0, O1, O2, O3); endmodule (* blackbox, keep *) -module OutPass4_frame_config (input I0, I1, I2, I3); +module OutPass4_frame_config (input CLK, I0, I1, I2, I3); endmodule @@ -414,4 +428,4 @@ module LUTFF_ESS ( O <= D; end endmodule -`endif // COMPLEX_DFF
\ No newline at end of file +`endif // COMPLEX_DFF diff --git a/techlibs/fabulous/synth_fabulous.cc b/techlibs/fabulous/synth_fabulous.cc index d7c45e094..b4a7ab2dc 100644 --- a/techlibs/fabulous/synth_fabulous.cc +++ b/techlibs/fabulous/synth_fabulous.cc @@ -83,6 +83,9 @@ struct SynthPass : public ScriptPass log(" do not run 'alumacc' pass. i.e. keep arithmetic operators in\n"); log(" their direct form ($add, $sub, etc.).\n"); log("\n"); + log(" -carry <none|ha>\n"); + log(" carry mapping style (none, half-adders, ...) default=none\n"); + log("\n"); log(" -noregfile\n"); log(" do not map register files\n"); log("\n"); @@ -119,7 +122,7 @@ struct SynthPass : public ScriptPass log("\n"); } - string top_module, json_file, blif_file, plib, fsm_opts, memory_opts; + string top_module, json_file, blif_file, plib, fsm_opts, memory_opts, carry_mode; std::vector<string> extra_plib, extra_map; bool autotop, forvpr, noalumacc, nofsm, noshare, noregfile, iopad, complexdff, flatten; @@ -137,6 +140,7 @@ struct SynthPass : public ScriptPass noshare = false; iopad = false; complexdff = false; + carry_mode = "none"; flatten = true; json_file = ""; blif_file = ""; @@ -229,6 +233,12 @@ struct SynthPass : public ScriptPass complexdff = true; continue; } + if (args[argidx] == "-carry") { + carry_mode = args[++argidx]; + if (carry_mode != "none" && carry_mode != "ha") + log_cmd_error("Unsupported carry style: %s\n", carry_mode.c_str()); + continue; + } if (args[argidx] == "-noflatten") { flatten = false; continue; @@ -326,7 +336,8 @@ struct SynthPass : public ScriptPass if (check_label("map_gates")) { run("opt -full"); - run("techmap -map +/techmap.v"); + run(stringf("techmap -map +/techmap.v -map +/fabulous/arith_map.v -D ARITH_%s", + help_mode ? "<carry>" : carry_mode.c_str())); run("opt -fast"); } diff --git a/techlibs/gatemate/cells_bb.v b/techlibs/gatemate/cells_bb.v index f6fe6a3e1..87b91764f 100644 --- a/techlibs/gatemate/cells_bb.v +++ b/techlibs/gatemate/cells_bb.v @@ -22,6 +22,9 @@ module CC_PLL #( parameter REF_CLK = "", // e.g. "10.0"
parameter OUT_CLK = "", // e.g. "50.0"
parameter PERF_MD = "", // LOWPOWER, ECONOMY, SPEED
+ parameter LOCK_REQ = 1,
+ parameter CLK270_DOUB = 0,
+ parameter CLK180_DOUB = 0,
parameter LOW_JITTER = 1,
parameter CI_FILTER_CONST = 2,
parameter CP_FILTER_CONST = 4
@@ -123,6 +126,12 @@ module CC_CFG_CTRL( );
endmodule
+(* blackbox *) (* keep *)
+module CC_USR_RSTN (
+ output USR_RSTN
+);
+endmodule
+
(* blackbox *)
module CC_FIFO_40K (
output A_ECC_1B_ERR,
diff --git a/techlibs/gatemate/cells_sim.v b/techlibs/gatemate/cells_sim.v index 7e88fd7cf..7ed6d83ff 100644 --- a/techlibs/gatemate/cells_sim.v +++ b/techlibs/gatemate/cells_sim.v @@ -114,10 +114,10 @@ module CC_LVDS_IBUF #( parameter [0:0] FF_IBF = 1'bx
)(
(* iopad_external_pin *)
- input IP, IN,
+ input I_P, I_N,
output Y
);
- assign Y = IP;
+ assign Y = I_P;
endmodule
@@ -133,10 +133,10 @@ module CC_LVDS_OBUF #( )(
input A,
(* iopad_external_pin *)
- output OP, ON
+ output O_P, O_N
);
- assign OP = A;
- assign ON = ~A;
+ assign O_P = A;
+ assign O_N = ~A;
endmodule
@@ -152,10 +152,10 @@ module CC_LVDS_TOBUF #( )(
input A, T,
(* iopad_external_pin *)
- output OP, ON
+ output O_P, O_N
);
- assign OP = T ? 1'bz : A;
- assign ON = T ? 1'bz : ~A;
+ assign O_P = T ? 1'bz : A;
+ assign O_N = T ? 1'bz : ~A;
endmodule
@@ -174,12 +174,12 @@ module CC_LVDS_IOBUF #( )(
input A, T,
(* iopad_external_pin *)
- inout IOP, ION,
+ inout IO_P, IO_N,
output Y
);
- assign IOP = T ? 1'bz : A;
- assign ION = T ? 1'bz : ~A;
- assign Y = IOP;
+ assign IO_P = T ? 1'bz : A;
+ assign IO_N = T ? 1'bz : ~A;
+ assign Y = IO_P;
endmodule
diff --git a/techlibs/gowin/cells_sim.v b/techlibs/gowin/cells_sim.v index 736aa0707..ab8207ef1 100644 --- a/techlibs/gowin/cells_sim.v +++ b/techlibs/gowin/cells_sim.v @@ -1553,6 +1553,53 @@ parameter DEVICE = "GW1N-1"; // "GW1N-1", "GW1N-4", "GW1N-9", "GW1NR-4", endmodule (* blackbox *) +module PLLVR (CLKOUT, CLKOUTP, CLKOUTD, CLKOUTD3, LOCK, CLKIN, CLKFB, FBDSEL, IDSEL, ODSEL, DUTYDA, PSDA, FDLY, RESET, RESET_P, VREN); +input CLKIN; +input CLKFB; +input RESET; +input RESET_P; +input [5:0] FBDSEL; +input [5:0] IDSEL; +input [5:0] ODSEL; +input [3:0] PSDA,FDLY; +input [3:0] DUTYDA; +input VREN; + +output CLKOUT; +output LOCK; +output CLKOUTP; +output CLKOUTD; +output CLKOUTD3; + +parameter FCLKIN = "100.0"; // frequency of CLKIN +parameter DYN_IDIV_SEL= "false"; // true:IDSEL, false:IDIV_SEL +parameter IDIV_SEL = 0; // 0:1, 1:2 ... 63:64 +parameter DYN_FBDIV_SEL= "false"; // true:FBDSEL, false:FBDIV_SEL +parameter FBDIV_SEL = 0; // 0:1, 1:2 ... 63:64 +parameter DYN_ODIV_SEL= "false"; // true:ODSEL, false:ODIV_SEL +parameter ODIV_SEL = 8; // 2/4/8/16/32/48/64/80/96/112/128 + +parameter PSDA_SEL= "0000"; +parameter DYN_DA_EN = "false"; // true:PSDA or DUTYDA or FDA, false: DA_SEL +parameter DUTYDA_SEL= "1000"; + +parameter CLKOUT_FT_DIR = 1'b1; // CLKOUT fine tuning direction. 1'b1 only +parameter CLKOUTP_FT_DIR = 1'b1; // 1'b1 only +parameter CLKOUT_DLY_STEP = 0; // 0, 1, 2, 4 +parameter CLKOUTP_DLY_STEP = 0; // 0, 1, 2 + +parameter CLKFB_SEL = "internal"; // "internal", "external" +parameter CLKOUT_BYPASS = "false"; // "true", "false" +parameter CLKOUTP_BYPASS = "false"; // "true", "false" +parameter CLKOUTD_BYPASS = "false"; // "true", "false" +parameter DYN_SDIV_SEL = 2; // 2~128, only even numbers +parameter CLKOUTD_SRC = "CLKOUT"; // CLKOUT, CLKOUTP +parameter CLKOUTD3_SRC = "CLKOUT"; // CLKOUT, CLKOUTP +parameter DEVICE = "GW1NS-4"; // "GW1NS-4", "GW1NS-4C", "GW1NSR-4", "GW1NSR-4C", "GW1NSER-4C" + +endmodule + +(* blackbox *) module OSC(OSCOUT); output OSCOUT; diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v index ee5a89e22..e6e15b16e 100644 --- a/techlibs/xilinx/cells_sim.v +++ b/techlibs/xilinx/cells_sim.v @@ -3614,7 +3614,7 @@ module DSP48E1 ( if (CREG == 1) begin always @(posedge CLK) if (RSTC) Cr <= 48'b0; else if (CEC) Cr <= C; end else always @* Cr <= C; - if (CREG == 1) initial Dr = 25'b0; + if (DREG == 1) initial Dr = 25'b0; if (DREG == 1) begin always @(posedge CLK) if (RSTD) Dr <= 25'b0; else if (CED) Dr <= D; end else always @* Dr <= D; diff --git a/tests/arch/common/blockram.v b/tests/arch/common/blockram.v index 5ed0736d0..c06ac96d5 100644 --- a/tests/arch/common/blockram.v +++ b/tests/arch/common/blockram.v @@ -22,7 +22,6 @@ module sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) endmodule // sync_ram_sp -`default_nettype none module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) (input wire clk, write_enable, input wire [DATA_WIDTH-1:0] data_in, @@ -45,3 +44,33 @@ module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) endmodule // sync_ram_sdp + +module sync_ram_tdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) + (input wire clk_a, clk_b, + input wire write_enable_a, write_enable_b, + input wire read_enable_a, read_enable_b, + input wire [DATA_WIDTH-1:0] write_data_a, write_data_b, + input wire [ADDRESS_WIDTH-1:0] addr_a, addr_b, + output reg [DATA_WIDTH-1:0] read_data_a, read_data_b); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] mem [0:DEPTH]; + + always @(posedge clk_a) begin + if (write_enable_a) + mem[addr_a] <= write_data_a; + else + read_data_a <= mem[addr_a]; + end + + always @(posedge clk_b) begin + if (write_enable_b) + mem[addr_b] <= write_data_b; + else + read_data_b <= mem[addr_b]; + end + +endmodule // sync_ram_tdp + diff --git a/tests/arch/ecp5/bug1836.mem b/tests/arch/ecp5/bug1836.mem new file mode 100644 index 000000000..1e904d87c --- /dev/null +++ b/tests/arch/ecp5/bug1836.mem @@ -0,0 +1,32 @@ +0x8000,0x8324,0x8647,0x896a,0x8c8b,0x8fab,0x92c7,0x95e1,
+0x98f8,0x9c0b,0x9f19,0xa223,0xa527,0xa826,0xab1f,0xae10,
+0xb0fb,0xb3de,0xb6b9,0xb98c,0xbc56,0xbf17,0xc1cd,0xc47a,
+0xc71c,0xc9b3,0xcc3f,0xcebf,0xd133,0xd39a,0xd5f5,0xd842,
+0xda82,0xdcb3,0xded7,0xe0eb,0xe2f1,0xe4e8,0xe6cf,0xe8a6,
+0xea6d,0xec23,0xedc9,0xef5e,0xf0e2,0xf254,0xf3b5,0xf504,
+0xf641,0xf76b,0xf884,0xf989,0xfa7c,0xfb5c,0xfc29,0xfce3,
+0xfd89,0xfe1d,0xfe9c,0xff09,0xff61,0xffa6,0xffd8,0xfff5,
+0xffff,0xfff5,0xffd8,0xffa6,0xff61,0xff09,0xfe9c,0xfe1d,
+0xfd89,0xfce3,0xfc29,0xfb5c,0xfa7c,0xf989,0xf884,0xf76b,
+0xf641,0xf504,0xf3b5,0xf254,0xf0e2,0xef5e,0xedc9,0xec23,
+0xea6d,0xe8a6,0xe6cf,0xe4e8,0xe2f1,0xe0eb,0xded7,0xdcb3,
+0xda82,0xd842,0xd5f5,0xd39a,0xd133,0xcebf,0xcc3f,0xc9b3,
+0xc71c,0xc47a,0xc1cd,0xbf17,0xbc56,0xb98c,0xb6b9,0xb3de,
+0xb0fb,0xae10,0xab1f,0xa826,0xa527,0xa223,0x9f19,0x9c0b,
+0x98f8,0x95e1,0x92c7,0x8fab,0x8c8b,0x896a,0x8647,0x8324,
+0x8000,0x7cdb,0x79b8,0x7695,0x7374,0x7054,0x6d38,0x6a1e,
+0x6707,0x63f4,0x60e6,0x5ddc,0x5ad8,0x57d9,0x54e0,0x51ef,
+0x4f04,0x4c21,0x4946,0x4673,0x43a9,0x40e8,0x3e32,0x3b85,
+0x38e3,0x364c,0x33c0,0x3140,0x2ecc,0x2c65,0x2a0a,0x27bd,
+0x257d,0x234c,0x2128,0x1f14,0x1d0e,0x1b17,0x1930,0x1759,
+0x1592,0x13dc,0x1236,0x10a1,0xf1d,0xdab,0xc4a,0xafb,
+0x9be,0x894,0x77b,0x676,0x583,0x4a3,0x3d6,0x31c,
+0x276,0x1e2,0x163,0xf6,0x9e,0x59,0x27,0xa,
+0x0,0xa,0x27,0x59,0x9e,0xf6,0x163,0x1e2,
+0x276,0x31c,0x3d6,0x4a3,0x583,0x676,0x77b,0x894,
+0x9be,0xafb,0xc4a,0xdab,0xf1d,0x10a1,0x1236,0x13dc,
+0x1592,0x1759,0x1930,0x1b17,0x1d0e,0x1f14,0x2128,0x234c,
+0x257d,0x27bd,0x2a0a,0x2c65,0x2ecc,0x3140,0x33c0,0x364c,
+0x38e3,0x3b85,0x3e32,0x40e8,0x43a9,0x4673,0x4946,0x4c21,
+0x4f04,0x51ef,0x54e0,0x57d9,0x5ad8,0x5ddc,0x60e6,0x63f4,
+0x6707,0x6a1e,0x6d38,0x7054,0x7374,0x7695,0x79b8,0x7cdb,
\ No newline at end of file diff --git a/tests/arch/ecp5/bug1836.ys b/tests/arch/ecp5/bug1836.ys new file mode 100644 index 000000000..15cdf4228 --- /dev/null +++ b/tests/arch/ecp5/bug1836.ys @@ -0,0 +1,23 @@ +read_verilog <<EOT +module top( + input clk, + output reg [15:0] sig1, sig2 +); + reg [7:0] ptr1, ptr2; + reg [15:0] mem [0:255]; + + initial begin + $readmemh("bug1836.mem", mem); + end + + always @(posedge clk) begin + sig1 <= mem[ptr1]; + ptr1 <= ptr1 + 3; + sig2 <= mem[ptr2]; + ptr2 <= ptr2 + 7; + end +endmodule +EOT + +synth_ecp5 -top top +select -assert-count 1 t:DP16KD diff --git a/tests/arch/ecp5/memories.ys b/tests/arch/ecp5/memories.ys index 5cddcb952..f075182c8 100644 --- a/tests/arch/ecp5/memories.ys +++ b/tests/arch/ecp5/memories.ys @@ -260,3 +260,13 @@ setattr -set logic_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:DP16KD # requested LUTROM explicitly select -assert-min 9 t:LUT4 + +# ============================== TDP RAM ============================== +# RAM bits <= 18K; Data width <= 18x2; Address width <= 9: -> DP16KD + +design -reset; read_verilog -defer ../common/blockram.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 18 sync_ram_tdp +hierarchy -top sync_ram_tdp +synth_ecp5 -top sync_ram_tdp; cd sync_ram_tdp +select -assert-count 1 t:DP16KD +select -assert-none t:LUT4 diff --git a/tests/arch/fabulous/carry.ys b/tests/arch/fabulous/carry.ys new file mode 100644 index 000000000..bba969d37 --- /dev/null +++ b/tests/arch/fabulous/carry.ys @@ -0,0 +1,9 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -carry ha # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-max 10 t:LUT4_HA +select -assert-max 4 t:LUT1 +select -assert-none t:LUT1 t:LUT4_HA %% t:* %D diff --git a/tests/arch/gatemate/memory.ys b/tests/arch/gatemate/memory.ys index e919920f8..c4bf11cd3 100644 --- a/tests/arch/gatemate/memory.ys +++ b/tests/arch/gatemate/memory.ys @@ -6,6 +6,14 @@ cd sync_ram_sdp select -assert-count 1 t:CC_BUFG select -assert-count 1 t:CC_BRAM_20K +# 512 x 20 bit x 2 -> CC_BRAM_20K TDP RAM +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 20 sync_ram_tdp +synth_gatemate -top sync_ram_tdp -noiopad +select -assert-count 2 t:CC_BUFG +select -assert-count 1 t:CC_BRAM_20K + # 512 x 80 bit -> CC_BRAM_40K SDP RAM design -reset read_verilog ../common/blockram.v diff --git a/tests/arch/ice40/spram.v b/tests/arch/ice40/spram.v new file mode 100644 index 000000000..4e1aef2c6 --- /dev/null +++ b/tests/arch/ice40/spram.v @@ -0,0 +1,22 @@ +module top (clk, write_enable, read_enable, write_data, addr, read_data); +parameter DATA_WIDTH = 8; +parameter ADDR_WIDTH = 8; +parameter SKIP_RDEN = 1; + +input clk; +input write_enable, read_enable; +input [DATA_WIDTH - 1 : 0] write_data; +input [ADDR_WIDTH - 1 : 0] addr; +output [DATA_WIDTH - 1 : 0] read_data; + +(* ram_style = "huge" *) +reg [DATA_WIDTH - 1 : 0] mem [2**ADDR_WIDTH - 1 : 0]; + +always @(posedge clk) begin + if (write_enable) + mem[addr] <= write_data; + else if (SKIP_RDEN || read_enable) + read_data <= mem[addr]; +end + +endmodule diff --git a/tests/arch/ice40/spram.ys b/tests/arch/ice40/spram.ys new file mode 100644 index 000000000..709c21862 --- /dev/null +++ b/tests/arch/ice40/spram.ys @@ -0,0 +1,15 @@ +read_verilog spram.v +hierarchy -top top +synth_ice40 +select -assert-count 1 t:SB_SPRAM256KA +select -assert-none t:SB_SPRAM256KA %% t:* %D + +# Testing with pattern as described in pattern document +design -reset +read_verilog spram.v +chparam -set SKIP_RDEN 0 +hierarchy -top top +synth_ice40 +select -assert-count 1 t:SB_SPRAM256KA +# Below fails due to extra SB_LUT4 +# select -assert-none t:SB_SPRAM256KA %% t:* %D diff --git a/tests/arch/intel_alm/blockram.ys b/tests/arch/intel_alm/blockram.ys index 3b61b9339..21b5ecbfb 100644 --- a/tests/arch/intel_alm/blockram.ys +++ b/tests/arch/intel_alm/blockram.ys @@ -1,6 +1,6 @@ read_verilog ../common/blockram.v chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp -synth_intel_alm -family cyclonev -noiopad -noclkbuf +synth_intel_alm -top sync_ram_sdp -family cyclonev -noiopad -noclkbuf cd sync_ram_sdp select -assert-count 1 t:MISTRAL_NOT select -assert-count 1 t:MISTRAL_M10K diff --git a/tests/arch/xilinx/asym_ram_sdp.ys b/tests/arch/xilinx/asym_ram_sdp.ys new file mode 100644 index 000000000..37f6f314d --- /dev/null +++ b/tests/arch/xilinx/asym_ram_sdp.ys @@ -0,0 +1,50 @@ +# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1 + +# w4b | r16b +design -reset +read_verilog asym_ram_sdp_read_wider.v +synth_xilinx -top asym_ram_sdp_read_wider -noiopad +select -assert-count 1 t:RAMB18E1 + +# w8b | r16b +design -reset +read_verilog asym_ram_sdp_read_wider.v +chparam -set WIDTHA 8 -set SIZEA 512 -set ADDRWIDTHA 9 asym_ram_sdp_read_wider +synth_xilinx -top asym_ram_sdp_read_wider -noiopad +select -assert-count 1 t:RAMB18E1 + +# w4b | r32b +design -reset +read_verilog asym_ram_sdp_read_wider.v +chparam -set WIDTHB 32 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider +synth_xilinx -top asym_ram_sdp_read_wider -noiopad +select -assert-count 1 t:RAMB18E1 + +# w16b | r4b +design -reset +read_verilog asym_ram_sdp_write_wider.v +synth_xilinx -top asym_ram_sdp_write_wider -noiopad +select -assert-count 1 t:RAMB18E1 + +# w16b | r8b +design -reset +read_verilog asym_ram_sdp_write_wider.v +chparam -set WIDTHB 8 -set SIZEB 512 -set ADDRWIDTHB 9 asym_ram_sdp_read_wider +synth_xilinx -top asym_ram_sdp_write_wider -noiopad +select -assert-count 1 t:RAMB18E1 + +# w32b | r4b +design -reset +read_verilog asym_ram_sdp_write_wider.v +chparam -set WIDTHA 32 -set SIZEA 128 -set ADDRWIDTHA 7 asym_ram_sdp_read_wider +synth_xilinx -top asym_ram_sdp_write_wider -noiopad +select -assert-count 1 t:RAMB18E1 + +# w4b | r24b +design -reset +read_verilog asym_ram_sdp_read_wider.v +chparam -set SIZEA 768 +chparam -set WIDTHB 24 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider +synth_xilinx -top asym_ram_sdp_read_wider -noiopad +select -assert-count 1 t:RAMB18E1 + diff --git a/tests/arch/xilinx/asym_ram_sdp_read_wider.v b/tests/arch/xilinx/asym_ram_sdp_read_wider.v new file mode 100644 index 000000000..8743209e3 --- /dev/null +++ b/tests/arch/xilinx/asym_ram_sdp_read_wider.v @@ -0,0 +1,72 @@ +// Asymmetric port RAM +// Read Wider than Write. Read Statement in loop +//asym_ram_sdp_read_wider.v +module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB); + parameter WIDTHA = 4; + parameter SIZEA = 1024; + parameter ADDRWIDTHA = 10; + + parameter WIDTHB = 16; + parameter SIZEB = 256; + parameter ADDRWIDTHB = 8; + + input clkA; + input clkB; + input weA; + input enaA, enaB; + input [ADDRWIDTHA-1:0] addrA; + input [ADDRWIDTHB-1:0] addrB; + input [WIDTHA-1:0] diA; + output [WIDTHB-1:0] doB; + + `define max(a,b) {(a) > (b) ? (a) : (b)} + `define min(a,b) {(a) < (b) ? (a) : (b)} + + function integer log2; + input integer value; + reg [31:0] shifted; + integer res; + begin + if (value < 2) + log2 = value; + else + begin + shifted = value-1; + for (res=0; shifted>0; res=res+1) + shifted = shifted>>1; + log2 = res; + end + end + endfunction + + localparam maxSIZE = `max(SIZEA, SIZEB); + localparam maxWIDTH = `max(WIDTHA, WIDTHB); + localparam minWIDTH = `min(WIDTHA, WIDTHB); + + localparam RATIO = maxWIDTH / minWIDTH; + localparam log2RATIO = log2(RATIO); + + reg [minWIDTH-1:0] RAM [0:maxSIZE-1]; + reg [WIDTHB-1:0] readB; + + always @(posedge clkA) + begin + if (enaA) begin + if (weA) + RAM[addrA] <= diA; + end + end + + always @(posedge clkB) + begin : ramread + integer i; + reg [log2RATIO-1:0] lsbaddr; + if (enaB) begin + for (i = 0; i < RATIO; i = i+1) begin + lsbaddr = i; + readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}]; + end + end + end + assign doB = readB; +endmodule
\ No newline at end of file diff --git a/tests/arch/xilinx/asym_ram_sdp_write_wider.v b/tests/arch/xilinx/asym_ram_sdp_write_wider.v new file mode 100644 index 000000000..cd61a3ccc --- /dev/null +++ b/tests/arch/xilinx/asym_ram_sdp_write_wider.v @@ -0,0 +1,71 @@ +// Asymmetric port RAM +// Write wider than Read. Write Statement in a loop. +// asym_ram_sdp_write_wider.v +module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB); + parameter WIDTHB = 4; + parameter SIZEB = 1024; + parameter ADDRWIDTHB = 10; + + parameter WIDTHA = 16; + parameter SIZEA = 256; + parameter ADDRWIDTHA = 8; + + input clkA; + input clkB; + input weA; + input enaA, enaB; + input [ADDRWIDTHA-1:0] addrA; + input [ADDRWIDTHB-1:0] addrB; + input [WIDTHA-1:0] diA; + output [WIDTHB-1:0] doB; + + `define max(a,b) {(a) > (b) ? (a) : (b)} + `define min(a,b) {(a) < (b) ? (a) : (b)} + + function integer log2; + input integer value; + reg [31:0] shifted; + integer res; + begin + if (value < 2) + log2 = value; + else + begin + shifted = value-1; + for (res=0; shifted>0; res=res+1) + shifted = shifted>>1; + log2 = res; + end + end + endfunction + + localparam maxSIZE = `max(SIZEA, SIZEB); + localparam maxWIDTH = `max(WIDTHA, WIDTHB); + localparam minWIDTH = `min(WIDTHA, WIDTHB); + + localparam RATIO = maxWIDTH / minWIDTH; + localparam log2RATIO = log2(RATIO); + + reg [minWIDTH-1:0] RAM [0:maxSIZE-1]; + reg [WIDTHB-1:0] readB; + + always @(posedge clkB) begin + if (enaB) begin + readB <= RAM[addrB]; + end + end + assign doB = readB; + + always @(posedge clkA) + begin : ramwrite + integer i; + reg [log2RATIO-1:0] lsbaddr; + for (i=0; i< RATIO; i= i+ 1) begin : write1 + lsbaddr = i; + if (enaA) begin + if (weA) + RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH]; + end + end + end +endmodule
\ No newline at end of file diff --git a/tests/arch/xilinx/priority_memory.v b/tests/arch/xilinx/priority_memory.v new file mode 100644 index 000000000..fc943e209 --- /dev/null +++ b/tests/arch/xilinx/priority_memory.v @@ -0,0 +1,122 @@ +module priority_memory ( + clk, wren_a, rden_a, addr_a, wdata_a, rdata_a, + wren_b, rden_b, addr_b, wdata_b, rdata_b + ); + + parameter ABITS = 12; + parameter WIDTH = 72; + + input clk; + input wren_a, rden_a, wren_b, rden_b; + input [ABITS-1:0] addr_a, addr_b; + input [WIDTH-1:0] wdata_a, wdata_b; + output reg [WIDTH-1:0] rdata_a, rdata_b; + + `ifdef USE_HUGE + (* ram_style = "huge" *) + `endif + reg [WIDTH-1:0] mem [0:2**ABITS-1]; + + integer i; + initial begin + rdata_a <= 'h0; + rdata_b <= 'h0; + end + + `ifndef FLIP_PORTS + always @(posedge clk) begin + // A port + if (wren_a) + mem[addr_a] <= wdata_a; + else if (rden_a) + rdata_a <= mem[addr_a]; + + // B port + if (wren_b) + mem[addr_b] <= wdata_b; + else if (rden_b) + if (wren_a && addr_a == addr_b) + rdata_b <= wdata_a; + else + rdata_b <= mem[addr_b]; + end + `else // FLIP PORTS + always @(posedge clk) begin + // A port + if (wren_b) + mem[addr_b] <= wdata_b; + else if (rden_b) + rdata_b <= mem[addr_b]; + + // B port + if (wren_a) + mem[addr_a] <= wdata_a; + else if (rden_a) + if (wren_b && addr_a == addr_b) + rdata_a <= wdata_b; + else + rdata_a <= mem[addr_a]; + end + `endif +endmodule + +module sp_write_first (clk, wren_a, rden_a, addr_a, wdata_a, rdata_a); + + parameter ABITS = 12; + parameter WIDTH = 72; + + input clk; + input wren_a, rden_a; + input [ABITS-1:0] addr_a; + input [WIDTH-1:0] wdata_a; + output reg [WIDTH-1:0] rdata_a; + + (* ram_style = "huge" *) + reg [WIDTH-1:0] mem [0:2**ABITS-1]; + + integer i; + initial begin + rdata_a <= 'h0; + end + + + always @(posedge clk) begin + // A port + if (wren_a) + mem[addr_a] <= wdata_a; + if (rden_a) + if (wren_a) + rdata_a <= wdata_a; + else + rdata_a <= mem[addr_a]; + end +endmodule + +module sp_read_first (clk, wren_a, rden_a, addr_a, wdata_a, rdata_a); + + parameter ABITS = 12; + parameter WIDTH = 72; + + input clk; + input wren_a, rden_a; + input [ABITS-1:0] addr_a; + input [WIDTH-1:0] wdata_a; + output reg [WIDTH-1:0] rdata_a; + + (* ram_style = "huge" *) + reg [WIDTH-1:0] mem [0:2**ABITS-1]; + + integer i; + initial begin + rdata_a <= 'h0; + end + + + always @(posedge clk) begin + // A port + if (wren_a) + mem[addr_a] <= wdata_a; + if (rden_a) + rdata_a <= mem[addr_a]; + end +endmodule diff --git a/tests/arch/xilinx/priority_memory.ys b/tests/arch/xilinx/priority_memory.ys new file mode 100644 index 000000000..d0b2a16ad --- /dev/null +++ b/tests/arch/xilinx/priority_memory.ys @@ -0,0 +1,60 @@ + +# no uram by default +design -reset +read_verilog priority_memory.v +synth_xilinx -family xcup -top priority_memory +select -assert-none t:URAM288 + +# uram parameter +design -reset +read -define USE_HUGE +read_verilog priority_memory.v +synth_xilinx -family xcup -top priority_memory -noiopad +select -assert-count 1 t:URAM288 + +# uram option +design -reset +read_verilog priority_memory.v +synth_xilinx -family xcup -top priority_memory -noiopad -uram +# check for URAM block +select -assert-count 1 t:URAM288 +# check port A in code maps to port A in hardware: +# %co:+[DOUT_A] selects everything connected to a URAM288.DOUT_A port +# w:rdata_a selects the wire rdata_a +# %i finds the intersection of the two above selections +# if the result is 1 then the wire rdata_a is connected to Port A correctly +select -assert-count 1 t:URAM288 %co:+[DOUT_A] w:rdata_a %i +# we expect no more than 2 LUT2s to control the hardware priority +# if there are extra LUTs, then it is likely emulating logic it shouldn't +# ignore anything using blif, since that doesn't seem to support priority logic +# and is indicative of using verific/tabby +select -assert-max 2 t:LUT* n:*blif* %d + +# reverse priority +design -reset +read -define FLIP_PORTS +read_verilog priority_memory.v +synth_xilinx -family xcup -top priority_memory -noiopad -uram +# test priority is mapped correctly, rdata_a should now be connected to Port B +# see above for details +select -assert-count 1 t:URAM288 %co:+[DOUT_B] w:rdata_a %i + +# sp write first +design -reset +read_verilog priority_memory.v +synth_xilinx -family xcup -top sp_write_first -noiopad +select -assert-count 1 t:URAM288 +# write first connects rdata_a to port B +# similar to above, but also tests that rdata_a *isn't* connected to port A +select -assert-none 1 t:URAM288 %co:+[DOUT_A] w:rdata_a %i +select -assert-count 1 t:URAM288 %co:+[DOUT_B] w:rdata_a %i + +# sp read first +design -reset +read_verilog priority_memory.v +synth_xilinx -family xcup -top sp_read_first -noiopad +select -assert-count 1 t:URAM288 +# read first connects rdata_a to port A +# see above for details +select -assert-count 1 t:URAM288 %co:+[DOUT_A] w:rdata_a %i +select -assert-none 1 t:URAM288 %co:+[DOUT_B] w:rdata_a %i diff --git a/tests/memlib/generate.py b/tests/memlib/generate.py index 341486584..f40210501 100644 --- a/tests/memlib/generate.py +++ b/tests/memlib/generate.py @@ -1,13 +1,6 @@ # TODO: -# - memory initialization -# - clock polarity combinations -# - CE/srst/rdwr/be interactions # - priority logic -# - byte enables, wrbe_separate -# - duplication for read ports -# - abits/dbits determination -# - mixed width # - swizzles for weird width progressions @@ -22,6 +15,7 @@ class Test: TESTS = [] ### basic sanity tests +# Asynchronous-read RAM ASYNC = """ module top(clk, ra, wa, rd, wd, we); @@ -56,6 +50,7 @@ TESTS += [ Test("async_small_block", ASYNC_SMALL, ["block_tdp"], [], {"RAM_BLOCK_TDP": 0}), ] +# Synchronous SDP read first SYNC = """ module top(clk, ra, wa, rd, wd, we); @@ -95,6 +90,261 @@ TESTS += [ Test("sync_small_block_attr", SYNC_SMALL_BLOCK, ["lut", "block_tdp"], [], {"RAM_BLOCK_TDP": 1}), ] +### initialization values testing +LUT_INIT = """ +module top(clk, ra, wa, rd, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = {dbits}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] ra, wa; +input wire [DBITS-1:0] wd; +output wire [DBITS-1:0] rd; + +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +integer i; +initial + for (i = 0; i < 2**ABITS-1; i = i + 1) + mem[i] = {ival}; + +always @(posedge clk) + if (we) + mem[wa] <= wd; + +assign rd = mem[ra]; + +endmodule +""" + +INIT_LUT_ZEROS = LUT_INIT.format(abits=4, dbits=4, ival=0); +INIT_LUT_VAL = LUT_INIT.format(abits=4, dbits=4, ival=5); +INIT_LUT_VAL2 = LUT_INIT.format(abits=6, dbits=6, ival="6'h12"); +INIT_LUT_X = LUT_INIT.format(abits=4, dbits=4, ival="4'hx") + +TESTS += [ + Test("init_lut_zeros_zero", INIT_LUT_ZEROS, ["lut"], ["INIT_ZERO"], {"RAM_LUT":1}), + Test("init_lut_zeros_any", INIT_LUT_ZEROS, ["lut"], ["INIT_ANY"], {"RAM_LUT":1}), + Test("init_lut_val_zero", INIT_LUT_VAL, ["lut"], ["INIT_ZERO"], {"RAM_LUT":0}), #CHECK: no emulation? + Test("init_lut_val_any", INIT_LUT_VAL, ["lut"], ["INIT_ANY"], {"RAM_LUT":1}), + Test("init_lut_val_no_undef", INIT_LUT_VAL, ["lut"], ["INIT_NO_UNDEF"], {"RAM_LUT":1}), + Test("init_lut_val2_any", INIT_LUT_VAL2, ["lut"], ["INIT_ANY"], {"RAM_LUT":8}), + Test("init_lut_val2_no_undef", INIT_LUT_VAL2, ["lut"], ["INIT_NO_UNDEF"], {"RAM_LUT":8}), + Test("init_lut_x_none", INIT_LUT_X, ["lut"], ["INIT_NONE"], {"RAM_LUT":1}), + Test("init_lut_x_zero", INIT_LUT_X, ["lut"], ["INIT_ZERO"], {"RAM_LUT":1}), + Test("init_lut_x_any", INIT_LUT_X, ["lut"], ["INIT_ANY"], {"RAM_LUT":1}), + Test("init_lut_x_no_undef", INIT_LUT_X, ["lut"], ["INIT_NO_UNDEF"], {"RAM_LUT":1}), +] + +### width testing 9-bit-per-byte +RAM_9b1B = """ +module top(clk, ra, wa, rd, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = {dbits}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] ra, wa; +input wire [DBITS-1:0] wd; +output reg [DBITS-1:0] rd; + +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +always @(posedge clk) + if (we) + mem[wa] <= wd; + +always @(posedge clk) + rd <= mem[ra]; + +endmodule +""" + +RAM_18b2B = RAM_9b1B.format(abits=3, dbits=18); +RAM_9b1B = RAM_9b1B.format(abits=4, dbits=9); +RAM_4b1B = RAM_9b1B.format(abits=5, dbits=4); +RAM_2b1B = RAM_9b1B.format(abits=6, dbits=2); +RAM_1b1B = RAM_9b1B.format(abits=7, dbits=1); + +TESTS += [ + Test("ram_18b2B", RAM_18b2B, ["9b1B"], [], {"RAM_9b1B":1}), + Test("ram_9b1B", RAM_9b1B, ["9b1B"], [], {"RAM_9b1B":1}), + Test("ram_4b1B", RAM_4b1B, ["9b1B"], [], {"RAM_9b1B":1}), + Test("ram_2b1B", RAM_2b1B, ["9b1B"], [], {"RAM_9b1B":1}), + Test("ram_1b1B", RAM_1b1B, ["9b1B"], [], {"RAM_9b1B":1}), +] + +### initializing 9-bits-per-byte +RAM_9b1B_init = """ +module top(clk, ra, wa, rd, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = {dbits}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] ra, wa; +input wire [DBITS-1:0] wd; +output reg [DBITS-1:0] rd; + +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +integer i; +initial + for (i = 0; i < 2**ABITS-1; i = i + 1) + mem[i] = {ival}; + +always @(posedge clk) + if (we) + mem[wa] <= wd; + +always @(posedge clk) + rd <= mem[ra]; + +endmodule +""" + +INIT_9b1B_ZEROS = RAM_9b1B_init.format(abits=4, dbits=9, ival=0); +INIT_9b1B_VAL = RAM_9b1B_init.format(abits=4, dbits=9, ival=275); +INIT_13b2B_VAL = RAM_9b1B_init.format(abits=3, dbits=13, ival="13'h01f3") +INIT_18b2B_VAL = RAM_9b1B_init.format(abits=4, dbits=18, ival="18'h1f39a"); +INIT_4b1B_X = RAM_9b1B_init.format(abits=5, dbits=4, ival="4'hx") + +TESTS += [ + Test("init_9b1B_zeros_zero", INIT_9b1B_ZEROS, ["9b1B"], ["INIT_ZERO"], {"RAM_9b1B":1}), + Test("init_9b1B_zeros_any", INIT_9b1B_ZEROS, ["9b1B"], ["INIT_ANY"], {"RAM_9b1B":1}), + Test("init_9b1B_val_zero", INIT_9b1B_VAL, ["9b1B"], ["INIT_ZERO"], {"RAM_9b1B":0}), #CHECK: no emulation? + Test("init_9b1B_val_any", INIT_9b1B_VAL, ["9b1B"], ["INIT_ANY"], {"RAM_9b1B":1}), + Test("init_9b1B_val_no_undef", INIT_9b1B_VAL, ["9b1B"], ["INIT_NO_UNDEF"], {"RAM_9b1B":1}), + Test("init_13b2B_val_any", INIT_13b2B_VAL, ["9b1B"], ["INIT_ANY"], {"RAM_9b1B":1}), + Test("init_18b2B_val_any", INIT_18b2B_VAL, ["9b1B"], ["INIT_ANY"], {"RAM_9b1B":2}), + Test("init_18b2B_val_no_undef", INIT_18b2B_VAL, ["9b1B"], ["INIT_NO_UNDEF"], {"RAM_9b1B":2}), + Test("init_4b1B_x_none", INIT_4b1B_X, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B":1}), + Test("init_4b1B_x_zero", INIT_4b1B_X, ["9b1B"], ["INIT_ZERO"], {"RAM_9b1B":1}), + Test("init_4b1B_x_any", INIT_4b1B_X, ["9b1B"], ["INIT_ANY"], {"RAM_9b1B":1}), + Test("init_4b1B_x_no_undef", INIT_4b1B_X, ["9b1B"], ["INIT_NO_UNDEF"], {"RAM_9b1B":1}), +] + +### Clock polarity combinations +# I'm not entirely convinced auto-test is correctly testing clock edging +# but they do at least all gen/synth +SYNCCLOCK = """ +module top(clk, ra, wa, rd, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = 8; + +input wire clk; +input wire we; +input wire [ABITS-1:0] ra, wa; +input wire [DBITS-1:0] wd; +output reg [DBITS-1:0] rd; + +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +always @(posedge clk) + if (we) + mem[wa] <= wd; + +always @(posedge clk) + rd <= mem[ra]; + +endmodule +""" +for (abits, cnt, wclk, rclk, shared) in [ + (4, 1, "ANY","ANY", False), + (4, 1, "ANY","NEG", False), + (4, 1, "ANY","POS", False), + (4, 1, "NEG","ANY", False), + (4, 1, "NEG","POS", False), + (4, 1, "NEG","NEG", False), + (4, 1, "POS","ANY", False), + (4, 1, "POS","NEG", False), + (4, 1, "POS","POS", False), + (4, 1, "ANY","ANY", True), + (4, 0, "NEG","POS", True), # FF mapping + (4, 1, "NEG","NEG", True), + (4, 0, "POS","NEG", True), # FF mapping + (4, 1, "POS","POS", True), + # cannot combine "ANY" with "POS|NEG" when using shared clock +]: + name = f"clock_a{abits}_w{wclk}r{rclk}s{shared}" + defs = ["WCLK_" + wclk, "RCLK_" + rclk] + if (shared): + defs.append("SHARED_CLK") + TESTS.append(Test( + name, SYNCCLOCK.format(abits=abits), + ["clock_sdp"], defs, {"RAM_CLOCK_SDP": cnt} + )) + +### mixed width testing +# Wide write port +MIXED_WRITE = """ +module top(clk, ra, wa, rd, wd, we); + +localparam WABITS = {wabits}; +localparam WDBITS = {wdbits}; + +localparam RABITS = {rabits}; +localparam RDBITS = {rdbits}; + +input wire clk; +input wire we; +input wire [WABITS-1:0] wa; +input wire [WDBITS-1:0] wd; +input wire [RABITS-1:0] ra; +output reg [RDBITS-1:0] rd; + +localparam DEPTH = (2**WABITS); + +localparam OFFSET = RABITS-WABITS; + +(* syn_ramstyle = "block_ram" *) +reg [WDBITS-1:0] mem [0:DEPTH-1]; + +always @(posedge clk) + if (we) + mem[wa] <= wd; + +if (OFFSET > 0) begin + reg [WDBITS-1:0] mem_read; + reg [OFFSET-1:0] subaddr_r; + always @(posedge clk) begin + mem_read <= mem[ra[RABITS-1:OFFSET]]; + subaddr_r <= ra[OFFSET-1:0]; + end + + always @(mem_read, subaddr_r) + rd <= mem_read[subaddr_r*RDBITS+:RDBITS]; +end +else +begin + always @(posedge clk) + case (OFFSET) + 0: rd <= mem[ra]; + -1: rd <= {{ mem[ra], mem[ra+1] }}; + endcase +end +endmodule +""" + +UNMIXED = MIXED_WRITE.format(wabits=4, wdbits=9, rabits=4, rdbits=9) +MIXED_9_18 = MIXED_WRITE.format(wabits=5, wdbits=9, rabits=4, rdbits=18) +MIXED_18_9 = MIXED_WRITE.format(wabits=3, wdbits=18, rabits=4, rdbits=9) +MIXED_36_9 = MIXED_WRITE.format(wabits=3, wdbits=36, rabits=5, rdbits=9) +MIXED_4_2 = MIXED_WRITE.format(wabits=5, wdbits=4, rabits=6, rdbits=2); + +TESTS += [ + Test("unmixed", UNMIXED, ["9b1B"], [], {"RAM_9b1B":1}), + Test("mixed_9_18", MIXED_9_18, ["9b1B"], [], {"RAM_9b1B":4}), #CHECK: only using half the memory + Test("mixed_18_9", MIXED_18_9, ["9b1B"], [], {"RAM_9b1B":1}), + Test("mixed_36_9", MIXED_36_9, ["9b1B"], [], {"RAM_9b1B":2}), + Test("mixed_4_2", MIXED_4_2, ["9b1B"], [], {"RAM_9b1B":1}), +] + ### basic TDP test TDP = """ @@ -131,7 +381,7 @@ TESTS += [ ] # shared clock - +# Synchronous SDP with clock domain crossing SYNC_2CLK = """ module top(rclk, wclk, ra, wa, rd, wd, we); @@ -163,7 +413,7 @@ TESTS += [ ] # inter-port transparency - +# Synchronous SDP with write-first behaviour SYNC_TRANS = """ module top(clk, ra, wa, rd, wd, we); @@ -201,7 +451,7 @@ TESTS += [ ] # rdwr checks - +# Synchronous single-port RAM with mutually exclusive read/write SP_NO_CHANGE = """ module top(clk, addr, rd, wd, we); @@ -247,6 +497,7 @@ end endmodule """ +# Synchronous single-port RAM with write-first behaviour SP_NEW = """ module top(clk, addr, rd, wd, we); @@ -295,6 +546,7 @@ end endmodule """ +# Synchronous single-port RAM with read-first behaviour SP_OLD = """ module top(clk, addr, rd, wd, we); @@ -373,6 +625,7 @@ TESTS += [ Test("sp_old_auto_be", SP_OLD_BE, ["block_sp"], ["RDWR_NO_CHANGE", "RDWR_OLD", "RDWR_NEW"], {"RAM_BLOCK_SP": (1, {"OPTION_RDWR": "OLD"})}), ] +# Synchronous read port with initial value SP_INIT = """ module top(clk, addr, rd, wd, we, re); @@ -418,6 +671,7 @@ TESTS += [ Test("sp_init_v_any_re", SP_INIT_V, ["block_sp"], ["RDINIT_ANY", "RDEN", "RDWR_OLD"], {"RAM_BLOCK_SP": 1}), ] +# Synchronous read port with asynchronous reset SP_ARST = """ module top(clk, addr, rd, wd, we, re, ar); @@ -488,6 +742,7 @@ TESTS += [ Test("sp_arst_n_init_re", SP_ARST_N, ["block_sp"], ["RDINIT_ANY", "RDARST_INIT", "RDEN", "RDWR_OLD"], {"RAM_BLOCK_SP": 1}), ] +# Synchronous read port with synchronous reset (reset priority over enable) SP_SRST = """ module top(clk, addr, rd, wd, we, re, sr); @@ -515,6 +770,7 @@ end endmodule """ +# Synchronous read port with synchronous reet (enable priority over reset) SP_SRST_G = """ module top(clk, addr, rd, wd, we, re, sr); @@ -602,6 +858,180 @@ TESTS += [ Test("sp_srst_gv_init_re", SP_SRST_GV, ["block_sp"], ["RDINIT_ANY", "RDSRST_INIT", "RDEN", "RDWR_OLD"], {"RAM_BLOCK_SP": 1}), ] +# Byte enables, wrbe_separate +SYNC_ENABLE = """ +module top(clk, rwa, rd, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = {dbits}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] rwa; +input wire [DBITS-1:0] wd; +output reg [DBITS-1:0] rd; + +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +always @(posedge clk) begin + if (we) + mem[rwa] <= wd; + else + rd <= mem[rwa]; +end + +endmodule +""" + +for (abits, dbits, sep, defs, cells) in [ + (4, 4, False, ["NO_BYTE"], {"RAM_WREN": 1}), + (5, 4, False, ["NO_BYTE"], {"RAM_WREN": 2}), + (6, 4, False, ["NO_BYTE"], {"RAM_WREN": 4}), + # (4, 4, True, ["NO_BYTE"], {"RAM_WREN": 1}), # should throw an error + (3, 8, False, ["NO_BYTE"], {"RAM_WREN": 2}), # needs two write ports + (4, 8, False, ["NO_BYTE"], {"RAM_WREN": 2}), + (4, 4, False, ["W4_B4"], {"RAM_WREN": 1}), + (4, 8, True, ["W4_B4"], {"RAM_WREN": 2}), + (4, 8, False, ["W8_B4"], {"RAM_WREN": 1}), + (4, 8, True, ["W8_B4"], {"RAM_WREN": 1}), + (4, 8, False, ["W8_B8"], {"RAM_WREN": 1}), + (4, 8, True, ["W8_B8"], {"RAM_WREN": 1}), + +]: + name = f"wren_a{abits}d{dbits}_{defs[0]}" + if (sep): + defs.append("WRBE_SEPARATE") + name += "_separate" + + TESTS.append(Test( + name, SYNC_ENABLE.format(abits=abits, dbits=dbits), + ["wren"], defs, cells + )) + +# Write port with byte enables +ENABLES = """ +module top(clk, we, be, rwa, wd, rd); + +localparam ABITS = {abits}; +localparam WBITS = {wbits}; +localparam WORDS = {words}; + +input wire clk; +input wire we; +input wire [WORDS-1:0] be; +input wire [ABITS-1:0] rwa; +input wire [(WBITS*WORDS)-1:0] wd; +output reg [(WBITS*WORDS)-1:0] rd; + +reg [(WBITS*WORDS)-1:0] mem [0:2**ABITS-1]; + +integer i; +always @(posedge clk) + for (i=0; i<WORDS; i=i+1) + if (we && be[i]) + mem[rwa][i*WBITS+:WBITS] <= wd[i*WBITS+:WBITS]; + +always @(posedge clk) + if (!we) + rd <= mem[rwa]; + +endmodule +""" + +for (abits, wbits, words, defs, cells) in [ + (4, 2, 8, ["W16_B4"], {"RAM_WREN": 2}), + (4, 4, 4, ["W16_B4"], {"RAM_WREN": 1}), + (5, 4, 2, ["W16_B4"], {"RAM_WREN": 1}), + (5, 4, 4, ["W16_B4"], {"RAM_WREN": 2}), + (4, 8, 2, ["W16_B4"], {"RAM_WREN": 1}), + (5, 8, 1, ["W16_B4"], {"RAM_WREN": 1}), + (5, 8, 2, ["W16_B4"], {"RAM_WREN": 2}), + (4,16, 1, ["W16_B4"], {"RAM_WREN": 1}), + (4, 4, 2, ["W8_B8"], {"RAM_WREN": 2}), + (4, 4, 1, ["W8_B8"], {"RAM_WREN": 1}), + (4, 8, 2, ["W8_B8"], {"RAM_WREN": 2}), + (3, 8, 2, ["W8_B8"], {"RAM_WREN": 2}), + (4, 4, 2, ["W8_B4"], {"RAM_WREN": 1}), + (4, 2, 4, ["W8_B4"], {"RAM_WREN": 2}), + (4, 4, 4, ["W8_B4"], {"RAM_WREN": 2}), + (4, 4, 4, ["W4_B4"], {"RAM_WREN": 4}), + (4, 4, 5, ["W4_B4"], {"RAM_WREN": 5}), + +]: + name = f"wren_a{abits}d{wbits}w{words}_{defs[0]}" + TESTS.append(Test( + name, ENABLES.format(abits=abits, wbits=wbits, words=words), + ["wren"], defs, cells + )) + + defs.append("WRBE_SEPARATE") + name += "_separate" + TESTS.append(Test( + name, ENABLES.format(abits=abits, wbits=wbits, words=words), + ["wren"], defs, cells + )) + +# abits/dbits determination (aka general geometry picking) +GEOMETRIC = """ +module top(clk, rwa, rd, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = {dbits}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] rwa; +input wire [DBITS-1:0] wd; +output reg [DBITS-1:0] rd; + +(* ram_style="block" *) +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +always @(posedge clk) + if (we) + mem[rwa] <= wd; + else + rd <= mem[rwa]; + +endmodule +""" + +for (abits,dbits, libs, defs, cells) in [ + # W64_B8 gives 16 * 64 = 1024 bits of memory with up to 8x8b rw ports + ( 4, 64, ["wren"], ["W64_B8"], {"RAM_WREN": 1}), + ( 5, 32, ["wren"], ["W64_B8"], {"RAM_WREN": 1}), + ( 5, 64, ["wren"], ["W64_B8"], {"RAM_WREN": 2}), + ( 6, 16, ["wren"], ["W64_B8"], {"RAM_WREN": 1}), + ( 6, 30, ["wren"], ["W64_B8"], {"RAM_WREN": 2}), + ( 6, 64, ["wren"], ["W64_B8"], {"RAM_WREN": 4}), + ( 7, 4, ["wren"], ["W64_B8"], {"RAM_WREN": 1}), + ( 7, 6, ["wren"], ["W64_B8"], {"RAM_WREN": 1}), + ( 7, 8, ["wren"], ["W64_B8"], {"RAM_WREN": 1}), + ( 7, 17, ["wren"], ["W64_B8"], {"RAM_WREN": 3}), + ( 8, 4, ["wren"], ["W64_B8"], {"RAM_WREN": 2}), + ( 8, 6, ["wren"], ["W64_B8"], {"RAM_WREN": 2}), + ( 9, 4, ["wren"], ["W64_B8"], {"RAM_WREN": 4}), + ( 9, 8, ["wren"], ["W64_B8"], {"RAM_WREN": 4}), + ( 9, 5, ["wren"], ["W64_B8"], {"RAM_WREN": 4}), + ( 9, 6, ["wren"], ["W64_B8"], {"RAM_WREN": 4}), + # 9b1B gives 128 bits of memory with 1 2 or 4 bit read and write ports + # or 144 bits with 9 or 18 bit read and write ports + ( 3, 18, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 1}), + ( 4, 4, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 1}), + ( 4, 18, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 2}), + ( 5, 32, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 8}), + ( 6, 4, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 2}), + ( 7, 11, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 11}), + ( 7, 18, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 16}), + ( 11, 1, ["9b1B"], ["INIT_NONE"], {"RAM_9b1B": 16}), +]: + name = f"geom_a{abits}d{dbits}_{libs[0]}" + TESTS.append(Test( + name, GEOMETRIC.format(abits=abits, dbits=dbits), + libs, defs, cells + )) + +# Mixed width testing WIDE_SDP = """ module top(rclk, ra, rd, re, rr, wclk, wa, wd, we); @@ -857,6 +1287,233 @@ for (aw, rw, ww, bw, cntww, cntwr) in [ {"RAM_WIDE_WRITE": cntww} )) +# Multiple read ports +# 1rw port plus 3 (or 7) r ports +QUAD_PORT = """ +module top(clk, rwa, r0a, r1a, r2a, rd, r0d, r1d, r2d, wd, we); + +localparam ABITS = {abits}; +localparam DBITS = {dbits}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] rwa; +input wire [ABITS-1:0] r0a; +input wire [ABITS-1:0] r1a; +input wire [ABITS-1:0] r2a; +input wire [DBITS-1:0] wd; +output wire [DBITS-1:0] rd; +output wire [DBITS-1:0] r0d; +output wire [DBITS-1:0] r1d; +output wire [DBITS-1:0] r2d; + +reg [DBITS-1:0] mem [0:2**ABITS-1]; + +always @(posedge clk) + if (we) + mem[rwa] <= wd; + +assign rd = mem[rwa]; +assign r0d = mem[r0a]; +assign r1d = mem[r1a]; +assign r2d = mem[r2a]; + +endmodule +""" + +for (abits, dbits, cnt) in [ + (2, 2, 1), + (4, 2, 1), + (5, 2, 2), + (4, 4, 2), + (6, 2, 4), + (4, 8, 4), +]: + TESTS.append(Test( + f"quad_port_a{abits}d{dbits}", + QUAD_PORT.format(abits=abits, dbits=dbits), + ["multilut"], ["PORTS_QUAD"], + {"LUT_MULTI": cnt} + )) + +# Wide asynchronous read port +WIDE_READ = """ +module top(clk, we, rwa, wd, rd); + +localparam ABITS = {abits}; +localparam WBITS = {wbits}; +localparam RWORDS = {rwords}; + +input wire clk; +input wire we; +input wire [ABITS-1:0] rwa; +input wire [WBITS-1:0] wd; +output wire [(WBITS*RWORDS)-1:0] rd; + +reg [WBITS-1:0] mem [0:2**ABITS-1]; + +always @(posedge clk) + if (we) + mem[rwa] <= wd; + +genvar i; +generate + for (i = 0; i < RWORDS; i = i + 1) + assign rd[i*WBITS+:WBITS] = mem[rwa + i]; +endgenerate + +endmodule +""" + +for (abits, wbits, rwords, cntquad, cntoct) in [ + (4, 2, 1, 1, 1), + (4, 2, 2, 1, 1), + (4, 2, 3, 1, 1), + (4, 2, 4, 1, 1), + (4, 2, 5, 2, 1), + (4, 2, 6, 2, 1), + (4, 2, 7, 2, 1), # Write port needs to be duplicated, so only 3 extra read + (4, 2, 8, 3, 1), # ports per quad port LUT (i.e. 7 ports in 2, 8 ports in 3) + (4, 2, 9, 3, 2), + (4, 4, 1, 2, 2), + (4, 4, 4, 2, 2), + (4, 4, 6, 4, 2), + (4, 4, 9, 6, 4), + (5, 2, 1, 2, 2), + (5, 2, 4, 2, 2), + (5, 2, 9, 6, 4), +]: + TESTS.append(Test( + f"wide_quad_a{abits}w{wbits}r{rwords}", + WIDE_READ.format(abits=abits, wbits=wbits, rwords=rwords), + ["multilut"], ["PORTS_QUAD"], + {"LUT_MULTI": cntquad} + )) + TESTS.append(Test( + f"wide_oct_a{abits}w{wbits}r{rwords}", + WIDE_READ.format(abits=abits, wbits=wbits, rwords=rwords), + ["multilut"], ["PORTS_OCT"], + {"LUT_MULTI": cntoct} + )) + +# signal priorities & pattern testing +PRIORITY = """ +module top(clk, clken, wren, wben, rden, rst, addr, wdata, rdata); + +localparam ABITS = {abits}; +localparam WBITS = {wbits}; +localparam WORDS = {words}; + +localparam BITS = WBITS * WORDS; + +input wire clk, clken; +input wire wren, rden, rst; +input wire [WORDS-1:0] wben; +input wire [ABITS-1:0] addr; +input wire [BITS-1:0] wdata; +output reg [BITS-1:0] rdata; + +reg [BITS-1:0] mem [0:2**ABITS-1]; + +integer i; +always @(posedge clk) begin +{code} +end +endmodule +""" +#reset_gate in ["ungated", "rst", "rden && rst"] +#clk_en in [True, False] +#rdwr in ["nc", "old", "new", "undef", "newdef"] + +for (testname, reset_gate, rdwr, clk_en, add_logic) in [ + ("no_reset", "", "old", False, 0), + ("gclken", "rst", "old", False, 0), + ("ungated", "ungated", "old", False, 1), # muxes wren with rst + ("gclken_ce", "rst", "old", True, 3), # AND to simulate CLK_EN + ("grden", "rden && rst", "old", False, 1), # selects _clken, simulates _rden + ("grden_ce", "rden && rst", "old", True, 4), # both of the above + ("exclwr", "", "nc", False, 2), # selects new_only and simulates + ("excl_rst", "rst", "nc", False, 3), # as above, extra gate for rst + ("transwr", "", "new", False, 0), + ("trans_rst", "rst", "new", False, 0), +]: + write = "if (wren) \n\t\tmem[addr] <= wdata;" + + if rdwr == "new": + read = """if (rden) + if (wren) + rdata <= wdata; + else + rdata <= mem[addr];""" + else: + read = "if (rden) \n\t\trdata <= mem[addr];" + + if "rst" in reset_gate: + read = f"if ({reset_gate})\n\t\trdata <= 0; \n\telse {read}" + + if reset_gate == "ungated": + outer = "if (rst)\n\trdata <= 0;\nelse " + else: + outer = "" + + if clk_en: + outer = f"{outer}if (clken) " + + code = f"""{outer}begin + {write} + {"else " if rdwr == "nc" else ""}{read} +end""" + + TESTS.append(Test( + testname, PRIORITY.format(code=code, abits=4, wbits=8, words=2), + ["block_sp_full"], ["USE_SRST"], + {"RAM_BLOCK_SP": 1, "$*": add_logic} + )) + +for (testname, reset_gate, defs, rdwr, add_logic) in [ + ("wr_byte", "", ["USE_SRST_BLOCKING"], "old", 0), + ("trans_byte", "", ["USE_SRST_BLOCKING"], "new", 0), + ("wr_rst_byte", "rst", ["USE_SRST"], "old", 2), # expected mux to emulate blocking + ("rst_wr_byte", "rst", ["USE_SRST_BLOCKING"], "old", 2), # should use hardware blocking, doesn't + ("rdenrst_wr_byte", "rden && rst", ["USE_SRST"], "old", 3), +]: + wordsloop = "for (i=0; i<WORDS; i=i+1)" + if rdwr == "old": + read_write = f"""if (rden) + rdata = mem[addr]; + {wordsloop} + if (wben[i]) + mem[addr][i] <= wdata[i];""" + else: + read_write = f"""{wordsloop} + if (wben[i]) begin + mem[addr][i] <= wdata[i]; + rdata[i] <= wdata[i]; + end else + rdata[i] <= mem[addr][i];""" + + if "rst" in reset_gate: + reset_rw = f"""if ({reset_gate}) + rdata <= 0; +else begin + {read_write} +end""" + else: + reset_rw = read_write + + if reset_gate == "ungated": + outer = "if (rst)\n\trdata <= 0;\nelse " + else: + outer = "" + + code = f"{outer}\n{reset_rw}" + + TESTS.append(Test( + testname, PRIORITY.format(code=code, abits=4, wbits=1, words=2), + ["block_sp_full"], defs, + {"RAM_BLOCK_SP": 1, "$*": add_logic} + )) + with open("run-test.mk", "w") as mf: mf.write("ifneq ($(strip $(SEED)),)\n") mf.write("SEEDOPT=-S$(SEED)\n") diff --git a/tests/memlib/memlib_9b1B.txt b/tests/memlib/memlib_9b1B.txt new file mode 100644 index 000000000..4917aaf8b --- /dev/null +++ b/tests/memlib/memlib_9b1B.txt @@ -0,0 +1,31 @@ +ram block \RAM_9b1B { + cost 64; + abits 7; + widths 1 2 4 9 18 per_port; + byte 9; + + ifdef INIT_NONE { + option "INIT" "NONE" { + init none; + } + } else ifdef INIT_ZERO { + option "INIT" "ZERO" { + init zero; + } + } else ifdef INIT_NO_UNDEF { + option "INIT" "NO_UNDEF" { + init no_undef; + } + } else ifdef INIT_ANY { + option "INIT" "ANY" { + init any; + } + } + + port sw "W" { + clock anyedge; + } + port sr "R" { + clock anyedge; + } +} diff --git a/tests/memlib/memlib_9b1B.v b/tests/memlib/memlib_9b1B.v new file mode 100644 index 000000000..55545ebd4 --- /dev/null +++ b/tests/memlib/memlib_9b1B.v @@ -0,0 +1,68 @@ +module RAM_9b1B ( + input PORT_R_CLK, + input [6:0] PORT_R_ADDR, + output reg [PORT_R_WIDTH-1:0] PORT_R_RD_DATA, + input PORT_W_CLK, + input [PORT_W_WR_EN_WIDTH-1:0] PORT_W_WR_EN, + input [6:0] PORT_W_ADDR, + input [PORT_W_WIDTH-1:0] PORT_W_WR_DATA +); + +parameter INIT = 0; +parameter OPTION_INIT = "UNDEFINED"; +parameter PORT_R_WIDTH = 9; +parameter PORT_W_WIDTH = 9; +parameter PORT_R_CLK_POL = 0; +parameter PORT_W_CLK_POL = 0; +parameter PORT_W_WR_EN_WIDTH = 1; + +reg [8:0] mem [0:15]; + +integer i; +initial + for (i = 0; i < 16; i += 1) + case (OPTION_INIT) + "NONE": mem[i] = mem[i]; //? + "ZERO": mem[i] = 9'h0; + "ANY": mem[i] = INIT[i*9+:9]; + "NO_UNDEF": mem[i] = INIT[i*9+:9]; + "UNDEFINED": mem[i] = 9'hx; + endcase + +wire [3:0] addr_r; +assign addr_r = PORT_R_ADDR[6:3]; +reg [17:0] mem_read; +reg [2:0] subaddr_r; +always @(negedge (PORT_R_CLK ^ PORT_R_CLK_POL)) begin + subaddr_r <= PORT_R_ADDR[2:0]; + mem_read[8:0] <= mem[addr_r]; + if (PORT_R_WIDTH == 18) + mem_read[17:9] <= mem[addr_r + 1]; +end + +always @(mem_read, subaddr_r) begin + case (PORT_R_WIDTH) + 18: PORT_R_RD_DATA <= mem_read; + 9: PORT_R_RD_DATA <= mem_read[8:0]; + 4: PORT_R_RD_DATA <= mem_read[subaddr_r[2]*4+:4]; + 2: PORT_R_RD_DATA <= mem_read[subaddr_r[2:1]*2+:2]; + 1: PORT_R_RD_DATA <= mem_read[subaddr_r]; + endcase +end + +wire [3:0] addr_w; +assign addr_w = PORT_W_ADDR[6:3]; +always @(negedge (PORT_W_CLK ^ PORT_W_CLK_POL)) begin + if (PORT_W_WR_EN[0]) + case (PORT_W_WIDTH) + 18, + 9: mem[addr_w] <= PORT_W_WR_DATA[8:0]; + 4: mem[addr_w][PORT_W_ADDR[2]*4+:4] <= PORT_W_WR_DATA; + 2: mem[addr_w][PORT_W_ADDR[2:1]*2+:2] <= PORT_W_WR_DATA; + 1: mem[addr_w][PORT_W_ADDR[2:0]] <= PORT_W_WR_DATA; + endcase + if (PORT_W_WR_EN[1]) + mem[addr_w + 1] <= PORT_W_WR_DATA[17:9]; +end + +endmodule diff --git a/tests/memlib/memlib_block_sp_full.txt b/tests/memlib/memlib_block_sp_full.txt new file mode 100644 index 000000000..000f91af3 --- /dev/null +++ b/tests/memlib/memlib_block_sp_full.txt @@ -0,0 +1,61 @@ +ram block \RAM_BLOCK_SP { + cost 2; + abits 4; + width 16; + byte 8; + port srsw "A" { + clock posedge; + clken; + rden; + + option "RDWR" "NO_CHANGE" { + rdwr no_change; + } + option "RDWR" "OLD" { + rdwr old; + } + option "RDWR" "NEW" { + rdwr new; + } + option "RDWR" "NEW_ONLY" { + rdwr new_only; + } + + ifdef USE_ARST { + option "RDARST" "ZERO" { + rdarst zero; + } + option "RDARST" "ANY" { + rdarst any; + } + } + + ifdef USE_SRST { + option "SRST_BLOCK" 0 { + option "SRST_GATE" 0 { + rdsrst zero ungated; + } + option "SRST_GATE" 1 { + rdsrst zero gated_clken; + } + option "SRST_GATE" 2 { + rdsrst zero gated_rden; + } + } + } + + ifdef USE_SRST_BLOCKING { + option "SRST_BLOCK" 1 { + option "SRST_GATE" 0 { + rdsrst zero ungated block_wr; + } + option "SRST_GATE" 1 { + rdsrst zero gated_clken block_wr; + } + option "SRST_GATE" 2 { + rdsrst zero gated_rden block_wr; + } + } + } + } +} diff --git a/tests/memlib/memlib_block_sp_full.v b/tests/memlib/memlib_block_sp_full.v new file mode 100644 index 000000000..8ba32b9ed --- /dev/null +++ b/tests/memlib/memlib_block_sp_full.v @@ -0,0 +1,82 @@ +module RAM_BLOCK_SP( + input PORT_A_CLK, + input PORT_A_CLK_EN, + input PORT_A_RD_EN, + input PORT_A_RD_ARST, + input PORT_A_RD_SRST, + input [1:0] PORT_A_WR_EN, + input [3:0] PORT_A_ADDR, + output reg [15:0] PORT_A_RD_DATA, + input [15:0] PORT_A_WR_DATA +); + +parameter OPTION_RDWR = "UNDEFINED"; +parameter OPTION_RDINIT = "UNDEFINED"; +parameter OPTION_RDARST = "UNDEFINED"; +parameter OPTION_RDSRST = "ZERO"; +parameter OPTION_SRST_GATE = 0; +parameter OPTION_SRST_BLOCK = 0; +parameter PORT_A_RD_INIT_VALUE = 16'hxxxx; +parameter PORT_A_RD_ARST_VALUE = 16'hxxxx; +parameter PORT_A_RD_SRST_VALUE = 16'hxxxx; + +reg [15:0] mem [0:15]; + +initial + if (OPTION_RDINIT == "ZERO") + PORT_A_RD_DATA = 0; + else if (OPTION_RDINIT == "ANY") + PORT_A_RD_DATA = PORT_A_RD_INIT_VALUE; + +localparam ARST_VALUE = + (OPTION_RDARST == "ZERO") ? 16'h0000 : + (OPTION_RDARST == "INIT") ? PORT_A_RD_INIT_VALUE : + (OPTION_RDARST == "ANY") ? PORT_A_RD_ARST_VALUE : + 16'hxxxx; + +localparam SRST_VALUE = + (OPTION_RDSRST == "ZERO") ? 16'h0000 : + (OPTION_RDSRST == "INIT") ? PORT_A_RD_INIT_VALUE : + (OPTION_RDSRST == "ANY") ? PORT_A_RD_SRST_VALUE : + 16'hxxxx; + +pulldown (PORT_A_RD_ARST); +pulldown (PORT_A_RD_SRST); + +always @(posedge PORT_A_CLK) begin + if (PORT_A_CLK_EN) begin + if (!(PORT_A_RD_SRST && OPTION_SRST_BLOCK)) begin + if (PORT_A_WR_EN[0]) + mem[PORT_A_ADDR][7:0] <= PORT_A_WR_DATA[7:0]; + if (PORT_A_WR_EN[1]) + mem[PORT_A_ADDR][15:8] <= PORT_A_WR_DATA[15:8]; + end + if (PORT_A_RD_EN && (!PORT_A_WR_EN || OPTION_RDWR != "NO_CHANGE")) begin + PORT_A_RD_DATA <= mem[PORT_A_ADDR]; + if (PORT_A_WR_EN && OPTION_RDWR == "NEW_ONLY") + PORT_A_RD_DATA <= 16'hx; + if (PORT_A_WR_EN[0]) + case (OPTION_RDWR) + "NEW": PORT_A_RD_DATA[7:0] <= PORT_A_WR_DATA[7:0]; + "NEW_ONLY": PORT_A_RD_DATA[7:0] <= PORT_A_WR_DATA[7:0]; + "UNDEFINED": PORT_A_RD_DATA[7:0] <= 8'hx; + endcase + if (PORT_A_WR_EN[1]) + case (OPTION_RDWR) + "NEW": PORT_A_RD_DATA[15:8] <= PORT_A_WR_DATA[15:8]; + "NEW_ONLY": PORT_A_RD_DATA[15:8] <= PORT_A_WR_DATA[15:8]; + "UNDEFINED": PORT_A_RD_DATA[15:8] <= 8'hx; + endcase + end + end + if (PORT_A_RD_SRST && (!OPTION_SRST_GATE || (OPTION_SRST_GATE == 2 && PORT_A_RD_EN) || (OPTION_SRST_GATE == 1 && PORT_A_CLK_EN))) + PORT_A_RD_DATA <= SRST_VALUE; +end + +always @(PORT_A_RD_ARST) + if (PORT_A_RD_ARST) + force PORT_A_RD_DATA = ARST_VALUE; + else + release PORT_A_RD_DATA; + +endmodule diff --git a/tests/memlib/memlib_clock_sdp.txt b/tests/memlib/memlib_clock_sdp.txt new file mode 100644 index 000000000..00e911ef8 --- /dev/null +++ b/tests/memlib/memlib_clock_sdp.txt @@ -0,0 +1,76 @@ +ram block \RAM_CLOCK_SDP { + cost 64; + abits 10; + widths 1 2 4 8 16 per_port; + init any; + port sw "W" { + ifdef SHARED_CLK { + ifdef WCLK_ANY { + option "WCLK" "ANY" { + clock anyedge "CLK"; + } + } + ifdef WCLK_POS { + option "WCLK" "POS" { + clock posedge "CLK"; + } + } + ifdef WCLK_NEG { + option "WCLK" "NEG" { + clock negedge "CLK"; + } + } + } else { + ifdef WCLK_ANY { + option "WCLK" "ANY" { + clock anyedge; + } + } + ifdef WCLK_POS { + option "WCLK" "POS" { + clock posedge; + } + } + ifdef WCLK_NEG { + option "WCLK" "NEG" { + clock negedge; + } + } + } + } + port sr "R" { + ifdef SHARED_CLK { + ifdef RCLK_ANY { + option "RCLK" "ANY" { + clock anyedge "CLK"; + } + } + ifdef RCLK_POS { + option "RCLK" "POS" { + clock posedge "CLK"; + } + } + ifdef RCLK_NEG { + option "RCLK" "NEG" { + clock negedge "CLK"; + } + } + } else { + ifdef RCLK_ANY { + option "RCLK" "ANY" { + clock anyedge; + } + } + ifdef RCLK_POS { + option "RCLK" "POS" { + clock posedge; + } + } + ifdef RCLK_NEG { + option "RCLK" "NEG" { + clock negedge; + } + } + } + } +} diff --git a/tests/memlib/memlib_clock_sdp.v b/tests/memlib/memlib_clock_sdp.v new file mode 100644 index 000000000..e9036351e --- /dev/null +++ b/tests/memlib/memlib_clock_sdp.v @@ -0,0 +1,36 @@ +module RAM_CLOCK_SDP( + input CLK_CLK, + input PORT_R_CLK, + input [9:0] PORT_R_ADDR, + output reg [15:0] PORT_R_RD_DATA, + input PORT_W_CLK, + input PORT_W_WR_EN, + input [9:0] PORT_W_ADDR, + input [15:0] PORT_W_WR_DATA +); + +parameter INIT = 0; +parameter PORT_R_WIDTH = 1; +parameter PORT_W_WIDTH = 1; +parameter CLK_CLK_POL = 0; +parameter PORT_R_CLK_POL = 0; +parameter PORT_W_CLK_POL = 0; +parameter OPTION_WCLK = "ANY"; +parameter OPTION_RCLK = "ANY"; + +reg [2**10-1:0] mem = INIT; + +wire RCLK; +case (OPTION_RCLK) +"ANY": assign RCLK = PORT_R_CLK == PORT_R_CLK_POL; +"POS": assign RCLK = PORT_R_CLK; +"NEG": assign RCLK = ~PORT_R_CLK; +endcase +always @(posedge RCLK) + PORT_R_RD_DATA <= mem[PORT_R_ADDR+:PORT_R_WIDTH]; + +always @(negedge PORT_W_CLK ^ (PORT_W_CLK_POL || OPTION_WCLK == "POS")) + if (PORT_W_WR_EN) + mem[PORT_W_ADDR+:PORT_W_WIDTH] <= PORT_W_WR_DATA; + +endmodule diff --git a/tests/memlib/memlib_lut.txt b/tests/memlib/memlib_lut.txt index 0cc8fda15..9f6d84123 100644 --- a/tests/memlib/memlib_lut.txt +++ b/tests/memlib/memlib_lut.txt @@ -1,7 +1,23 @@ ram distributed \RAM_LUT { abits 4; width 4; - init any; + ifdef INIT_NONE { + option "INIT" "NONE" { + init none; + } + } else ifdef INIT_ZERO { + option "INIT" "ZERO" { + init zero; + } + } else ifdef INIT_NO_UNDEF { + option "INIT" "NO_UNDEF" { + init no_undef; + } + } else { + option "INIT" "ANY" { + init any; + } + } cost 4; port ar "R" { } diff --git a/tests/memlib/memlib_lut.v b/tests/memlib/memlib_lut.v index 1f20a110a..2685d2337 100644 --- a/tests/memlib/memlib_lut.v +++ b/tests/memlib/memlib_lut.v @@ -9,6 +9,7 @@ module RAM_LUT( ); parameter INIT = 0; +parameter OPTION_INIT = "UNDEFINED"; parameter PORT_RW_CLK_POL = 1; reg [3:0] mem [0:15]; @@ -16,7 +17,13 @@ reg [3:0] mem [0:15]; integer i; initial for (i = 0; i < 16; i += 1) - mem[i] = INIT[i*4+:4]; + case (OPTION_INIT) + "NONE": mem[i] = mem[i]; //? + "ZERO": mem[i] = 4'h0; + "ANY": mem[i] = INIT[i*4+:4]; + "NO_UNDEF": mem[i] = INIT[i*4+:4]; + "UNDEFINED": mem[i] = 4'hx; + endcase assign PORT_R_RD_DATA = mem[PORT_R_ADDR]; assign PORT_RW_RD_DATA = mem[PORT_RW_ADDR]; diff --git a/tests/memlib/memlib_multilut.txt b/tests/memlib/memlib_multilut.txt new file mode 100644 index 000000000..387f4f8e2 --- /dev/null +++ b/tests/memlib/memlib_multilut.txt @@ -0,0 +1,19 @@ +ram distributed \LUT_MULTI { + abits 4; + width 2; + init any; + port arsw "RW" { + clock posedge; + } + ifdef PORTS_QUAD { + option "PORTS" "QUAD" { + port ar "R0" "R1" "R2" { + } + } + } else ifdef PORTS_OCT { + option "PORTS" "OCT" { + port ar "R0" "R1" "R2" "R3" "R4" "R5" "R6" { + } + } + } +} diff --git a/tests/memlib/memlib_multilut.v b/tests/memlib/memlib_multilut.v new file mode 100644 index 000000000..a623d41fd --- /dev/null +++ b/tests/memlib/memlib_multilut.v @@ -0,0 +1,45 @@ +module LUT_MULTI( + input [3:0] PORT_R0_ADDR, + input [3:0] PORT_R1_ADDR, + input [3:0] PORT_R2_ADDR, + input [3:0] PORT_R3_ADDR, + input [3:0] PORT_R4_ADDR, + input [3:0] PORT_R5_ADDR, + input [3:0] PORT_R6_ADDR, + input [3:0] PORT_RW_ADDR, + input PORT_RW_CLK, + input PORT_RW_WR_EN, + input [1:0] PORT_RW_WR_DATA, + output [1:0] PORT_R0_RD_DATA, + output [1:0] PORT_R1_RD_DATA, + output [1:0] PORT_R2_RD_DATA, + output [1:0] PORT_R3_RD_DATA, + output [1:0] PORT_R4_RD_DATA, + output [1:0] PORT_R5_RD_DATA, + output [1:0] PORT_R6_RD_DATA, + output [1:0] PORT_RW_RD_DATA +); + +parameter INIT = 0; +parameter OPTION_PORTS = "UNDEFINED"; + +reg [1:0] mem [0:15]; +integer i; +initial + for (i = 0; i < 16; i += 1) + mem[i] = INIT[i*4+:4]; + +assign PORT_R0_RD_DATA = mem[PORT_R0_ADDR]; +assign PORT_R1_RD_DATA = mem[PORT_R1_ADDR]; +assign PORT_R2_RD_DATA = mem[PORT_R2_ADDR]; +assign PORT_R3_RD_DATA = mem[PORT_R3_ADDR]; +assign PORT_R4_RD_DATA = mem[PORT_R4_ADDR]; +assign PORT_R5_RD_DATA = mem[PORT_R5_ADDR]; +assign PORT_R6_RD_DATA = mem[PORT_R6_ADDR]; +assign PORT_RW_RD_DATA = mem[PORT_RW_ADDR]; + +always @(posedge PORT_RW_CLK) + if (PORT_RW_WR_EN) + mem[PORT_RW_ADDR] <= PORT_RW_WR_DATA; + +endmodule diff --git a/tests/memlib/memlib_wren.txt b/tests/memlib/memlib_wren.txt new file mode 100644 index 000000000..31ff3ff60 --- /dev/null +++ b/tests/memlib/memlib_wren.txt @@ -0,0 +1,37 @@ +ram block \RAM_WREN { + abits 4; + init none; + + ifdef NO_BYTE { + # single enable signal + widths 4 8 global; + } else ifdef W4_B4 { + widths 4 global; + byte 4; + } else ifdef W8_B4 { + widths 8 global; + option "BYTESIZE" 4 { + byte 4; + } + } else ifdef W8_B8 { + width 8; + byte 8; + } else ifdef W16_B4 { + widths 16 global; + option "BYTESIZE" 4 { + byte 4; + } + } else ifdef W64_B8 { + widths 64 global; + option "BYTESIZE" 8 { + byte 8; + } + } + + port srsw "A" { + clock posedge; + ifdef WRBE_SEPARATE { + wrbe_separate; + } + } +} diff --git a/tests/memlib/memlib_wren.v b/tests/memlib/memlib_wren.v new file mode 100644 index 000000000..b9433d42e --- /dev/null +++ b/tests/memlib/memlib_wren.v @@ -0,0 +1,33 @@ +module RAM_WREN ( + input PORT_A_CLK, + input [ABITS-1:0] PORT_A_ADDR, + input [WIDTH-1:0] PORT_A_WR_DATA, + output reg [WIDTH-1:0] PORT_A_RD_DATA, + input [PORT_A_WR_EN_WIDTH-1:0] PORT_A_WR_EN, + input [PORT_A_WR_BE_WIDTH-1:0] PORT_A_WR_BE +); + +parameter ABITS=4; +parameter WIDTH=8; +parameter PORT_A_WR_EN_WIDTH=1; +parameter PORT_A_WR_BE_WIDTH=0; +parameter OPTION_BYTESIZE=WIDTH; +parameter WB=OPTION_BYTESIZE; + +reg [WIDTH-1:0] mem [0:2**ABITS-1]; + +integer i; +always @(posedge PORT_A_CLK) begin + for (i=0; i<PORT_A_WR_EN_WIDTH; i=i+1) // use PORT_A_WR_EN + if (!PORT_A_WR_BE_WIDTH && PORT_A_WR_EN[i]) + mem[PORT_A_ADDR][i*WB+:WB] <= PORT_A_WR_DATA[i*WB+:WB]; + for (i=0; i<PORT_A_WR_BE_WIDTH; i=i+1) // use PORT_A_WR_BE + if (PORT_A_WR_EN[0] && PORT_A_WR_BE[i]) + mem[PORT_A_ADDR][i*WB+:WB] <= PORT_A_WR_DATA[i*WB+:WB]; +end + +always @(posedge PORT_A_CLK) + if (!PORT_A_WR_EN[0]) + PORT_A_RD_DATA <= mem[PORT_A_ADDR]; + +endmodule diff --git a/tests/svinterfaces/resolve_types.sv b/tests/svinterfaces/resolve_types.sv new file mode 100644 index 000000000..3c6644e33 --- /dev/null +++ b/tests/svinterfaces/resolve_types.sv @@ -0,0 +1,24 @@ +// This test checks that types, including package types, are resolved from within an interface. + +typedef logic [7:0] x_t; + +package pkg; + typedef logic [7:0] y_t; +endpackage + +interface iface; + x_t x; + pkg::y_t y; +endinterface + +module dut (input logic [7:0] x, output logic [7:0] y); + iface intf(); + assign intf.x = x; + assign y = intf.y; + + ondemand u(.intf); +endmodule + +module ref (input logic [7:0] x, output logic [7:0] y); + assign y = ~x; +endmodule diff --git a/tests/svinterfaces/resolve_types.ys b/tests/svinterfaces/resolve_types.ys new file mode 100644 index 000000000..a25791f37 --- /dev/null +++ b/tests/svinterfaces/resolve_types.ys @@ -0,0 +1,6 @@ +read_verilog -sv resolve_types.sv +hierarchy -libdir . -check +flatten +equiv_make ref dut equiv +equiv_simple +equiv_status -assert diff --git a/tests/svinterfaces/run-test.sh b/tests/svinterfaces/run-test.sh index 9ef53926c..afa222766 100755 --- a/tests/svinterfaces/run-test.sh +++ b/tests/svinterfaces/run-test.sh @@ -4,3 +4,4 @@ ./runone.sh svinterface_at_top ./run_simple.sh load_and_derive +./run_simple.sh resolve_types diff --git a/tests/svtypes/struct_array.sv b/tests/svtypes/struct_array.sv index 739f202ab..a0b84640d 100644 --- a/tests/svtypes/struct_array.sv +++ b/tests/svtypes/struct_array.sv @@ -141,6 +141,26 @@ module top; always_comb assert(s3_llb==80'hFC00_4200_0012_3400_FFFC); + struct packed { + bit [-10:-3] [-2:-1] [5:2] a; + bit [0:15] b; // filler for non-zero offset + } s3_off; + + initial begin + s3_off = '0; + + s3_off.a[-5:-4] = 16'h1234; + s3_off.a[-8] = 8'h42; + + s3_off.a[-10] = '1; + s3_off.a[-10][-1][3:0] = '0; + + s3_off.b = '1; + s3_off.b[14:15] = '0; + end + + always_comb assert(s3_off==80'hFC00_4200_0012_3400_FFFC); + `ifndef VERIFIC // Note that the tests below for unpacked arrays in structs rely on the // fact that they are actually packed in Yosys. diff --git a/tests/svtypes/struct_sizebits.sv b/tests/svtypes/struct_sizebits.sv new file mode 100644 index 000000000..092d9ecef --- /dev/null +++ b/tests/svtypes/struct_sizebits.sv @@ -0,0 +1,112 @@ +// These tests are adapted from tests/sat/sizebits.sv + +module top; + +typedef struct packed { + logic [2:7][3:0] y; +} sy_t; + +struct packed { + logic t; + logic [5:2] x; + sy_t sy; + union packed { + logic [7:2][2:9][1:4] z; + logic [1:6*8*4] z2; + } sz; +} s; + +//wire [$size(s.x)-1:0]x_size; +//wire [$size({s.x, s.x})-1:0]xx_size; +//wire [$size(s.sy.y)-1:0]y_size; +//wire [$size(s.sz.z)-1:0]z_size; + +//wire [$bits(s.x)-1:0]x_bits; +//wire [$bits({s.x, s.x})-1:0]xx_bits; + +always_comb begin + assert ($size(s) == $size(s.t) + $size(s.x) + $size(s.sy) + $size(s.sz)); + assert ($size(s) == 1 + 4 + 6*4 + 6*8*4); + + assert ($size(s.t) == 1); + assert ($size(s.x) == 4); +`ifndef VERIFIC + assert ($size({3{s.x}}) == 3*4); +`endif + assert ($size(s.sy.y) == 6); + assert ($size(s.sy.y, 1) == 6); + assert ($size(s.sy.y, (1+1)) == 4); + assert ($size(s.sy.y[2], 1) == 4); + // This is unsupported at the moment + // assert ($size(s.sy.y[2][1], 1) == 1); + + assert ($size(s.sz.z) == 6); + assert ($size(s.sz.z, 1) == 6); + assert ($size(s.sz.z, 2) == 8); + assert ($size(s.sz.z, 3) == 4); + assert ($size(s.sz.z[3], 1) == 8); + assert ($size(s.sz.z[3][3], 1) == 4); + // This is unsupported at the moment + // assert ($size(s.sz.z[3][3][3], 1) == 1); + // This should trigger an error if enabled (it does). + // assert ($size(s.sz.z, 4) == 4); + + assert ($bits(s.t) == 1); + assert ($bits(s.x) == 4); + assert ($bits(s.sy.y) == 4*6); + assert ($bits(s.sz.z) == 4*6*8); + + assert ($high(s.x) == 5); + assert ($high(s.sy.y) == 7); + assert ($high(s.sy.y, 1) == 7); + assert ($high(s.sy.y, (1+1)) == 3); + + assert ($high(s.sz.z) == 7); + assert ($high(s.sz.z, 1) == 7); + assert ($high(s.sz.z, 2) == 9); + assert ($high(s.sz.z, 3) == 4); + assert ($high(s.sz.z[3]) == 9); + assert ($high(s.sz.z[3][3]) == 4); + assert ($high(s.sz.z[3], 2) == 4); + + assert ($low(s.x) == 2); + assert ($low(s.sy.y) == 2); + assert ($low(s.sy.y, 1) == 2); + assert ($low(s.sy.y, (1+1)) == 0); + + assert ($low(s.sz.z) == 2); + assert ($low(s.sz.z, 1) == 2); + assert ($low(s.sz.z, 2) == 2); + assert ($low(s.sz.z, 3) == 1); + assert ($low(s.sz.z[3]) == 2); + assert ($low(s.sz.z[3][3]) == 1); + assert ($low(s.sz.z[3], 2) == 1); + + assert ($left(s.x) == 5); + assert ($left(s.sy.y) == 2); + assert ($left(s.sy.y, 1) == 2); + assert ($left(s.sy.y, (1+1)) == 3); + + assert ($left(s.sz.z) == 7); + assert ($left(s.sz.z, 1) == 7); + assert ($left(s.sz.z, 2) == 2); + assert ($left(s.sz.z, 3) == 1); + assert ($left(s.sz.z[3]) == 2); + assert ($left(s.sz.z[3][3]) == 1); + assert ($left(s.sz.z[3], 2) == 1); + + assert ($right(s.x) == 2); + assert ($right(s.sy.y) == 7); + assert ($right(s.sy.y, 1) == 7); + assert ($right(s.sy.y, (1+1)) == 0); + + assert ($right(s.sz.z) == 2); + assert ($right(s.sz.z, 1) == 2); + assert ($right(s.sz.z, 2) == 9); + assert ($right(s.sz.z, 3) == 4); + assert ($right(s.sz.z[3]) == 9); + assert ($right(s.sz.z[3][3]) == 4); + assert ($right(s.sz.z[3], 2) == 4); +end + +endmodule diff --git a/tests/svtypes/typedef_struct.sv b/tests/svtypes/typedef_struct.sv index 7ae007952..8df8e32b0 100644 --- a/tests/svtypes/typedef_struct.sv +++ b/tests/svtypes/typedef_struct.sv @@ -16,6 +16,7 @@ module top; bit a; logic[7:0] b; t_t t; + p::p_t ps; } s_t; s_t s; @@ -29,6 +30,7 @@ module top; assign s1 = s; assign ps.a = 8'hAA; assign ps.b = 8'h55; + assign s.ps = ps; always_comb begin assert(s.a == 1'b1); @@ -37,6 +39,8 @@ module top; assert(s1.t == 8'h55); assert(ps.a == 8'hAA); assert(ps.b == 8'h55); + assert(s.ps.a == 8'hAA); + assert(s.ps.b == 8'h55); end endmodule diff --git a/tests/svtypes/union_simple.sv b/tests/svtypes/union_simple.sv index 12e4b376f..a55df4d0a 100644 --- a/tests/svtypes/union_simple.sv +++ b/tests/svtypes/union_simple.sv @@ -48,14 +48,30 @@ module top; U_t u; } instruction_t; + typedef struct packed { + instruction_t ir; + logic [3:0] state; + } s_t; + instruction_t ir1; + s_t s1; + assign ir1 = 32'h0AA01EB7; // lui t4,0xAA01 + assign s1.ir = ir1; + assign s1.state = '1; + always_comb begin assert(ir1.u.opcode == 'h37); assert(ir1.r.opcode == 'h37); assert(ir1.u.rd == 'd29); assert(ir1.r.rd == 'd29); assert(ir1.u.imm == 'hAA01); + assert(s1.ir.u.opcode == 'h37); + assert(s1.ir.r.opcode == 'h37); + assert(s1.ir.u.rd == 'd29); + assert(s1.ir.r.rd == 'd29); + assert(s1.ir.u.imm == 'hAA01); + assert(s1.state == 4'b1111); end union packed { diff --git a/tests/techmap/bmuxmap_pmux.ys b/tests/techmap/bmuxmap_pmux.ys new file mode 100644 index 000000000..c75d981e7 --- /dev/null +++ b/tests/techmap/bmuxmap_pmux.ys @@ -0,0 +1,45 @@ +read_ilang << EOT + +module \top + wire width 4 input 0 \S + wire width 5 output 1 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 4 + connect \A 80'10110100011101110001110010001110101010111000110011111111111110100000110100111000 + connect \S \S + connect \Y \Y + end +end + +EOT + +hierarchy -auto-top +equiv_opt -assert bmuxmap -pmux + +### +design -reset + +read_ilang << EOT + +module \top + wire width 10 input 0 \A + wire input 1 \S + wire width 5 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 1 + connect \A \A + connect \S \S + connect \Y \Y + end +end + +EOT + +hierarchy -auto-top +equiv_opt -assert bmuxmap -pmux + + diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys new file mode 100644 index 000000000..52b3ee6bf --- /dev/null +++ b/tests/various/chformal_coverenable.ys @@ -0,0 +1,25 @@ +read_verilog -formal <<EOT +module top(input a, b, c, d); + + always @* begin + if (a) assert (b == c); + if (!a) assert (b != c); + if (b) assume (c); + if (c) cover (d); + end + +endmodule +EOT + +prep -top top + +select -assert-count 1 t:$cover + +chformal -cover -coverenable +select -assert-count 2 t:$cover + +chformal -assert -coverenable +select -assert-count 4 t:$cover + +chformal -assume -coverenable +select -assert-count 5 t:$cover diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys new file mode 100644 index 000000000..1c2efa723 --- /dev/null +++ b/tests/various/equiv_make_make_assert.ys @@ -0,0 +1,32 @@ +read_verilog <<EOT +module gold( + input wire [7:0] a, + input wire [7:0] b, + output wire [7:0] c +); + +wire [7:0] b_neg; +assign b_neg = -b; +assign c = a + b_neg; +endmodule + +module gate( + input wire [7:0] a, + input wire [7:0] b, + output wire [7:0] c +); + +wire [7:0] b_neg; +assign b_neg = ~b + 1; +assign c = a + b_neg; +endmodule + +EOT + +equiv_make -make_assert gold gate miter + +select -assert-count 0 t:$equiv +select -assert-count 2 t:$assert + +prep -top miter +sat -prove-asserts -verify diff --git a/tests/various/rtlil_z_bits.ys b/tests/various/rtlil_z_bits.ys new file mode 100644 index 000000000..c38669159 --- /dev/null +++ b/tests/various/rtlil_z_bits.ys @@ -0,0 +1,9 @@ +! mkdir -p temp +read_rtlil <<EOT +module \test + wire output 1 \a + connect \a 1'z +end +EOT +write_rtlil temp/rtlil_z_bits.il +! grep -F -q "connect \\a 1'z" temp/rtlil_z_bits.il diff --git a/tests/verific/.gitignore b/tests/verific/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/verific/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/verific/case.sv b/tests/verific/case.sv new file mode 100644 index 000000000..ed8529b91 --- /dev/null +++ b/tests/verific/case.sv @@ -0,0 +1,28 @@ +module top ( + input clk, + input [5:0] currentstate, + output reg [1:0] o + ); + always @ (posedge clk) + begin + case (currentstate) + 5'd1,5'd2, 5'd3: + begin + o <= 2'b01; + end + 5'd4: + begin + o <= 2'b10; + end + 5'd5,5'd6,5'd7: + begin + o <= 2'b11; + end + default : + begin + o <= 2'b00; + end + endcase + end +endmodule + diff --git a/tests/verific/case.ys b/tests/verific/case.ys new file mode 100644 index 000000000..a181b39cf --- /dev/null +++ b/tests/verific/case.ys @@ -0,0 +1,16 @@ +verific -cfg db_abstract_case_statement_synthesis 0 +read -sv case.sv +verific -import top +prep +rename top gold + +verific -cfg db_abstract_case_statement_synthesis 1 +read -sv case.sv +verific -import top +prep +rename top gate + +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verific/range_case.sv b/tests/verific/range_case.sv new file mode 100644 index 000000000..9843feafe --- /dev/null +++ b/tests/verific/range_case.sv @@ -0,0 +1,11 @@ +module top(input clk, input signed [3:0] sel_w , output reg out); + +always @ (posedge clk) +begin + case (sel_w) inside + [-4:3] : out <= 1'b1; + [4:5] : out <= 1'b0; + endcase +end + +endmodule diff --git a/tests/verific/range_case.ys b/tests/verific/range_case.ys new file mode 100644 index 000000000..27afbbc17 --- /dev/null +++ b/tests/verific/range_case.ys @@ -0,0 +1,16 @@ +verific -cfg db_abstract_case_statement_synthesis 0 +read -sv range_case.sv +verific -import top +proc +rename top gold + +verific -cfg db_abstract_case_statement_synthesis 1 +read -sv range_case.sv +verific -import top +proc +rename top gate + +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verific/run-test.sh b/tests/verific/run-test.sh new file mode 100755 index 000000000..2f91cf0fd --- /dev/null +++ b/tests/verific/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts --bash diff --git a/tests/verilog/typedef_const_shadow.sv b/tests/verilog/typedef_const_shadow.sv new file mode 100644 index 000000000..e2c331be1 --- /dev/null +++ b/tests/verilog/typedef_const_shadow.sv @@ -0,0 +1,12 @@ +module top; + localparam W = 5; + typedef logic [W-1:0] T; + T x; // width 5 + if (1) begin : blk + localparam W = 10; + typedef T U; + typedef logic [W-1:0] V; + U y; // width 5 + V z; // width 10 + end +endmodule diff --git a/tests/verilog/typedef_const_shadow.ys b/tests/verilog/typedef_const_shadow.ys new file mode 100644 index 000000000..ecf47181d --- /dev/null +++ b/tests/verilog/typedef_const_shadow.ys @@ -0,0 +1,4 @@ +read_verilog -sv typedef_const_shadow.sv +select -assert-count 1 w:x s:5 %i +select -assert-count 1 w:blk.y s:5 %i +select -assert-count 1 w:blk.z s:10 %i diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py index eef8dc36e..484f1661c 100644 --- a/tests/xprop/generate.py +++ b/tests/xprop/generate.py @@ -6,6 +6,7 @@ import argparse parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter) parser.add_argument('-S', '--seed', type=int, help='seed for PRNG') +parser.add_argument('-m', '--more', action='store_true', help='run more tests') parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test') parser.add_argument('-f', '--filter', default='', help='regular expression to filter tests to generate') args = parser.parse_args() @@ -32,7 +33,7 @@ def add_test(name, src, seq=False): print( f"\t@cd {workdir} && python3 -u ../test.py -S {args.seed} -c {args.count}{seq_arg} > test.log 2>&1 || echo {workdir}: failed > status\n" f"\t@cat {workdir}/status\n" - # f"\t@grep '^.*: ok' {workdir}/status\n" + f"\t@grep '^.*: ok' {workdir}/status\n" , file=makefile, ) @@ -123,50 +124,55 @@ print(".PHONY: all", file=makefile) print("all:\n\t@echo done\n", file=makefile) for cell in ["not", "pos", "neg"]: - unary_test(cell, 1, False, 1) - unary_test(cell, 3, False, 3) - unary_test(cell, 3, True, 3) - unary_test(cell, 3, True, 1) - unary_test(cell, 3, False, 5) + if args.more: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 3) + unary_test(cell, 3, True, 3) + unary_test(cell, 3, True, 1) + unary_test(cell, 3, False, 5) unary_test(cell, 3, True, 5) for cell in ["and", "or", "xor", "xnor"]: binary_test(cell, 1, 1, False, 1) binary_test(cell, 1, 1, True, 2) binary_test(cell, 2, 2, False, 2) - binary_test(cell, 2, 2, False, 1) - binary_test(cell, 2, 1, False, 2) - binary_test(cell, 2, 1, False, 1) + if args.more: + binary_test(cell, 2, 2, False, 1) + binary_test(cell, 2, 1, False, 2) + binary_test(cell, 2, 1, False, 1) # [, "pow"] are not implemented yet for cell in ["add", "sub", "mul", "div", "mod", "divfloor", "modfloor"]: - binary_test(cell, 1, 1, False, 1) - binary_test(cell, 1, 1, False, 2) - binary_test(cell, 3, 3, False, 1) - binary_test(cell, 3, 3, False, 3) - binary_test(cell, 3, 3, False, 6) - binary_test(cell, 3, 3, True, 1) - binary_test(cell, 3, 3, True, 3) - binary_test(cell, 3, 3, True, 6) + if args.more: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, False, 2) + binary_test(cell, 3, 3, False, 1) + binary_test(cell, 3, 3, False, 3) + binary_test(cell, 3, 3, False, 6) + binary_test(cell, 3, 3, True, 1) + binary_test(cell, 3, 3, True, 3) + binary_test(cell, 3, 3, True, 6) binary_test(cell, 5, 3, False, 3) binary_test(cell, 5, 3, True, 3) for cell in ["lt", "le", "eq", "ne", "eqx", "nex", "ge", "gt"]: - binary_test(cell, 1, 1, False, 1) - binary_test(cell, 1, 1, False, 2) - binary_test(cell, 3, 3, False, 1) - binary_test(cell, 3, 3, False, 2) - binary_test(cell, 3, 3, True, 1) - binary_test(cell, 3, 3, True, 2) - binary_test(cell, 5, 3, False, 1) - binary_test(cell, 5, 3, True, 1) + if args.more: + binary_test(cell, 1, 1, False, 1) + binary_test(cell, 1, 1, False, 2) + binary_test(cell, 3, 3, False, 1) + binary_test(cell, 3, 3, False, 2) + binary_test(cell, 3, 3, True, 1) + binary_test(cell, 3, 3, True, 2) + binary_test(cell, 5, 3, False, 1) + binary_test(cell, 5, 3, True, 1) binary_test(cell, 5, 3, False, 2) binary_test(cell, 5, 3, True, 2) for cell in ["reduce_and", "reduce_or", "reduce_xor", "reduce_xnor"]: - unary_test(cell, 1, False, 1) - unary_test(cell, 3, False, 1) - unary_test(cell, 3, True, 1) + if args.more: + unary_test(cell, 1, False, 1) + unary_test(cell, 3, False, 1) + unary_test(cell, 3, True, 1) unary_test(cell, 3, False, 3) unary_test(cell, 3, True, 3) @@ -183,33 +189,36 @@ for cell in ["logic_and", "logic_or"]: binary_test(cell, 3, 3, True, 1) for cell in ["shl", "shr", "sshl", "sshr", "shift"]: - shift_test(cell, 2, 1, False, False, 2) - shift_test(cell, 2, 1, True, False, 2) - shift_test(cell, 2, 1, False, False, 4) - shift_test(cell, 2, 1, True, False, 4) - shift_test(cell, 4, 2, False, False, 4) - shift_test(cell, 4, 2, True, False, 4) - shift_test(cell, 4, 2, False, False, 8) - shift_test(cell, 4, 2, True, False, 8) + if args.more: + shift_test(cell, 2, 1, False, False, 2) + shift_test(cell, 2, 1, True, False, 2) + shift_test(cell, 2, 1, False, False, 4) + shift_test(cell, 2, 1, True, False, 4) + shift_test(cell, 4, 2, False, False, 4) + shift_test(cell, 4, 2, True, False, 4) + shift_test(cell, 4, 2, False, False, 8) + shift_test(cell, 4, 2, True, False, 8) shift_test(cell, 4, 3, False, False, 3) shift_test(cell, 4, 3, True, False, 3) for cell in ["shift"]: - shift_test(cell, 2, 1, False, True, 2) - shift_test(cell, 2, 1, True, True, 2) - shift_test(cell, 2, 1, False, True, 4) - shift_test(cell, 2, 1, True, True, 4) - shift_test(cell, 4, 2, False, True, 4) - shift_test(cell, 4, 2, True, True, 4) + if args.more: + shift_test(cell, 2, 1, False, True, 2) + shift_test(cell, 2, 1, True, True, 2) + shift_test(cell, 2, 1, False, True, 4) + shift_test(cell, 2, 1, True, True, 4) + shift_test(cell, 4, 2, False, True, 4) + shift_test(cell, 4, 2, True, True, 4) shift_test(cell, 4, 2, False, True, 8) shift_test(cell, 4, 2, True, True, 8) shift_test(cell, 4, 3, False, True, 3) shift_test(cell, 4, 3, True, True, 3) for cell in ["shiftx"]: - shift_test(cell, 2, 1, False, True, 2) - shift_test(cell, 2, 1, False, True, 4) - shift_test(cell, 4, 2, False, True, 4) + if args.more: + shift_test(cell, 2, 1, False, True, 2) + shift_test(cell, 2, 1, False, True, 4) + shift_test(cell, 4, 2, False, True, 4) shift_test(cell, 4, 2, False, True, 8) shift_test(cell, 4, 3, False, True, 3) diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh index 1fc7e10b6..db4b7ca82 100755 --- a/tests/xprop/run-test.sh +++ b/tests/xprop/run-test.sh @@ -2,4 +2,4 @@ set -e python3 generate.py $@ -make -f run-test.mk +${MAKE:-make} -f run-test.mk diff --git a/tests/xprop/test.py b/tests/xprop/test.py index 84ad0a1f4..a275b0d93 100644 --- a/tests/xprop/test.py +++ b/tests/xprop/test.py @@ -47,7 +47,7 @@ if "clean" in steps: def yosys(command): - subprocess.check_call(["yosys", "-Qp", command]) + subprocess.check_call(["../../../yosys", "-Qp", command]) def remove(file): try: @@ -275,7 +275,7 @@ if "prepare" in steps: file=tb_file, ) - print(" $finish;", file=tb_file) + print(" $finish(0);", file=tb_file) print("end", file=tb_file) print("endmodule", file=tb_file) @@ -344,8 +344,8 @@ for mode in ["", "_xprop"]: read_rtlil wrapped{mode}.il chformal -remove dffunmap - write_verilog -noparallelcase vsim_expr{mode}.v write_verilog -noexpr vsim_noexpr{mode}.v + write_verilog -noparallelcase vsim_expr{mode}.v """ ) @@ -357,15 +357,15 @@ for mode in ["", "_xprop"]: "-DSIMLIB_FF", "-DSIMLIB_GLOBAL_CLOCK=top.gclk", f"-DDUMPFILE=\"vsim_{expr}.vcd\"", + "-o", + f"vsim_{expr}", "verilog_sim_tb.v", f"vsim_{expr}.v", *simlibs, - "-o", - f"vsim_{expr}", ] ) with open(f"vsim_{expr}.out", "w") as f: - subprocess.check_call([f"./vsim_{expr}"], stdout=f) + subprocess.check_call(["vvp", f"./vsim_{expr}"], stdout=f) for mode in ["", "_xprop"]: if f"sim{mode}" not in steps: |