mirror of https://github.com/YosysHQ/yosys.git
Added $assert support to satgen
This commit is contained in:
parent
1e67099b77
commit
c36bac0e10
|
@ -38,6 +38,7 @@ struct SatGen
|
|||
SigMap *sigmap;
|
||||
std::string prefix;
|
||||
SigPool initial_state;
|
||||
RTLIL::SigSpec asserts_a, asserts_en;
|
||||
bool ignore_div_by_zero;
|
||||
bool model_undef;
|
||||
|
||||
|
@ -96,6 +97,19 @@ struct SatGen
|
|||
return importSigSpecWorker(sig, pf, true, false);
|
||||
}
|
||||
|
||||
int importAsserts(int timestep = -1)
|
||||
{
|
||||
std::vector<int> check_bits, enable_bits;
|
||||
if (model_undef) {
|
||||
check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a, timestep)), importDefSigSpec(asserts_a, timestep));
|
||||
enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en, timestep)), importDefSigSpec(asserts_en, timestep));
|
||||
} else {
|
||||
check_bits = importDefSigSpec(asserts_a, timestep);
|
||||
enable_bits = importDefSigSpec(asserts_en, timestep);
|
||||
}
|
||||
return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
|
||||
}
|
||||
|
||||
int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
|
||||
{
|
||||
if (timestep_rhs < 0)
|
||||
|
@ -765,6 +779,13 @@ struct SatGen
|
|||
return true;
|
||||
}
|
||||
|
||||
if (cell->type == "$assert")
|
||||
{
|
||||
asserts_a.append((*sigmap)(cell->connections.at("\\A")));
|
||||
asserts_en.append((*sigmap)(cell->connections.at("\\EN")));
|
||||
return true;
|
||||
}
|
||||
|
||||
// Unsupported internal cell types: $pow $lut
|
||||
// .. and all sequential cells except $dff and $_DFF_[NP]_
|
||||
return false;
|
||||
|
|
Loading…
Reference in New Issue