diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 5cfdff3fb..4ef28be9f 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -20,6 +20,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" #include "kernel/json.h" +#include "kernel/yw.h" #include "libs/json11/json11.hpp" USING_YOSYS_NAMESPACE @@ -710,18 +711,6 @@ struct AigerWriter f << it.second; } - template static std::vector witness_path(T *obj) { - std::vector 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(PrettyJson &json) { json.begin_object(); diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4315f6f67..4eb675c3c 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -29,6 +29,7 @@ #include "kernel/log.h" #include "kernel/mem.h" #include "kernel/json.h" +#include "kernel/yw.h" #include USING_YOSYS_NAMESPACE @@ -141,18 +142,6 @@ struct BtorWorker return " " + infostr; } - template static std::vector witness_path(T *obj) { - std::vector 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 ywmap_state(const SigSpec &sig) { if (ywmap_json.active()) ywmap_states.emplace_back(sig); diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index 14cf61fd7..8d0cc8112 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -316,6 +316,7 @@ def wit2yw(input, mapfile, output): if current_t > t: t = current_t values = WitnessValues() + array_inits = set() frames.append(values) line = next(input, None) @@ -327,39 +328,63 @@ def wit2yw(input, mapfile, output): 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('[') or not addr.endswith(']'): + 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") - addr = int(addr[1:-1], 2) + 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 >= btor_sig["size"]: - raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file") + if addr < 0 or addr >= size: + raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file") - btor_sig = [{ - "path": (*btor_sig["path"], f"\\[{addr}]"), - "width": btor_sig["width"], - "offset": 0, - }] - - signal_value = iter(reversed(tokens[2])) + array_inits.add((path, addr)) + btor_sig = [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + btor_sigs = [btor_sig] else: - signal_value = iter(reversed(tokens[1])) + value = tokens[1] - 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(signal_value) + for btor_sig in btor_sigs: + value_bits = iter(reversed(value)) - if next(signal_value, None) is not None: - raise click.ClickException(f"{input_name}: excess bits in BTOR witness file") + 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: diff --git a/kernel/yw.cc b/kernel/yw.cc index 4a6e37a13..73e7710db 100644 --- a/kernel/yw.cc +++ b/kernel/yw.cc @@ -161,7 +161,7 @@ ReadWitness::ReadWitness(const std::string &filename) : 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 = json["init_only"].bool_value(); + signal.init_only = signal_json["init_only"].bool_value(); signals.push_back(signal); } diff --git a/kernel/yw.h b/kernel/yw.h index 8b651fd83..503319b1d 100644 --- a/kernel/yw.h +++ b/kernel/yw.h @@ -52,6 +52,18 @@ struct WitnessHierarchyItem { template void witness_hierarchy(RTLIL::Module *module, D data, T callback); +template static std::vector witness_path(T *obj) { + std::vector 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 { diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index af3a38be8..1dd406f22 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -24,6 +24,7 @@ #include "kernel/fstdata.h" #include "kernel/ff.h" #include "kernel/yw.h" +#include "kernel/json.h" #include @@ -75,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; @@ -95,6 +107,8 @@ struct SimShared bool date = false; bool multiclock = false; int next_output_id = 0; + int step = 0; + std::vector triggered_assertions; }; void zinit(State &v) @@ -161,6 +175,7 @@ struct SimInstance dict> signal_database; dict>> trace_mem_database; + dict, Const> trace_mem_init_database; dict fst_handles; dict fst_inputs; dict> fst_memories; @@ -306,6 +321,21 @@ struct SimInstance return log_id(module->name); } + vector witness_full_path() const + { + if (instance != nullptr) + return parent->witness_full_path(instance); + return vector(); + } + + vector 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; @@ -700,7 +730,11 @@ struct SimInstance State a = get_state(cell->getPort(ID::A))[0]; State en = get_state(cell->getPort(ID::EN))[0]; - if (cell->type == ID($cover) && en == State::S1 && a != State::S1) + 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($assume) && en == State::S1 && a != State::S1) @@ -875,7 +909,11 @@ struct SimInstance int output_id = shared->next_output_id++; Const data; if (!shared->output_data.empty()) { - data = mem.get_init_data().extract(index * mem.width, mem.width); + 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)); @@ -1060,6 +1098,7 @@ struct SimWorker : SimShared std::string timescale; std::string sim_filename; std::string map_filename; + std::string summary_filename; std::string scope; ~SimWorker() @@ -1103,6 +1142,9 @@ struct SimWorker : SimShared void update(bool gclk) { + if (gclk) + step += 1; + while (1) { if (debug) @@ -1130,7 +1172,7 @@ struct SimWorker : SimShared top->update_ph1(); if (debug) log("\n-- ph3 (initialize) --\n"); - top->update_ph3(false); + top->update_ph3(true); } void set_inports(pool ports, State value) @@ -1709,7 +1751,10 @@ struct SimWorker : SimShared SigChunk(found_path.wire, signal.offset, signal.width), value); } else if (!found_path.memid.empty()) { - found_path.instance->register_memory_addr(found_path.memid, found_path.addr); + 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); @@ -1793,6 +1838,37 @@ struct SimWorker : SimShared 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; @@ -2330,6 +2406,9 @@ struct SimPass : public Pass { log(" -append \n"); log(" number of extra clock cycles to simulate for a Yosys witness input\n"); log("\n"); + log(" -summary \n"); + log(" write a JSON summary to the given file\n"); + log("\n"); log(" -map \n"); log(" read file with port and latch symbols, needed for AIGER witness input\n"); log("\n"); @@ -2469,6 +2548,12 @@ struct SimPass : public Pass { 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; @@ -2558,6 +2643,8 @@ struct SimPass : public Pass { log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); } } + + worker.write_summary(); } } SimPass;