From 50d117956c7913d2bb661a948f0a1bff6bd0f3f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 4 Sep 2023 14:49:19 +0200 Subject: [PATCH] sim: Add print support --- passes/sat/sim.cc | 92 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 90 insertions(+), 2 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 325e123201c..7b2236ad6fa 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -25,6 +25,7 @@ #include "kernel/ff.h" #include "kernel/yw.h" #include "kernel/json.h" +#include "kernel/fmt.h" #include @@ -168,11 +169,38 @@ struct SimInstance Const data; }; + struct print_state_t + { + Const past_trg; + Const past_en; + Const past_args; + + Cell *cell; + Fmt fmt; + + std::tuple _sort_label() const + { + return std::make_tuple( + cell->getParam(ID::TRG_ENABLE).as_bool(), // Group by trigger + cell->getPort(ID::TRG), + cell->getParam(ID::TRG_POLARITY), + -cell->getParam(ID::PRIORITY).as_int(), // Then sort by descending PRIORITY + cell + ); + } + + bool operator<(const print_state_t &other) const + { + return _sort_label() < other._sort_label(); + } + }; + dict ff_database; dict mem_database; pool formal_database; pool initstate_database; dict mem_cells; + std::vector print_database; std::vector memories; @@ -289,13 +317,26 @@ struct SimInstance if (shared->fst) fst_memories[name] = shared->fst->getMemoryHandles(scope + "." + RTLIL::unescape_id(name)); } - if (cell->type.in(ID($assert), ID($cover), ID($assume))) { + + if (cell->type.in(ID($assert), ID($cover), ID($assume))) formal_database.insert(cell); - } + if (cell->type == ID($initstate)) initstate_database.insert(cell); + + if (cell->type == ID($print)) { + print_database.emplace_back(); + auto &print = print_database.back(); + print.cell = cell; + print.fmt.parse_rtlil(cell); + print.past_trg = Const(State::Sx, cell->getPort(ID::TRG).size()); + print.past_args = Const(State::Sx, cell->getPort(ID::ARGS).size()); + print.past_en = State::Sx; + } } + std::sort(print_database.begin(), print_database.end()); + if (shared->zinit) { for (auto &it : ff_database) @@ -519,6 +560,9 @@ struct SimInstance return; } + if (cell->type == ID($print)) + return; + log_error("Unsupported cell type: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell)); } @@ -760,6 +804,50 @@ struct SimInstance } } + // Do prints *before* assertions + for (auto &print : print_database) { + Cell *cell = print.cell; + bool triggered = false; + + Const trg = get_state(cell->getPort(ID::TRG)); + Const en = get_state(cell->getPort(ID::EN)); + Const args = get_state(cell->getPort(ID::ARGS)); + + if (!en.as_bool()) + goto update_print; + + if (cell->getParam(ID::TRG_ENABLE).as_bool()) { + Const trg_pol = cell->getParam(ID::TRG_POLARITY); + for (int i = 0; i < trg.size(); i++) { + bool pol = trg_pol[i] == State::S1; + State curr = trg[i], past = print.past_trg[i]; + if (pol && curr == State::S1 && past == State::S0) + triggered = true; + if (!pol && curr == State::S0 && past == State::S1) + triggered = true; + } + } else { + if (args != print.past_args || en != print.past_en) + triggered = true; + } + + if (triggered) { + int pos = 0; + for (auto &part : print.fmt.parts) { + part.sig = args.extract(pos, part.sig.size()); + pos += part.sig.size(); + } + + std::string rendered = print.fmt.render(); + log("%s", rendered.c_str()); + } + + update_print: + print.past_trg = trg; + print.past_en = en; + print.past_args = args; + } + if (check_assertions) { for (auto cell : formal_database)