mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Added satgen initstate support

Browse source
This commit is contained in:
Clifford Wolf 2016-07-22 10:28:45 +02:00
parent 7fef5ff104
commit 89deb412c6
1 changed files with 27 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
kernel/satgen.h
View file

@ -71,6 +71,7 @@ struct SatGen
std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en; std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en;
std::map<std::string, RTLIL::SigSpec> predict_a, predict_en; std::map<std::string, RTLIL::SigSpec> predict_a, predict_en;
std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals; std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
std::map<std::pair<std::string, int>, bool> initstates;
bool ignore_div_by_zero; bool ignore_div_by_zero;
bool model_undef; bool model_undef;
@ -267,6 +268,13 @@ struct SatGen
ez->assume(ez->OR(undef, ez->IFF(y, yy))); ez->assume(ez->OR(undef, ez->IFF(y, yy)));
} }
void setInitState(int timestep)
{
auto key = make_pair(prefix, timestep);
log_assert(initstates.count(key) == 0 || initstates.at(key) == true);
initstates[key] = true;
}
bool importCell(RTLIL::Cell *cell, int timestep = -1) bool importCell(RTLIL::Cell *cell, int timestep = -1)
{ {
bool arith_undef_handled = false; bool arith_undef_handled = false;
@ -1331,6 +1339,25 @@ struct SatGen
return true; return true;
} }
if (cell->type == "$initstate")
{
auto key = make_pair(prefix, timestep);
if (initstates.count(key) == 0)
initstates[key] = false;
std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
log_assert(GetSize(y) == 1);
ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
if (model_undef) {
std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
log_assert(GetSize(undef_y) == 1);
ez->SET(undef_y[0], ez->CONST_FALSE);
}
return true;
}
if (cell->type == "$assert") if (cell->type == "$assert")
{ {
std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));