mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-05-05 06:45:46 +00:00
Code Activity

Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor

Browse source
This commit is contained in:
Ahmed Irfan 2014-01-20 09:58:04 +01:00
commit b7adf4c7a0
16 changed files with 349 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

1
kernel/celltypes.h
View file

@ -96,6 +96,7 @@ struct CellTypes
cell_types.insert("$pmux");
cell_types.insert("$safe_pmux");
cell_types.insert("$lut");
cell_types.insert("$assert");
}
void setup_internals_mem()

7
kernel/rtlil.cc
View file

@ -595,6 +595,13 @@ namespace {
return;
}
if (cell->type == "$assert") {
port("\\A", 1);
port("\\EN", 1);
check_expected();
return;
}
if (cell->type == "$_INV_") { check_gate("AY"); return; }
if (cell->type == "$_AND_") { check_gate("ABY"); return; }
if (cell->type == "$_OR_") { check_gate("ABY"); return; }

21
kernel/satgen.h
View file

@ -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;