diff options
| -rw-r--r-- | CHANGELOG | 17 | ||||
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | backends/json/json.cc | 17 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 6 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 5 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 10 | ||||
| -rw-r--r-- | frontends/json/jsonparse.cc | 34 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 5 | ||||
| -rw-r--r-- | kernel/fstdata.cc | 22 | ||||
| -rw-r--r-- | kernel/fstdata.h | 1 | ||||
| -rw-r--r-- | manual/command-reference-manual.tex | 97 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 555 | ||||
| -rw-r--r-- | techlibs/gowin/cells_sim.v | 10 | ||||
| -rw-r--r-- | tests/various/.gitignore | 1 | ||||
| -rw-r--r-- | tests/various/json_escape_chars.ys | 14 |
15 files changed, 644 insertions, 158 deletions
@@ -2,9 +2,17 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.14 .. Yosys 0.14-dev +Yosys 0.15 .. Yosys 0.15-dev -------------------------- +Yosys 0.14 .. Yosys 0.15 +-------------------------- + + * Various + - clk2fflogic: nice names for autogenerated signals + - simulation include support for all flip-flop types. + - Added AIGER witness file co-simulation. + * Verilog - Fixed evaluation of constant functions with variables or arguments with reversed dimensions @@ -14,6 +22,13 @@ Yosys 0.14 .. Yosys 0.14-dev * SystemVerilog - Added support for accessing whole sub-structures in expressions + + * New commands and options + - Added glift command, used to create gate-level information flow tracking + (GLIFT) models by the "constructive mapping" approach + + * Verific support + - Ability to override default parser mode for verific -f command. Yosys 0.13 .. Yosys 0.14 -------------------------- @@ -129,12 +129,12 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.14+51 +YOSYS_VER := 0.15+7 GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline a4522d6.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 07a4368.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -142,7 +142,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 = b4790a6 +ABCREV = d7ecb23 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 VERBOSE=$(Q) @@ -916,7 +916,7 @@ clean: rm -rf tests/simple/*.out tests/simple/*.log rm -rf tests/memories/*.out tests/memories/*.log tests/memories/*.dmp rm -rf tests/sat/*.log tests/techmap/*.log tests/various/*.log - rm -rf tests/bram/temp tests/fsm/temp tests/realmath/temp tests/share/temp tests/smv/temp + rm -rf tests/bram/temp tests/fsm/temp tests/realmath/temp tests/share/temp tests/smv/temp tests/various/temp rm -rf vloghtb/Makefile vloghtb/refdat vloghtb/rtl vloghtb/scripts vloghtb/spec vloghtb/check_yosys vloghtb/vloghammer_tb.tar.bz2 vloghtb/temp vloghtb/log_test_* rm -f tests/svinterfaces/*.log_stdout tests/svinterfaces/*.log_stderr tests/svinterfaces/dut_result.txt tests/svinterfaces/reference_result.txt tests/svinterfaces/a.out tests/svinterfaces/*_syn.v tests/svinterfaces/*.diff rm -f tests/tools/cmp_tbdata diff --git a/backends/json/json.cc b/backends/json/json.cc index 02532c39d..270d762ee 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -52,8 +52,23 @@ struct JsonWriter string newstr = "\""; for (char c : str) { if (c == '\\') + newstr += "\\\\"; + else if (c == '"') + newstr += "\\\""; + else if (c == '\b') + newstr += "\\b"; + else if (c == '\f') + newstr += "\\f"; + else if (c == '\n') + newstr += "\\n"; + else if (c == '\r') + newstr += "\\r"; + else if (c == '\t') + newstr += "\\t"; + else if (c < 0x20) + newstr += stringf("\\u%04X", c); + else newstr += c; - newstr += c; } return newstr + "\""; } diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a928419a1..9bf0de03e 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -985,8 +985,10 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell); - decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); + if (cell->name[0] == '$' && cell->attributes.count(ID::src)) + decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); + else + decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); if (cell->type == ID($cover)) decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e5cfcdc08..7e0d8f571 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -583,7 +583,10 @@ if aimfile is not None: if not got_topt: skip_steps = max(skip_steps, step) - num_steps = max(num_steps, step+1) + # some solvers optimize the properties so that they fail one cycle early, + # thus we check the properties in the cycle the aiger witness ends, and + # if that doesn't work, we check the cycle after that as well. + num_steps = max(num_steps, step+2) step += 1 if btorwitfile is not None: diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index d73a875ba..3d458e6cf 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -536,10 +536,16 @@ class SmtIo: self.modinfo[self.curmod].clocks[fields[2]] = "event" if fields[1] == "yosys-smt2-assert": - self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3] + if len(fields) > 4: + self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-cover": - self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if len(fields) > 4: + self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-maximize": self.modinfo[self.curmod].maximize.add(fields[2]) diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc index 50c25abda..1aab81015 100644 --- a/frontends/json/jsonparse.cc +++ b/frontends/json/jsonparse.cc @@ -60,10 +60,38 @@ struct JsonNode break; if (ch == '\\') { - int ch = f.get(); + ch = f.get(); - if (ch == EOF) - log_error("Unexpected EOF in JSON string.\n"); + switch (ch) { + case EOF: log_error("Unexpected EOF in JSON string.\n"); break; + case '"': + case '/': + case '\\': break; + case 'b': ch = '\b'; break; + case 'f': ch = '\f'; break; + case 'n': ch = '\n'; break; + case 'r': ch = '\r'; break; + case 't': ch = '\t'; break; + case 'u': + int val = 0; + for (int i = 0; i < 4; i++) { + ch = f.get(); + val <<= 4; + if (ch >= '0' && '9' >= ch) { + val += ch - '0'; + } else if (ch >= 'A' && 'F' >= ch) { + val += 10 + ch - 'A'; + } else if (ch >= 'a' && 'f' >= ch) { + val += 10 + ch - 'a'; + } else + log_error("Unexpected non-digit character in \\uXXXX sequence: %c.\n", ch); + } + if (val < 128) + ch = val; + else + log_error("Unsupported \\uXXXX sequence in JSON string: %04X.\n", val); + break; + } } data_string += ch; diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 17dbed067..8c2f7f0da 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -169,7 +169,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att FOREACH_ATTRIBUTE(obj, mi, attr) { if (attr->Key()[0] == ' ' || attr->Value() == nullptr) continue; - attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); + std::string val = std::string(attr->Value()); + if (val.size()>1 && val[0]=='\"' && val.back()=='\"') + val = val.substr(1,val.size()-2); + attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(val); } if (nl) { diff --git a/kernel/fstdata.cc b/kernel/fstdata.cc index 1386a3300..587678ce3 100644 --- a/kernel/fstdata.cc +++ b/kernel/fstdata.cc @@ -22,12 +22,29 @@ USING_YOSYS_NAMESPACE +static std::string file_base_name(std::string const & path) +{ + return path.substr(path.find_last_of("/\\") + 1); +} + FstData::FstData(std::string filename) : ctx(nullptr) { + #if !defined(YOSYS_DISABLE_SPAWN) + std::string filename_trim = file_base_name(filename); + if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0) { + filename_trim.erase(filename_trim.size()-4); + tmp_file = stringf("/tmp/converted_%s.fst", filename_trim.c_str()); + std::string cmd = stringf("vcd2fst %s %s", filename.c_str(), tmp_file.c_str()); + log("Exec: %s\n", cmd.c_str()); + if (run_command(cmd) != 0) + log_cmd_error("Shell command failed!\n"); + filename = tmp_file; + } + #endif const std::vector<std::string> g_units = { "s", "ms", "us", "ns", "ps", "fs", "as", "zs" }; ctx = (fstReaderContext *)fstReaderOpen(filename.c_str()); if (!ctx) - log_error("Error opening '%s'\n", filename.c_str()); + log_error("Error opening '%s' as FST file\n", filename.c_str()); int scale = (int)fstReaderGetTimescale(ctx); timescale = pow(10.0, scale); timescale_str = ""; @@ -53,6 +70,8 @@ FstData::~FstData() { if (ctx) fstReaderClose(ctx); + if (!tmp_file.empty()) + remove(tmp_file.c_str()); } uint64_t FstData::getStartTime() { return fstReaderGetStartTime(ctx); } @@ -184,6 +203,7 @@ void FstData::reconstructAllAtTimes(std::vector<fstHandle> &signal, uint64_t sta fstReaderSetUnlimitedTimeRange(ctx); fstReaderSetFacProcessMaskAll(ctx); fstReaderIterBlocks2(ctx, reconstruct_clb_attimes, reconstruct_clb_varlen_attimes, this, nullptr); + past_data = last_data; callback(last_time); if (last_time!=end_time) callback(end_time); diff --git a/kernel/fstdata.h b/kernel/fstdata.h index 707d1b64e..4a355fd77 100644 --- a/kernel/fstdata.h +++ b/kernel/fstdata.h @@ -74,6 +74,7 @@ private: CallbackFunction callback; std::vector<fstHandle> clk_signals; bool all_samples; + std::string tmp_file; }; YOSYS_NAMESPACE_END diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 1aa0facb5..e3055c0bc 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -2222,6 +2222,89 @@ one-hot encoding and binary encoding is supported. .map <old_bitpattern> <new_bitpattern> \end{lstlisting} +\section{glift -- create GLIFT models and optimization problems} +\label{cmd:glift} +\begin{lstlisting}[numbers=left,frame=single] + glift <command> [options] [selection] + +Augments the current or specified module with gate-level information flow tracking +(GLIFT) logic using the "constructive mapping" approach. Also can set up QBF-SAT +optimization problems in order to optimize GLIFT models or trade off precision and +complexity. + + +Commands: + + -create-precise-model + Replaces the current or specified module with one that has corresponding "taint" + inputs, outputs, and internal nets along with precise taint tracking logic. + For example, precise taint tracking logic for an AND gate is: + + y_t = a & b_t | b & a_t | a_t & b_t + + + -create-imprecise-model + Replaces the current or specified module with one that has corresponding "taint" + inputs, outputs, and internal nets along with imprecise "All OR" taint tracking + logic: + + y_t = a_t | b_t + + + -create-instrumented-model + Replaces the current or specified module with one that has corresponding "taint" + inputs, outputs, and internal nets along with 4 varying-precision versions of taint + tracking logic. Which version of taint tracking logic is used for a given gate is + determined by a MUX selected by an $anyconst cell. By default, unless the + `-no-cost-model` option is provided, an additional wire named `__glift_weight` with + the `keep` and `minimize` attributes is added to the module along with pmuxes and + adders to calculate a rough estimate of the number of logic gates in the GLIFT model + given an assignment for the $anyconst cells. The four versions of taint tracking logic + for an AND gate are: + y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`) + y_t = a_t | a & b_t + y_t = b_t | b & a_t + y_t = a_t | b_t (like `-create-imprecise-model`) + + +Options: + + -taint-constants + Constant values in the design are labeled as tainted. + (default: label constants as un-tainted) + + -keep-outputs + Do not remove module outputs. Taint tracking outputs will appear in the module ports + alongside the orignal outputs. + (default: original module outputs are removed) + + -simple-cost-model + Do not model logic area. Instead model the number of non-zero assignments to $anyconsts. + Taint tracking logic versions vary in their size, but all reduced-precision versions are + significantly smaller than the fully-precise version. A non-zero $anyconst assignment means + that reduced-precision taint tracking logic was chosen for some gate. + Only applicable in combination with `-create-instrumented-model`. + (default: use a complex model and give that wire the "keep" and "minimize" attributes) + + -no-cost-model + Do not model taint tracking logic area and do not create a `__glift_weight` wire. + Only applicable in combination with `-create-instrumented-model`. + (default: model area and give that wire the "keep" and "minimize" attributes) + + -instrument-more + Allow choice from more versions of (even simpler) taint tracking logic. A total + of 8 versions of taint tracking logic will be added per gate, including the 4 + versions from `-create-instrumented-model` and these additional versions: + + y_t = a_t + y_t = b_t + y_t = 1 + y_t = 0 + + Only applicable in combination with `-create-instrumented-model`. + (default: do not add more versions of taint tracking logic. +\end{lstlisting} + \section{greenpak4\_dffinv -- merge greenpak4 inverters and DFF/latches} \label{cmd:greenpak4_dffinv} \begin{lstlisting}[numbers=left,frame=single] @@ -4834,6 +4917,13 @@ This command simulates the circuit using the given top-level module. -fst <filename> write the simulation results to the given FST file + -aiw <filename> + write the simulation results to an AIGER witness file + (requires a *.aim file via -map) + + -x + ignore constant x outputs in simulation file. + -clock <portname> name of top-level clock input @@ -4867,6 +4957,9 @@ This command simulates the circuit using the given top-level module. -r read simulation results file (file formats supported: FST) + -map <filename> + read file with port and latch symbols, needed for AIGER witness input + -scope scope of simulation top model @@ -7551,9 +7644,11 @@ Like -sv, but define FORMAL instead of SYNTHESIS. Load the specified VHDL files into Verific. - verific {-f|-F} <command-file> + verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal] <command-file> Load and execute the specified command file. +Override verilog parsing mode can be set. +The macros YOSYS, SYNTHESIS/FORMAL, and VERIFIC are defined implicitly. Command file parser supports following commands: +define - defines macro diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 3b8114fa9..d15ae9b57 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -65,6 +65,15 @@ static double stringToTime(std::string str) return value * pow(10.0, g_units.at(endptr)); } +struct SimWorker; +struct OutputWriter +{ + OutputWriter(SimWorker *w) { worker = w;}; + virtual ~OutputWriter() {}; + virtual void write(std::map<int, bool> &use_signal) = 0; + SimWorker *worker; +}; + struct SimShared { bool debug = false; @@ -77,6 +86,9 @@ struct SimShared double stop_time = -1; SimulationMode sim_mode = SimulationMode::sim; bool cycles_set = false; + std::vector<std::unique_ptr<OutputWriter>> outputfiles; + std::vector<std::pair<int,std::map<int,Const>>> output_data; + bool ignore_x = false; }; void zinit(State &v) @@ -140,8 +152,7 @@ struct SimInstance std::vector<Mem> memories; - dict<Wire*, pair<int, Const>> vcd_database; - dict<Wire*, pair<fstHandle, Const>> fst_database; + dict<Wire*, pair<int, Const>> signal_database; dict<Wire*, fstHandle> fst_handles; SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) : @@ -685,100 +696,53 @@ struct SimInstance it.second->writeback(wbmods); } - void write_vcd_header(std::ofstream &f, int &id) + void register_signals(int &id) { - f << stringf("$scope module %s $end\n", log_id(name())); - for (auto wire : module->wires()) { if (shared->hide_internal && wire->name[0] == '$') continue; - f << stringf("$var wire %d n%d %s%s $end\n", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); - vcd_database[wire] = make_pair(id++, Const()); + signal_database[wire] = make_pair(id, Const()); + id++; } for (auto child : children) - child.second->write_vcd_header(f, id); - - f << stringf("$upscope $end\n"); + child.second->register_signals(id); } - void write_vcd_step(std::ofstream &f) + void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int)> register_signal) { - for (auto &it : vcd_database) - { - Wire *wire = it.first; - Const value = get_state(wire); - int id = it.second.first; - - if (it.second.second == value) - continue; + enter_scope(name()); - it.second.second = value; - - f << "b"; - for (int i = GetSize(value)-1; i >= 0; i--) { - switch (value[i]) { - case State::S0: f << "0"; break; - case State::S1: f << "1"; break; - case State::Sx: f << "x"; break; - default: f << "z"; - } - } - - f << stringf(" n%d\n", id); - } - - for (auto child : children) - child.second->write_vcd_step(f); - } - - void write_fst_header(struct fstContext *f) - { - fstWriterSetScope(f, FST_ST_VCD_MODULE, stringf("%s",log_id(name())).c_str(), nullptr); - for (auto wire : module->wires()) + for (auto signal : signal_database) { - if (shared->hide_internal && wire->name[0] == '$') - continue; - - fstHandle id = fstWriterCreateVar(f, FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire), - stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0); - fst_database[wire] = make_pair(id, Const()); + register_signal(signal.first, signal.second.first); } for (auto child : children) - child.second->write_fst_header(f); + child.second->write_output_header(enter_scope, exit_scope, register_signal); - fstWriterSetUpscope(f); + exit_scope(); } - void write_fst_step(struct fstContext *f) + void register_output_step_values(std::map<int,Const> *data) { - for (auto &it : fst_database) + for (auto &it : signal_database) { Wire *wire = it.first; Const value = get_state(wire); - fstHandle id = it.second.first; + int id = it.second.first; if (it.second.second == value) continue; it.second.second = value; - std::stringstream ss; - for (int i = GetSize(value)-1; i >= 0; i--) { - switch (value[i]) { - case State::S0: ss << "0"; break; - case State::S1: ss << "1"; break; - case State::Sx: ss << "x"; break; - default: ss << "z"; - } - } - fstWriterEmitValueChange(f, id, ss.str().c_str()); + data->emplace(id, value); } for (auto child : children) - child.second->write_fst_step(f); + child.second->register_output_step_values(data); } void setInitState() @@ -801,6 +765,19 @@ struct SimInstance child.second->setInitState(); } + void setState(dict<int, std::pair<SigBit,bool>> bits, std::string values) + { + for(auto bit : bits) { + if (bit.first >= GetSize(values)) + log_error("Too few input data bits in file.\n"); + switch(values.at(bit.first)) { + case '0': set_state(bit.second.first, bit.second.second ? State::S1 : State::S0); break; + case '1': set_state(bit.second.first, bit.second.second ? State::S0 : State::S1); break; + default: set_state(bit.second.first, State::Sx); break; + } + } + } + bool checkSignals() { bool retVal = false; @@ -844,84 +821,49 @@ struct SimInstance struct SimWorker : SimShared { SimInstance *top = nullptr; - std::ofstream vcdfile; - struct fstContext *fstfile = nullptr; pool<IdString> clock, clockn, reset, resetn; std::string timescale; std::string sim_filename; + std::string map_filename; std::string scope; ~SimWorker() { + outputfiles.clear(); delete top; } - void write_vcd_header() + void register_signals() { - vcdfile << stringf("$version %s $end\n", yosys_version_str); - - std::time_t t = std::time(nullptr); - char mbstr[255]; - if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) { - vcdfile << stringf("$date ") << mbstr << stringf(" $end\n"); - } - - if (!timescale.empty()) - vcdfile << stringf("$timescale %s $end\n", timescale.c_str()); - int id = 1; - top->write_vcd_header(vcdfile, id); - - vcdfile << stringf("$enddefinitions $end\n"); - } - - void write_vcd_step(int t) - { - vcdfile << stringf("#%d\n", t); - top->write_vcd_step(vcdfile); - } - - void write_fst_header() - { - std::time_t t = std::time(nullptr); - fstWriterSetDate(fstfile, asctime(std::localtime(&t))); - fstWriterSetVersion(fstfile, yosys_version_str); - if (!timescale.empty()) - fstWriterSetTimescaleFromString(fstfile, timescale.c_str()); - - fstWriterSetPackType(fstfile, FST_WR_PT_FASTLZ); - fstWriterSetRepackOnClose(fstfile, 1); - - top->write_fst_header(fstfile); - } - - void write_fst_step(int t) - { - fstWriterEmitTimeChange(fstfile, t); - - top->write_fst_step(fstfile); + top->register_signals(id); } - void write_output_header() + void register_output_step(int t) { - if (vcdfile.is_open()) - write_vcd_header(); - if (fstfile) - write_fst_header(); + std::map<int,Const> data; + top->register_output_step_values(&data); + output_data.emplace_back(t, data); } - void write_output_step(int t) + void write_output_files() { - if (vcdfile.is_open()) - write_vcd_step(t); - if (fstfile) - write_fst_step(t); - } - - void write_output_end() - { - if (fstfile) - fstWriterClose(fstfile); + std::map<int, bool> use_signal; + bool first = ignore_x; + for(auto& d : output_data) + { + if (first) { + for (auto &data : d.second) + use_signal[data.first] = !data.second.is_fully_undef(); + first = false; + } else { + for (auto &data : d.second) + use_signal[data.first] = true; + } + if (!ignore_x) break; + } + for(auto& writer : outputfiles) + writer->write(use_signal); } void update() @@ -963,6 +905,7 @@ struct SimWorker : SimShared { log_assert(top == nullptr); top = new SimInstance(this, scope, topmod); + register_signals(); if (debug) log("\n===== 0 =====\n"); @@ -977,8 +920,7 @@ struct SimWorker : SimShared update(); - write_output_header(); - write_output_step(0); + register_output_step(0); for (int cycle = 0; cycle < numcycles; cycle++) { @@ -990,7 +932,7 @@ struct SimWorker : SimShared set_inports(clockn, State::S1); update(); - write_output_step(10*cycle + 5); + register_output_step(10*cycle + 5); if (debug) log("\n===== %d =====\n", 10*cycle + 10); @@ -1006,12 +948,12 @@ struct SimWorker : SimShared } update(); - write_output_step(10*cycle + 10); + register_output_step(10*cycle + 10); } - write_output_step(10*numcycles + 2); + register_output_step(10*numcycles + 2); - write_output_end(); + write_output_files(); if (writeback) { pool<Module*> wbmods; @@ -1028,6 +970,7 @@ struct SimWorker : SimShared log_error("Scope must be defined for co-simulation.\n"); top = new SimInstance(this, scope, topmod); + register_signals(); std::vector<fstHandle> fst_clock; @@ -1111,18 +1054,19 @@ struct SimWorker : SimShared try { fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) { log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString()); + bool did_something = false; for(auto &item : inputs) { std::string v = fst->valueOf(item.second); - top->set_state(item.first, Const::from_string(v)); + did_something |= top->set_state(item.first, Const::from_string(v)); } if (initial) { top->setInitState(); - write_output_header(); initial = false; } - update(); - write_output_step(5*cycle); + if (did_something) + update(); + register_output_step(time); bool status = top->checkSignals(); if (status) @@ -1138,16 +1082,320 @@ struct SimWorker : SimShared } catch(fst_end_of_data_exception) { // end of data detected } - write_output_step(5*(cycle-1)+2); - write_output_end(); + + write_output_files(); if (writeback) { pool<Module*> wbmods; top->writeback(wbmods); } + delete fst; + } + + void run_cosim_witness(Module *topmod) + { + log_assert(top == nullptr); + std::ifstream mf(map_filename); + std::string type, symbol; + int variable, index; + dict<int, std::pair<SigBit,bool>> inputs, inits, latches; + while (mf >> type >> variable >> index >> symbol) { + RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); + Wire *w = topmod->wire(escaped_s); + if (!w) + log_error("Wire %s not present in module %s\n",log_signal(w),log_id(topmod)); + if (index < w->start_offset || index > w->start_offset + w->width) + log_error("Index %d for wire %s is out of range\n", index, log_signal(w)); + if (type == "input") { + inputs[variable] = {SigBit(w,index), false}; + } else if (type == "init") { + inits[variable] = {SigBit(w,index), false}; + } else if (type == "latch") { + latches[variable] = {SigBit(w,index), false}; + } else if (type == "invlatch") { + latches[variable] = {SigBit(w,index), true}; + } + } + + std::ifstream f; + f.open(sim_filename.c_str()); + if (f.fail() || GetSize(sim_filename) == 0) + log_error("Can not open file `%s`\n", sim_filename.c_str()); + + int state = 0; + std::string status; + int cycle = 0; + top = new SimInstance(this, scope, topmod); + register_signals(); + + while (!f.eof()) + { + std::string line; + std::getline(f, line); + if (line.size()==0 || line[0]=='#') continue; + if (line[0]=='.') break; + if (state==0 && line.size()!=1) { + // old format detected, latch data + state = 2; + } + if (state==1 && line[0]!='b' && line[0]!='c') { + // was old format but with 1 bit latch + top->setState(latches, status); + state = 3; + } + + switch(state) + { + case 0: + status = line; + state = 1; + break; + case 1: + state = 2; + break; + case 2: + top->setState(latches, line); + state = 3; + break; + default: + log("Simulating cycle %d.\n", cycle); + top->setState(inputs, line); + if (cycle) { + set_inports(clock, State::S1); + set_inports(clockn, State::S0); + } else { + top->setState(inits, line); + set_inports(clock, State::S0); + set_inports(clockn, State::S1); + } + update(); + register_output_step(10*cycle); + if (cycle) { + set_inports(clock, State::S0); + set_inports(clockn, State::S1); + update(); + register_output_step(10*cycle + 5); + } + cycle++; + break; + } + } + register_output_step(10*cycle); + write_output_files(); } }; +struct VCDWriter : public OutputWriter +{ + VCDWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) { + vcdfile.open(filename.c_str()); + } + + void write(std::map<int, bool> &use_signal) override + { + if (!vcdfile.is_open()) return; + vcdfile << stringf("$version %s $end\n", yosys_version_str); + + std::time_t t = std::time(nullptr); + char mbstr[255]; + if (std::strftime(mbstr, sizeof(mbstr), "%c", std::localtime(&t))) { + vcdfile << stringf("$date ") << mbstr << stringf(" $end\n"); + } + + if (!worker->timescale.empty()) + vcdfile << stringf("$timescale %s $end\n", worker->timescale.c_str()); + + 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](Wire *wire, int id) { if (use_signal.at(id)) vcdfile << stringf("$var wire %d n%d %s%s $end\n", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); } + ); + + vcdfile << stringf("$enddefinitions $end\n"); + + for(auto& d : worker->output_data) + { + vcdfile << stringf("#%d\n", d.first); + for (auto &data : d.second) + { + if (!use_signal.at(data.first)) continue; + Const value = data.second; + vcdfile << "b"; + for (int i = GetSize(value)-1; i >= 0; i--) { + switch (value[i]) { + case State::S0: vcdfile << "0"; break; + case State::S1: vcdfile << "1"; break; + case State::Sx: vcdfile << "x"; break; + default: vcdfile << "z"; + } + } + vcdfile << stringf(" n%d\n", data.first); + } + } + } + + std::ofstream vcdfile; +}; + +struct FSTWriter : public OutputWriter +{ + FSTWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) { + fstfile = (struct fstContext *)fstWriterCreate(filename.c_str(),1); + } + + virtual ~FSTWriter() + { + fstWriterClose(fstfile); + } + + void write(std::map<int, bool> &use_signal) override + { + if (!fstfile) return; + std::time_t t = std::time(nullptr); + fstWriterSetDate(fstfile, asctime(std::localtime(&t))); + fstWriterSetVersion(fstfile, yosys_version_str); + if (!worker->timescale.empty()) + fstWriterSetTimescaleFromString(fstfile, worker->timescale.c_str()); + + fstWriterSetPackType(fstfile, FST_WR_PT_FASTLZ); + fstWriterSetRepackOnClose(fstfile, 1); + + 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](Wire *wire, int id) { + if (!use_signal.at(id)) return; + fstHandle fst_id = fstWriterCreateVar(fstfile, FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire), + stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0); + + mapping.emplace(id, fst_id); + } + ); + + for(auto& d : worker->output_data) + { + fstWriterEmitTimeChange(fstfile, d.first); + for (auto &data : d.second) + { + if (!use_signal.at(data.first)) continue; + Const value = data.second; + std::stringstream ss; + for (int i = GetSize(value)-1; i >= 0; i--) { + switch (value[i]) { + case State::S0: ss << "0"; break; + case State::S1: ss << "1"; break; + case State::Sx: ss << "x"; break; + default: ss << "z"; + } + } + fstWriterEmitValueChange(fstfile, mapping[data.first], ss.str().c_str()); + } + } + } + + struct fstContext *fstfile = nullptr; + std::map<int,fstHandle> mapping; +}; + +struct AIWWriter : public OutputWriter +{ + AIWWriter(SimWorker *worker, std::string filename) : OutputWriter(worker) { + aiwfile.open(filename.c_str()); + } + + virtual ~AIWWriter() + { + aiwfile << '.' << '\n'; + } + + void write(std::map<int, bool> &) override + { + if (!aiwfile.is_open()) return; + std::ifstream mf(worker->map_filename); + std::string type, symbol; + int variable, index; + while (mf >> type >> variable >> index >> symbol) { + RTLIL::IdString escaped_s = RTLIL::escape_id(symbol); + Wire *w = worker->top->module->wire(escaped_s); + if (!w) + log_error("Wire %s not present in module %s\n",log_signal(w),log_id(worker->top->module)); + if (index < w->start_offset || index > w->start_offset + w->width) + log_error("Index %d for wire %s is out of range\n", index, log_signal(w)); + if (type == "input") { + aiw_inputs[variable] = SigBit(w,index); + } else if (type == "init") { + aiw_inits[variable] = SigBit(w,index); + } else if (type == "latch") { + aiw_latches[variable] = {SigBit(w,index), false}; + } else if (type == "invlatch") { + aiw_latches[variable] = {SigBit(w,index), true}; + } + } + + worker->top->write_output_header( + [](IdString) {}, + []() {}, + [this](Wire *wire, int id) { mapping[wire] = id; } + ); + + std::map<int, Yosys::RTLIL::Const> current; + bool first = true; + for(auto& d : worker->output_data) + { + for (auto &data : d.second) + { + current[data.first] = data.second; + } + if (first) { + for (int i = 0;; i++) + { + if (aiw_latches.count(i)) { + SigBit bit = aiw_latches.at(i).first; + auto v = current[mapping[bit.wire]].bits.at(bit.offset); + if (v == State::S1) + aiwfile << (aiw_latches.at(i).second ? '0' : '1'); + else + aiwfile << (aiw_latches.at(i).second ? '1' : '0'); + continue; + } + aiwfile << '\n'; + break; + } + first = false; + } + + for (int i = 0;; i++) + { + if (aiw_inputs.count(i)) { + SigBit bit = aiw_inputs.at(i); + auto v = current[mapping[bit.wire]].bits.at(bit.offset); + if (v == State::S1) + aiwfile << '1'; + else + aiwfile << '0'; + continue; + } + if (aiw_inits.count(i)) { + SigBit bit = aiw_inits.at(i); + auto v = current[mapping[bit.wire]].bits.at(bit.offset); + if (v == State::S1) + aiwfile << '1'; + else + aiwfile << '0'; + continue; + } + aiwfile << '\n'; + break; + } + } + } + + std::ofstream aiwfile; + dict<int, std::pair<SigBit, bool>> aiw_latches; + dict<int, SigBit> aiw_inputs, aiw_inits; + std::map<Wire*,int> mapping; +}; + struct SimPass : public Pass { SimPass() : Pass("sim", "simulate the circuit") { } void help() override @@ -1164,6 +1412,13 @@ struct SimPass : public Pass { log(" -fst <filename>\n"); log(" write the simulation results to the given FST file\n"); log("\n"); + log(" -aiw <filename>\n"); + log(" write the simulation results to an AIGER witness file\n"); + log(" (requires a *.aim file via -map)\n"); + log("\n"); + log(" -x\n"); + log(" ignore constant x outputs in simulation file.\n"); + log("\n"); log(" -clock <portname>\n"); log(" name of top-level clock input\n"); log("\n"); @@ -1197,6 +1452,9 @@ struct SimPass : public Pass { log(" -r\n"); log(" read simulation results file (file formats supported: FST)\n"); log("\n"); + log(" -map <filename>\n"); + log(" read file with port and latch symbols, needed for AIGER witness input\n"); + log("\n"); log(" -scope\n"); log(" scope of simulation top model\n"); log("\n"); @@ -1238,13 +1496,19 @@ struct SimPass : public Pass { if (args[argidx] == "-vcd" && argidx+1 < args.size()) { std::string vcd_filename = args[++argidx]; rewrite_filename(vcd_filename); - worker.vcdfile.open(vcd_filename.c_str()); + worker.outputfiles.emplace_back(std::unique_ptr<VCDWriter>(new VCDWriter(&worker, vcd_filename.c_str()))); continue; } if (args[argidx] == "-fst" && argidx+1 < args.size()) { std::string fst_filename = args[++argidx]; rewrite_filename(fst_filename); - worker.fstfile = (struct fstContext *)fstWriterCreate(fst_filename.c_str(),1); + worker.outputfiles.emplace_back(std::unique_ptr<FSTWriter>(new FSTWriter(&worker, fst_filename.c_str()))); + continue; + } + if (args[argidx] == "-aiw" && argidx+1 < args.size()) { + std::string aiw_filename = args[++argidx]; + rewrite_filename(aiw_filename); + worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(new AIWWriter(&worker, aiw_filename.c_str()))); continue; } if (args[argidx] == "-n" && argidx+1 < args.size()) { @@ -1298,6 +1562,12 @@ struct SimPass : public Pass { worker.sim_filename = sim_filename; 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] == "-scope" && argidx+1 < args.size()) { worker.scope = args[++argidx]; continue; @@ -1334,6 +1604,10 @@ struct SimPass : public Pass { worker.sim_mode = SimulationMode::gate; continue; } + if (args[argidx] == "-x") { + worker.ignore_x = true; + continue; + } break; } extra_args(args, argidx, design); @@ -1359,7 +1633,10 @@ struct SimPass : public Pass { if (worker.sim_filename.empty()) worker.run(top_mod, numcycles); else - worker.run_cosim(top_mod, numcycles); + if (worker.map_filename.empty()) + worker.run_cosim(top_mod, numcycles); + else + worker.run_cosim_witness(top_mod); } } SimPass; diff --git a/techlibs/gowin/cells_sim.v b/techlibs/gowin/cells_sim.v index cc2ad3df5..b07ee6924 100644 --- a/techlibs/gowin/cells_sim.v +++ b/techlibs/gowin/cells_sim.v @@ -550,7 +550,6 @@ module GND(output G); assign G = 0; endmodule -(* abc9_box *) module IBUF(output O, input I); specify @@ -560,7 +559,6 @@ module IBUF(output O, input I); assign O = I; endmodule -(* abc9_box *) module OBUF(output O, input I); specify @@ -584,6 +582,14 @@ module IOBUF (O, IO, I, OEN); assign I = IO; endmodule +module TLVDS_OBUF (I, O, OB); + input I; + output O; + output OB; + assign O = I; + assign OB = ~I; +endmodule + module GSR (input GSRI); wire GSRO = GSRI; endmodule diff --git a/tests/various/.gitignore b/tests/various/.gitignore index 2bb6c7179..c6373468a 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -5,3 +5,4 @@ /run-test.mk /plugin.so /plugin.so.dSYM +/temp diff --git a/tests/various/json_escape_chars.ys b/tests/various/json_escape_chars.ys new file mode 100644 index 000000000..f118357c0 --- /dev/null +++ b/tests/various/json_escape_chars.ys @@ -0,0 +1,14 @@ +! mkdir -p temp +read_verilog <<EOT +(* src = "\042 \057 \134 \010 \014 \012 \015 \011 \025 \033" *) +module foo; +endmodule +EOT +write_json temp/test_escapes.json +design -reset +read_json temp/test_escapes.json +write_json temp/test_escapes.json +design -reset +read_json temp/test_escapes.json +write_rtlil temp/test_escapes.json.il +! grep -F 'attribute \src "\" / \\ \010 \014 \n \015 \t \025 \033"' temp/test_escapes.json.il |