riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

satgen import sigbit api

This commit is contained in:
Clifford Wolf 2014-10-03 18:51:50 +02:00
parent 3e4b0cac8d
commit 56c1d43408
1 changed files with 17 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
kernel/satgen.h
View File

@ -38,6 +38,7 @@ struct SatGen
std::string prefix; std::string prefix;
SigPool initial_state; SigPool initial_state;
std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en; std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en;
std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
bool ignore_div_by_zero; bool ignore_div_by_zero;
bool model_undef; bool model_undef;
@ -52,7 +53,7 @@ struct SatGen
this->prefix = prefix; this->prefix = prefix;
} }
std::vector<int> importSigSpecWorker(RTLIL::SigSpec &sig, std::string &pf, bool undef_mode, bool dup_undef) std::vector<int> importSigSpecWorker(RTLIL::SigSpec sig, std::string &pf, bool undef_mode, bool dup_undef)
{ {
log_assert(!undef_mode || model_undef); log_assert(!undef_mode || model_undef);
sigmap->apply(sig); sigmap->apply(sig);
@ -69,6 +70,7 @@ struct SatGen
} else { } else {
std::string name = pf + stringf(bit.wire->width == 1 ? "%s" : "%s [%d]", RTLIL::id2cstr(bit.wire->name), bit.offset); std::string name = pf + stringf(bit.wire->width == 1 ? "%s" : "%s [%d]", RTLIL::id2cstr(bit.wire->name), bit.offset);
vec.push_back(ez->frozen_literal(name)); vec.push_back(ez->frozen_literal(name));
imported_signals[pf][bit] = vec.back();
} }
return vec; return vec;
} }
@ -94,6 +96,20 @@ struct SatGen
return importSigSpecWorker(sig, pf, true, false); return importSigSpecWorker(sig, pf, true, false);
} }
int importSigBit(RTLIL::SigBit bit, int timestep = -1)
{
log_assert(timestep != 0);
std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
return importSigSpecWorker(bit, pf, false, false).front();
}
bool importedSigBit(RTLIL::SigBit bit, int timestep = -1)
{
log_assert(timestep != 0);
std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
return imported_signals[pf].count(bit);
}
void getAsserts(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1) void getAsserts(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1)
{ {
std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));