diff options
author | Clifford Wolf <clifford@clifford.at> | 2016-07-13 16:56:17 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2016-07-13 16:56:17 +0200 |
commit | 721f1f5ecfb6334904f6058d6d376d21b5efc438 (patch) | |
tree | 3573f744b6d7c33f55dd06a152d4ff199cf30b22 /kernel | |
parent | b3155af5f65333d272da339222e1e1962fb088b7 (diff) | |
download | yosys-721f1f5ecfb6334904f6058d6d376d21b5efc438.tar.gz yosys-721f1f5ecfb6334904f6058d6d376d21b5efc438.tar.bz2 yosys-721f1f5ecfb6334904f6058d6d376d21b5efc438.zip |
Added basic support for $expect cells
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/celltypes.h | 1 | ||||
-rw-r--r-- | kernel/rtlil.cc | 25 | ||||
-rw-r--r-- | kernel/rtlil.h | 2 | ||||
-rw-r--r-- | kernel/satgen.h | 9 |
4 files changed, 29 insertions, 8 deletions
diff --git a/kernel/celltypes.h b/kernel/celltypes.h index cf7bc2dcf..78403fcd3 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -116,6 +116,7 @@ struct CellTypes setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true); setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true); + setup_type("$expect", {A, EN}, pool<RTLIL::IdString>(), true); setup_type("$equiv", {A, B}, {Y}, true); } diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 9da6d2816..644a83a76 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1017,14 +1017,7 @@ namespace { return; } - if (cell->type == "$assert") { - port("\\A", 1); - port("\\EN", 1); - check_expected(); - return; - } - - if (cell->type == "$assume") { + if (cell->type.in("$assert", "$assume", "$expect")) { port("\\A", 1); port("\\EN", 1); check_expected(); @@ -1795,6 +1788,22 @@ RTLIL::Cell* RTLIL::Module::addAssert(RTLIL::IdString name, RTLIL::SigSpec sig_a return cell; } +RTLIL::Cell* RTLIL::Module::addAssume(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en) +{ + RTLIL::Cell *cell = addCell(name, "$assume"); + cell->setPort("\\A", sig_a); + cell->setPort("\\EN", sig_en); + return cell; +} + +RTLIL::Cell* RTLIL::Module::addExpect(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en) +{ + RTLIL::Cell *cell = addCell(name, "$expect"); + cell->setPort("\\A", sig_a); + cell->setPort("\\EN", sig_en); + return cell; +} + RTLIL::Cell* RTLIL::Module::addEquiv(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y) { RTLIL::Cell *cell = addCell(name, "$equiv"); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 274f97023..627835a9c 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1004,6 +1004,8 @@ public: RTLIL::Cell* addLut (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_y, RTLIL::Const lut); RTLIL::Cell* addTribuf (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_y); RTLIL::Cell* addAssert (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); + RTLIL::Cell* addAssume (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); + RTLIL::Cell* addExpect (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); RTLIL::Cell* addEquiv (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y); RTLIL::Cell* addSr (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true); diff --git a/kernel/satgen.h b/kernel/satgen.h index e118c1569..da892c710 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -69,6 +69,7 @@ struct SatGen SigPool initial_state; std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en; std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en; + std::map<std::string, RTLIL::SigSpec> expects_a, expects_en; std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals; bool ignore_div_by_zero; bool model_undef; @@ -1346,6 +1347,14 @@ struct SatGen return true; } + if (cell->type == "$expect") + { + std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); + expects_a[pf].append((*sigmap)(cell->getPort("\\A"))); + expects_en[pf].append((*sigmap)(cell->getPort("\\EN"))); + return true; + } + // Unsupported internal cell types: $pow $lut // .. and all sequential cells except $dff and $_DFF_[NP]_ return false; |