mirror of https://github.com/YosysHQ/yosys.git
Merge pull request #6072 from YosysHQ/nella/dlatchlibmap-cleanup
Update to `dfflibmap` to be able to map LATCHes (clean up of #5976)
This commit is contained in:
nella
GitHub
commit
b8959e70ba
|
|
@ -296,7 +296,10 @@ static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool fla
|
||||||
{
|
{
|
||||||
auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node);
|
auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node);
|
||||||
RTLIL::SigSpec enable_sig, data_sig, clear_sig, preset_sig;
|
RTLIL::SigSpec enable_sig, data_sig, clear_sig, preset_sig;
|
||||||
|
const std::string name = module->name.unescape();
|
||||||
|
|
||||||
|
std::optional<char> clear_preset_var1;
|
||||||
|
std::optional<char> clear_preset_var2;
|
||||||
for (auto child : node->children) {
|
for (auto child : node->children) {
|
||||||
if (child->id == "enable")
|
if (child->id == "enable")
|
||||||
enable_sig = parse_func_expr(module, child->value.c_str());
|
enable_sig = parse_func_expr(module, child->value.c_str());
|
||||||
|
|
@ -306,32 +309,83 @@ static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool fla
|
||||||
clear_sig = parse_func_expr(module, child->value.c_str());
|
clear_sig = parse_func_expr(module, child->value.c_str());
|
||||||
if (child->id == "preset")
|
if (child->id == "preset")
|
||||||
preset_sig = parse_func_expr(module, child->value.c_str());
|
preset_sig = parse_func_expr(module, child->value.c_str());
|
||||||
|
|
||||||
|
for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}}) {
|
||||||
|
if (child->id == id) {
|
||||||
|
if (child->value.size() != 1)
|
||||||
|
log_error("Unexpected length of clear_preset_var* value %s in latch cell %s\n", child->value, name);
|
||||||
|
*var = child->value[0];
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (enable_sig.size() == 0 || data_sig.size() == 0) {
|
if (enable_sig.size() == 0 || data_sig.size() == 0) {
|
||||||
if (!flag_ignore_miss_data_latch)
|
if (!flag_ignore_miss_data_latch)
|
||||||
log_error("Latch cell %s has no data_in and/or enable attribute.\n", module);
|
log_error("Latch cell %s has no data_in and/or enable attribute.\n", name);
|
||||||
else
|
else
|
||||||
log("Ignored latch cell %s with no data_in and/or enable attribute.\n", module);
|
log("Ignored latch cell %s with no data_in and/or enable attribute.\n", name);
|
||||||
|
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
RTLIL::Cell *cell = module->addCell(NEW_ID, ID($_NOT_));
|
for (auto& [out_sig, cp_var, neg] : {tuple{iq_sig, clear_preset_var1, false}, {iqn_sig, clear_preset_var2, true}}) {
|
||||||
cell->setPort(ID::A, iq_sig);
|
SigSpec q_sig = out_sig;
|
||||||
cell->setPort(ID::Y, iqn_sig);
|
if (neg) {
|
||||||
|
q_sig = module->addWire(NEW_ID, out_sig.as_wire());
|
||||||
|
module->addNotGate(NEW_ID, q_sig, out_sig);
|
||||||
|
}
|
||||||
|
|
||||||
if (clear_sig.size() == 1) {
|
RTLIL::Cell* cell = module->addCell(NEW_ID, "");
|
||||||
RTLIL::SigSpec clear_negative = module->NotGate(NEW_ID, clear_sig);
|
cell->setPort(ID::D, data_sig);
|
||||||
data_sig = module->AndGate(NEW_ID, data_sig, clear_negative);
|
cell->setPort(ID::Q, q_sig);
|
||||||
enable_sig = module->OrGate(NEW_ID, enable_sig, clear_sig);
|
cell->setPort(ID::E, enable_sig);
|
||||||
}
|
|
||||||
|
|
||||||
if (preset_sig.size() == 1) {
|
if (clear_sig.size() == 0 && preset_sig.size() == 0) {
|
||||||
data_sig = module->OrGate(NEW_ID, data_sig, preset_sig);
|
cell->type = ID::$_DLATCH_P_;
|
||||||
enable_sig = module->OrGate(NEW_ID, enable_sig, preset_sig);
|
}
|
||||||
|
|
||||||
|
if (clear_sig.size() == 1 && preset_sig.size() == 0) {
|
||||||
|
cell->type = ID::$_DLATCH_PP0_;
|
||||||
|
cell->setPort(ID::R, clear_sig);
|
||||||
|
}
|
||||||
|
|
||||||
|
if (clear_sig.size() == 0 && preset_sig.size() == 1) {
|
||||||
|
cell->type = ID::$_DLATCH_PP1_;
|
||||||
|
cell->setPort(ID::R, preset_sig);
|
||||||
|
}
|
||||||
|
|
||||||
|
if (clear_sig.size() == 1 && preset_sig.size() == 1) {
|
||||||
|
cell->type = ID::$_DLATCHSR_PPP_;
|
||||||
|
|
||||||
|
SigBit s_sig = preset_sig;
|
||||||
|
SigBit r_sig = clear_sig;
|
||||||
|
if (cp_var && *cp_var != 'X') {
|
||||||
|
// Either set or reset dominates
|
||||||
|
bool set_dominates;
|
||||||
|
if (*cp_var == 'L') {
|
||||||
|
set_dominates = neg;
|
||||||
|
} else if (*cp_var == 'H') {
|
||||||
|
set_dominates = !neg;
|
||||||
|
} else {
|
||||||
|
log_error("Latch cell %s has unsupported clear&preset behavior \'%c\'.\n", name, *cp_var);
|
||||||
|
}
|
||||||
|
log_debug("cell %s variable %d cp_var %c set dominates? %d\n", name, (int)neg + 1, *cp_var, set_dominates);
|
||||||
|
// S&R priority is well-defined now
|
||||||
|
if (set_dominates) {
|
||||||
|
r_sig = module->AndnotGate(NEW_ID, r_sig, s_sig);
|
||||||
|
} else {
|
||||||
|
s_sig = module->AndnotGate(NEW_ID, s_sig, r_sig);
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
log_debug("cell %s variable %d undef c&p behavior\n", name, (int)neg + 1);
|
||||||
|
}
|
||||||
|
|
||||||
|
cell->setPort(ID::S, s_sig);
|
||||||
|
cell->setPort(ID::R, r_sig);
|
||||||
|
}
|
||||||
|
|
||||||
|
log_assert(!cell->type.empty());
|
||||||
}
|
}
|
||||||
cell = module->addDlatchGate(NEW_ID, enable_sig, data_sig, iq_sig, true);
|
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -67,7 +67,7 @@ enum FfInit {
|
||||||
};
|
};
|
||||||
|
|
||||||
struct DffLegalizePass : public Pass {
|
struct DffLegalizePass : public Pass {
|
||||||
DffLegalizePass() : Pass("dfflegalize", "convert FFs to types supported by the target") { }
|
DffLegalizePass() : Pass("dfflegalize", "convert FFs and LATCHes to types supported by the target") { }
|
||||||
void help() override
|
void help() override
|
||||||
{
|
{
|
||||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||||
|
|
@ -1071,7 +1071,7 @@ struct DffLegalizePass : public Pass {
|
||||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||||
{
|
{
|
||||||
|
|
||||||
log_header(design, "Executing DFFLEGALIZE pass (convert FFs to types supported by the target).\n");
|
log_header(design, "Executing DFFLEGALIZE pass (convert FFs and LATCHes to types supported by the target).\n");
|
||||||
|
|
||||||
for (int i = 0; i < NUM_FFTYPES; i++) {
|
for (int i = 0; i < NUM_FFTYPES; i++) {
|
||||||
for (int j = 0; j < NUM_NEG; j++)
|
for (int j = 0; j < NUM_NEG; j++)
|
||||||
|
|
|
||||||
|
|
@ -37,7 +37,7 @@ static std::map<RTLIL::IdString, cell_mapping> cell_mappings;
|
||||||
static void logmap(IdString dff)
|
static void logmap(IdString dff)
|
||||||
{
|
{
|
||||||
if (cell_mappings.count(dff) == 0) {
|
if (cell_mappings.count(dff) == 0) {
|
||||||
log(" unmapped dff cell: %s\n", dff);
|
log(" unmapped dff/dlatch cell: %s\n", dff);
|
||||||
} else {
|
} else {
|
||||||
log(" %s %s (", cell_mappings[dff].cell_name, dff.substr(1));
|
log(" %s %s (", cell_mappings[dff].cell_name, dff.substr(1));
|
||||||
bool first = true;
|
bool first = true;
|
||||||
|
|
@ -81,6 +81,27 @@ static void logmap_all()
|
||||||
logmap(ID($_DFFSR_PNP_));
|
logmap(ID($_DFFSR_PNP_));
|
||||||
logmap(ID($_DFFSR_PPN_));
|
logmap(ID($_DFFSR_PPN_));
|
||||||
logmap(ID($_DFFSR_PPP_));
|
logmap(ID($_DFFSR_PPP_));
|
||||||
|
|
||||||
|
logmap(ID($_DLATCH_N_));
|
||||||
|
logmap(ID($_DLATCH_P_));
|
||||||
|
|
||||||
|
logmap(ID($_DLATCH_NN0_));
|
||||||
|
logmap(ID($_DLATCH_NN1_));
|
||||||
|
logmap(ID($_DLATCH_NP0_));
|
||||||
|
logmap(ID($_DLATCH_NP1_));
|
||||||
|
logmap(ID($_DLATCH_PN0_));
|
||||||
|
logmap(ID($_DLATCH_PN1_));
|
||||||
|
logmap(ID($_DLATCH_PP0_));
|
||||||
|
logmap(ID($_DLATCH_PP1_));
|
||||||
|
|
||||||
|
logmap(ID($_DLATCHSR_NNN_));
|
||||||
|
logmap(ID($_DLATCHSR_NNP_));
|
||||||
|
logmap(ID($_DLATCHSR_NPN_));
|
||||||
|
logmap(ID($_DLATCHSR_NPP_));
|
||||||
|
logmap(ID($_DLATCHSR_PNN_));
|
||||||
|
logmap(ID($_DLATCHSR_PNP_));
|
||||||
|
logmap(ID($_DLATCHSR_PPN_));
|
||||||
|
logmap(ID($_DLATCHSR_PPP_));
|
||||||
}
|
}
|
||||||
|
|
||||||
static bool parse_next_state(const LibertyAst *cell, const LibertyAst *attr, std::string &data_name, bool &data_not_inverted, std::string &enable_name, bool &enable_not_inverted)
|
static bool parse_next_state(const LibertyAst *cell, const LibertyAst *attr, std::string &data_name, bool &data_not_inverted, std::string &enable_name, bool &enable_not_inverted)
|
||||||
|
|
@ -235,269 +256,170 @@ static bool parse_pin(const LibertyAst *cell, const LibertyAst *attr, std::strin
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
static void find_cell(std::vector<const LibertyAst *> cells, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, bool has_enable, bool enapol, std::vector<std::string> &dont_use_cells)
|
struct FfSpec {
|
||||||
|
bool is_latch = false;
|
||||||
|
bool ctrlpol = false; // clock for ff, enable for latch
|
||||||
|
bool has_reset = false, rstpol = false, rstval = false;
|
||||||
|
bool has_sr = false, setpol = false, clrpol = false;
|
||||||
|
bool dff_has_enable = false, dff_enapol = false;
|
||||||
|
};
|
||||||
|
|
||||||
|
struct BestCell {
|
||||||
|
const LibertyAst *cell = nullptr;
|
||||||
|
std::map<std::string, char> ports;
|
||||||
|
int pins = 0;
|
||||||
|
bool noninv = false;
|
||||||
|
double area = 0;
|
||||||
|
};
|
||||||
|
|
||||||
|
static bool is_dont_use(const LibertyAst *cell, std::vector<std::string> &dont_use_cells)
|
||||||
{
|
{
|
||||||
const LibertyAst *best_cell = nullptr;
|
const LibertyAst *dn = cell->find("dont_use");
|
||||||
std::map<std::string, char> best_cell_ports;
|
if (dn != nullptr && dn->value == "true")
|
||||||
int best_cell_pins = 0;
|
return true;
|
||||||
bool best_cell_noninv = false;
|
for (std::string &pat : dont_use_cells)
|
||||||
double best_cell_area = 0;
|
if (patmatch(pat.c_str(), cell->args[0].c_str()))
|
||||||
|
return true;
|
||||||
for (auto cell : cells)
|
return false;
|
||||||
{
|
|
||||||
const LibertyAst *dn = cell->find("dont_use");
|
|
||||||
if (dn != nullptr && dn->value == "true")
|
|
||||||
continue;
|
|
||||||
|
|
||||||
bool dont_use = false;
|
|
||||||
for (std::string &dont_use_cell : dont_use_cells)
|
|
||||||
{
|
|
||||||
if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str()))
|
|
||||||
{
|
|
||||||
dont_use = true;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (dont_use)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
const LibertyAst *ff = cell->find("ff");
|
|
||||||
if (ff == nullptr)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
std::string cell_clk_pin, cell_rst_pin, cell_next_pin, cell_enable_pin;
|
|
||||||
bool cell_clk_pol, cell_rst_pol, cell_next_pol, cell_enable_pol;
|
|
||||||
|
|
||||||
if (!parse_pin(cell, ff->find("clocked_on"), cell_clk_pin, cell_clk_pol) || cell_clk_pol != clkpol)
|
|
||||||
continue;
|
|
||||||
if (!parse_next_state(cell, ff->find("next_state"), cell_next_pin, cell_next_pol, cell_enable_pin, cell_enable_pol) || (has_enable && (cell_enable_pin.empty() || cell_enable_pol != enapol)))
|
|
||||||
continue;
|
|
||||||
|
|
||||||
bool cell_rstval = rstval;
|
|
||||||
if (has_reset && !cell_next_pol) {
|
|
||||||
// next_state is negated
|
|
||||||
// we later propagate this inversion to the output,
|
|
||||||
// which requires the negation of the reset value
|
|
||||||
cell_rstval = !rstval;
|
|
||||||
}
|
|
||||||
if (has_reset && cell_rstval == false) {
|
|
||||||
if (!parse_pin(cell, ff->find("clear"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol)
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
if (has_reset && cell_rstval == true) {
|
|
||||||
if (!parse_pin(cell, ff->find("preset"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol)
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::map<std::string, char> this_cell_ports;
|
|
||||||
this_cell_ports[cell_clk_pin] = 'C';
|
|
||||||
if (has_reset)
|
|
||||||
this_cell_ports[cell_rst_pin] = 'R';
|
|
||||||
if (has_enable)
|
|
||||||
this_cell_ports[cell_enable_pin] = 'E';
|
|
||||||
this_cell_ports[cell_next_pin] = 'D';
|
|
||||||
|
|
||||||
double area = 0;
|
|
||||||
const LibertyAst *ar = cell->find("area");
|
|
||||||
if (ar != nullptr && !ar->value.empty())
|
|
||||||
area = atof(ar->value.c_str());
|
|
||||||
|
|
||||||
int num_pins = 0;
|
|
||||||
bool found_output = false;
|
|
||||||
bool found_noninv_output = false;
|
|
||||||
for (auto pin : cell->children)
|
|
||||||
{
|
|
||||||
if (pin->id != "pin" || pin->args.size() != 1)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
const LibertyAst *dir = pin->find("direction");
|
|
||||||
if (dir == nullptr || dir->value == "internal")
|
|
||||||
continue;
|
|
||||||
num_pins++;
|
|
||||||
|
|
||||||
if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0)
|
|
||||||
goto continue_cell_loop;
|
|
||||||
|
|
||||||
const LibertyAst *func = pin->find("function");
|
|
||||||
if (dir->value == "output" && func != nullptr) {
|
|
||||||
std::string value = func->value;
|
|
||||||
for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t"))
|
|
||||||
value.erase(pos, 1);
|
|
||||||
if (value == ff->args[0]) {
|
|
||||||
this_cell_ports[pin->args[0]] = cell_next_pol ? 'Q' : 'q';
|
|
||||||
if (cell_next_pol)
|
|
||||||
found_noninv_output = true;
|
|
||||||
found_output = true;
|
|
||||||
} else
|
|
||||||
if (value == ff->args[1]) {
|
|
||||||
this_cell_ports[pin->args[0]] = cell_next_pol ? 'q' : 'Q';
|
|
||||||
if (!cell_next_pol)
|
|
||||||
found_noninv_output = true;
|
|
||||||
found_output = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (this_cell_ports.count(pin->args[0]) == 0)
|
|
||||||
this_cell_ports[pin->args[0]] = 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output))))
|
|
||||||
continue;
|
|
||||||
|
|
||||||
if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
best_cell = cell;
|
|
||||||
best_cell_pins = num_pins;
|
|
||||||
best_cell_area = area;
|
|
||||||
best_cell_noninv = found_noninv_output;
|
|
||||||
best_cell_ports.swap(this_cell_ports);
|
|
||||||
continue_cell_loop:;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (best_cell != nullptr) {
|
|
||||||
log(" cell %s (%sinv, pins=%d, area=%.2f) is a direct match for cell type %s.\n",
|
|
||||||
best_cell->args[0].c_str(), best_cell_noninv ? "non" : "", best_cell_pins, best_cell_area, cell_type.c_str());
|
|
||||||
cell_mappings[cell_type].cell_name = RTLIL::escape_id(best_cell->args[0]);
|
|
||||||
cell_mappings[cell_type].ports = best_cell_ports;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
static void find_cell_sr(std::vector<const LibertyAst *> cells, IdString cell_type, bool clkpol, bool setpol, bool clrpol, bool has_enable, bool enapol, std::vector<std::string> &dont_use_cells)
|
// scan the cell pins, and if the cell is a better match than the current best, record it
|
||||||
|
static void find_better_cell(BestCell &best, const LibertyAst *cell, const LibertyAst *storage, bool data_pol, std::map<std::string, char> &this_cell_ports)
|
||||||
{
|
{
|
||||||
const LibertyAst *best_cell = nullptr;
|
double area = 0;
|
||||||
std::map<std::string, char> best_cell_ports;
|
const LibertyAst *ar = cell->find("area");
|
||||||
int best_cell_pins = 0;
|
if (ar != nullptr && !ar->value.empty())
|
||||||
bool best_cell_noninv = false;
|
area = atof(ar->value.c_str());
|
||||||
double best_cell_area = 0;
|
|
||||||
|
|
||||||
log_assert(!enapol && "set/reset cell with enable is unimplemented due to lack of cells for testing");
|
int num_pins = 0;
|
||||||
|
bool found_output = false;
|
||||||
|
bool found_noninv_output = false;
|
||||||
|
for (auto pin : cell->children)
|
||||||
|
{
|
||||||
|
if (pin->id != "pin" || pin->args.size() != 1)
|
||||||
|
continue;
|
||||||
|
|
||||||
|
const LibertyAst *dir = pin->find("direction");
|
||||||
|
if (dir == nullptr || dir->value == "internal")
|
||||||
|
continue;
|
||||||
|
num_pins++;
|
||||||
|
|
||||||
|
if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0)
|
||||||
|
return;
|
||||||
|
|
||||||
|
const LibertyAst *func = pin->find("function");
|
||||||
|
if (dir->value == "output" && func != nullptr) {
|
||||||
|
std::string value = func->value;
|
||||||
|
for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t"))
|
||||||
|
value.erase(pos, 1);
|
||||||
|
if (value == storage->args[0]) {
|
||||||
|
this_cell_ports[pin->args[0]] = data_pol ? 'Q' : 'q';
|
||||||
|
if (data_pol)
|
||||||
|
found_noninv_output = true;
|
||||||
|
found_output = true;
|
||||||
|
} else
|
||||||
|
if (value == storage->args[1]) {
|
||||||
|
this_cell_ports[pin->args[0]] = data_pol ? 'q' : 'Q';
|
||||||
|
if (!data_pol)
|
||||||
|
found_noninv_output = true;
|
||||||
|
found_output = true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if (this_cell_ports.count(pin->args[0]) == 0)
|
||||||
|
this_cell_ports[pin->args[0]] = 0;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (!found_output || (best.cell != nullptr && (num_pins > best.pins || (best.noninv && !found_noninv_output))))
|
||||||
|
return;
|
||||||
|
|
||||||
|
if (best.cell != nullptr && num_pins == best.pins && area >= best.area)
|
||||||
|
return;
|
||||||
|
|
||||||
|
best.cell = cell;
|
||||||
|
best.pins = num_pins;
|
||||||
|
best.area = area;
|
||||||
|
best.noninv = found_noninv_output;
|
||||||
|
best.ports.swap(this_cell_ports);
|
||||||
|
}
|
||||||
|
|
||||||
|
static void find_cell(std::vector<const LibertyAst *> cells, IdString cell_type, FfSpec spec, std::vector<std::string> &dont_use_cells)
|
||||||
|
{
|
||||||
|
BestCell best;
|
||||||
|
|
||||||
|
log_assert(!(spec.has_sr && spec.dff_enapol) && "set/reset cell with enable is unimplemented due to lack of cells for testing");
|
||||||
|
|
||||||
|
// ff stores its state in a "ff" group with a "clocked_on" control pin, latch in a "latch" group with an "enable"
|
||||||
|
const char *group = spec.is_latch ? "latch" : "ff";
|
||||||
|
const char *ctrl_attr = spec.is_latch ? "enable" : "clocked_on";
|
||||||
|
|
||||||
for (auto cell : cells)
|
for (auto cell : cells)
|
||||||
{
|
{
|
||||||
const LibertyAst *dn = cell->find("dont_use");
|
if (is_dont_use(cell, dont_use_cells))
|
||||||
if (dn != nullptr && dn->value == "true")
|
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
bool dont_use = false;
|
const LibertyAst *storage = cell->find(group);
|
||||||
for (std::string &dont_use_cell : dont_use_cells)
|
if (storage == nullptr)
|
||||||
{
|
continue;
|
||||||
if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str()))
|
|
||||||
{
|
std::string cell_ctrl_pin, cell_rst_pin, cell_set_pin, cell_clr_pin, cell_data_pin, cell_enable_pin;
|
||||||
dont_use = true;
|
bool cell_ctrl_pol, cell_rst_pol, cell_set_pol, cell_clr_pol, cell_data_pol, cell_enable_pol;
|
||||||
break;
|
|
||||||
}
|
if (!parse_pin(cell, storage->find(ctrl_attr), cell_ctrl_pin, cell_ctrl_pol) || cell_ctrl_pol != spec.ctrlpol)
|
||||||
|
continue;
|
||||||
|
if (spec.is_latch) {
|
||||||
|
if (!parse_pin(cell, storage->find("data_in"), cell_data_pin, cell_data_pol))
|
||||||
|
continue;
|
||||||
|
} else {
|
||||||
|
if (!parse_next_state(cell, storage->find("next_state"), cell_data_pin, cell_data_pol, cell_enable_pin, cell_enable_pol) || (spec.dff_has_enable && (cell_enable_pin.empty() || cell_enable_pol != spec.dff_enapol)))
|
||||||
|
continue;
|
||||||
}
|
}
|
||||||
if (dont_use)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
const LibertyAst *ff = cell->find("ff");
|
|
||||||
if (ff == nullptr)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
std::string cell_clk_pin, cell_set_pin, cell_clr_pin, cell_next_pin, cell_enable_pin;
|
|
||||||
bool cell_clk_pol, cell_set_pol, cell_clr_pol, cell_next_pol, cell_enable_pol;
|
|
||||||
|
|
||||||
if (!parse_pin(cell, ff->find("clocked_on"), cell_clk_pin, cell_clk_pol) || cell_clk_pol != clkpol)
|
|
||||||
continue;
|
|
||||||
if (!parse_next_state(cell, ff->find("next_state"), cell_next_pin, cell_next_pol, cell_enable_pin, cell_enable_pol))
|
|
||||||
continue;
|
|
||||||
|
|
||||||
if (!parse_pin(cell, ff->find("preset"), cell_set_pin, cell_set_pol))
|
|
||||||
continue;
|
|
||||||
if (!parse_pin(cell, ff->find("clear"), cell_clr_pin, cell_clr_pol))
|
|
||||||
continue;
|
|
||||||
if (!cell_next_pol) {
|
|
||||||
// next_state is negated
|
|
||||||
// we later propagate this inversion to the output,
|
|
||||||
// which requires the swap of set and reset
|
|
||||||
std::swap(cell_set_pin, cell_clr_pin);
|
|
||||||
std::swap(cell_set_pol, cell_clr_pol);
|
|
||||||
}
|
|
||||||
if (cell_set_pol != setpol)
|
|
||||||
continue;
|
|
||||||
if (cell_clr_pol != clrpol)
|
|
||||||
continue;
|
|
||||||
|
|
||||||
std::map<std::string, char> this_cell_ports;
|
std::map<std::string, char> this_cell_ports;
|
||||||
this_cell_ports[cell_clk_pin] = 'C';
|
this_cell_ports[cell_ctrl_pin] = spec.is_latch ? 'E' : 'C';
|
||||||
this_cell_ports[cell_set_pin] = 'S';
|
|
||||||
this_cell_ports[cell_clr_pin] = 'R';
|
|
||||||
if (has_enable)
|
|
||||||
this_cell_ports[cell_enable_pin] = 'E';
|
|
||||||
this_cell_ports[cell_next_pin] = 'D';
|
|
||||||
|
|
||||||
double area = 0;
|
if (spec.has_reset) {
|
||||||
const LibertyAst *ar = cell->find("area");
|
// a negated data path is propagated to the output, which requires negating the reset value
|
||||||
if (ar != nullptr && !ar->value.empty())
|
const char *rst_attr = (spec.rstval == cell_data_pol) ? "preset" : "clear";
|
||||||
area = atof(ar->value.c_str());
|
if (!parse_pin(cell, storage->find(rst_attr), cell_rst_pin, cell_rst_pol) || cell_rst_pol != spec.rstpol)
|
||||||
|
|
||||||
int num_pins = 0;
|
|
||||||
bool found_output = false;
|
|
||||||
bool found_noninv_output = false;
|
|
||||||
for (auto pin : cell->children)
|
|
||||||
{
|
|
||||||
if (pin->id != "pin" || pin->args.size() != 1)
|
|
||||||
continue;
|
continue;
|
||||||
|
this_cell_ports[cell_rst_pin] = 'R';
|
||||||
const LibertyAst *dir = pin->find("direction");
|
|
||||||
if (dir == nullptr || dir->value == "internal")
|
|
||||||
continue;
|
|
||||||
num_pins++;
|
|
||||||
|
|
||||||
if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0)
|
|
||||||
goto continue_cell_loop;
|
|
||||||
|
|
||||||
const LibertyAst *func = pin->find("function");
|
|
||||||
if (dir->value == "output" && func != nullptr) {
|
|
||||||
std::string value = func->value;
|
|
||||||
for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t"))
|
|
||||||
value.erase(pos, 1);
|
|
||||||
if (value == ff->args[0]) {
|
|
||||||
// next_state negation propagated to output
|
|
||||||
this_cell_ports[pin->args[0]] = cell_next_pol ? 'Q' : 'q';
|
|
||||||
if (cell_next_pol)
|
|
||||||
found_noninv_output = true;
|
|
||||||
found_output = true;
|
|
||||||
} else
|
|
||||||
if (value == ff->args[1]) {
|
|
||||||
// next_state negation propagated to output
|
|
||||||
this_cell_ports[pin->args[0]] = cell_next_pol ? 'q' : 'Q';
|
|
||||||
if (!cell_next_pol)
|
|
||||||
found_noninv_output = true;
|
|
||||||
found_output = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (this_cell_ports.count(pin->args[0]) == 0)
|
|
||||||
this_cell_ports[pin->args[0]] = 0;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output))))
|
if (spec.has_sr) {
|
||||||
continue;
|
if (!parse_pin(cell, storage->find("preset"), cell_set_pin, cell_set_pol))
|
||||||
|
continue;
|
||||||
|
if (!parse_pin(cell, storage->find("clear"), cell_clr_pin, cell_clr_pol))
|
||||||
|
continue;
|
||||||
|
if (!cell_data_pol) {
|
||||||
|
// a negated data path is propagated to the output, which requires swapping set and reset
|
||||||
|
std::swap(cell_set_pin, cell_clr_pin);
|
||||||
|
std::swap(cell_set_pol, cell_clr_pol);
|
||||||
|
}
|
||||||
|
if (cell_set_pol != spec.setpol || cell_clr_pol != spec.clrpol)
|
||||||
|
continue;
|
||||||
|
this_cell_ports[cell_set_pin] = 'S';
|
||||||
|
this_cell_ports[cell_clr_pin] = 'R';
|
||||||
|
}
|
||||||
|
|
||||||
if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area)
|
if (spec.dff_has_enable)
|
||||||
continue;
|
this_cell_ports[cell_enable_pin] = 'E';
|
||||||
|
this_cell_ports[cell_data_pin] = 'D';
|
||||||
|
|
||||||
best_cell = cell;
|
find_better_cell(best, cell, storage, cell_data_pol, this_cell_ports);
|
||||||
best_cell_pins = num_pins;
|
|
||||||
best_cell_area = area;
|
|
||||||
best_cell_noninv = found_noninv_output;
|
|
||||||
best_cell_ports.swap(this_cell_ports);
|
|
||||||
continue_cell_loop:;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
if (best_cell != nullptr) {
|
if (best.cell != nullptr) {
|
||||||
log(" cell %s (%sinv, pins=%d, area=%.2f) is a direct match for cell type %s.\n",
|
log(" cell %s (%sinv, pins=%d, area=%.2f) is a direct match for cell type %s.\n",
|
||||||
best_cell->args[0].c_str(), best_cell_noninv ? "non" : "", best_cell_pins, best_cell_area, cell_type.c_str());
|
best.cell->args[0].c_str(), best.noninv ? "non" : "", best.pins, best.area, cell_type.c_str());
|
||||||
cell_mappings[cell_type].cell_name = RTLIL::escape_id(best_cell->args[0]);
|
cell_mappings[cell_type].cell_name = RTLIL::escape_id(best.cell->args[0]);
|
||||||
cell_mappings[cell_type].ports = best_cell_ports;
|
cell_mappings[cell_type].ports = best.ports;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module)
|
static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module)
|
||||||
{
|
{
|
||||||
log("Mapping DFF cells in module `%s':\n", module->name);
|
log("Mapping DFF/DLATCH cells in module `%s':\n", module->name);
|
||||||
|
|
||||||
dict<SigBit, pool<Cell*>> notmap;
|
dict<SigBit, pool<Cell*>> notmap;
|
||||||
SigMap sigmap(module);
|
SigMap sigmap(module);
|
||||||
|
|
@ -575,19 +497,19 @@ static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module)
|
||||||
}
|
}
|
||||||
|
|
||||||
struct DfflibmapPass : public Pass {
|
struct DfflibmapPass : public Pass {
|
||||||
DfflibmapPass() : Pass("dfflibmap", "technology mapping of flip-flops") { }
|
DfflibmapPass() : Pass("dfflibmap", "technology mapping of flip-flops and latches") { }
|
||||||
void help() override
|
void help() override
|
||||||
{
|
{
|
||||||
log("\n");
|
log("\n");
|
||||||
log(" dfflibmap [-prepare] [-map-only] [-info] [-dont_use <cell_name>] -liberty <file> [selection]\n");
|
log(" dfflibmap [-prepare] [-map-only] [-info] [-dont_use <cell_name>] -liberty <file> [selection]\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
log("Map internal flip-flop cells to the flip-flop cells in the technology\n");
|
log("Map internal flip-flop and latch cells to the flip-flop and latch cells in the\n");
|
||||||
log("library specified in the given liberty files.\n");
|
log("technology library specified in the given liberty files.\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
log("This pass may add inverters as needed. Therefore it is recommended to\n");
|
log("This pass may add inverters as needed. Therefore it is recommended to\n");
|
||||||
log("first run this pass and then map the logic paths to the target technology.\n");
|
log("first run this pass and then map the logic paths to the target technology.\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
log("When called with -prepare, this command will convert the internal FF cells\n");
|
log("When called with -prepare, this command will convert the internal FF/latch cells\n");
|
||||||
log("to the internal cell types that best match the cells found in the given\n");
|
log("to the internal cell types that best match the cells found in the given\n");
|
||||||
log("liberty file, but won't actually map them to the target cells.\n");
|
log("liberty file, but won't actually map them to the target cells.\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
|
|
@ -608,7 +530,7 @@ struct DfflibmapPass : public Pass {
|
||||||
}
|
}
|
||||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||||
{
|
{
|
||||||
log_header(design, "Executing DFFLIBMAP pass (mapping DFF cells to sequential cells from liberty file).\n");
|
log_header(design, "Executing DFFLIBMAP pass (mapping DFF/DLATCH cells to sequential cells from liberty file).\n");
|
||||||
log_push();
|
log_push();
|
||||||
|
|
||||||
bool prepare_mode = false;
|
bool prepare_mode = false;
|
||||||
|
|
@ -667,40 +589,61 @@ struct DfflibmapPass : public Pass {
|
||||||
delete f;
|
delete f;
|
||||||
}
|
}
|
||||||
|
|
||||||
find_cell(merged.cells, ID($_DFF_N_), false, false, false, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_N_), {}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_P_), true, false, false, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_P_), {.ctrlpol=true}, dont_use_cells);
|
||||||
|
|
||||||
find_cell(merged.cells, ID($_DFF_NN0_), false, true, false, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_NN0_), {.has_reset=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_NN1_), false, true, false, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_NN1_), {.has_reset=true, .rstval=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_NP0_), false, true, true, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_NP0_), {.has_reset=true, .rstpol=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_NP1_), false, true, true, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_NP1_), {.has_reset=true, .rstpol=true, .rstval=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_PN0_), true, true, false, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_PN0_), {.ctrlpol=true, .has_reset=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_PN1_), true, true, false, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_PN1_), {.ctrlpol=true, .has_reset=true, .rstval=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_PP0_), true, true, true, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_PP0_), {.ctrlpol=true, .has_reset=true, .rstpol=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFF_PP1_), true, true, true, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFF_PP1_), {.ctrlpol=true, .has_reset=true, .rstpol=true, .rstval=true}, dont_use_cells);
|
||||||
|
|
||||||
find_cell(merged.cells, ID($_DFFE_NN_), false, false, false, false, true, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFE_NN_), {.dff_has_enable=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFFE_NP_), false, false, false, false, true, true, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFE_NP_), {.dff_has_enable=true, .dff_enapol=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFFE_PN_), true, false, false, false, true, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFE_PN_), {.ctrlpol=true, .dff_has_enable=true}, dont_use_cells);
|
||||||
find_cell(merged.cells, ID($_DFFE_PP_), true, false, false, false, true, true, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFE_PP_), {.ctrlpol=true, .dff_has_enable=true, .dff_enapol=true}, dont_use_cells);
|
||||||
|
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_NNN_), false, false, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_NNN_), {.has_sr=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_NNP_), false, false, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_NNP_), {.has_sr=true, .clrpol=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_NPN_), false, true, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_NPN_), {.has_sr=true, .setpol=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_NPP_), false, true, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_NPP_), {.has_sr=true, .setpol=true, .clrpol=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_PNN_), true, false, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_PNN_), {.ctrlpol=true, .has_sr=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_PNP_), true, false, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_PNP_), {.ctrlpol=true, .has_sr=true, .clrpol=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_PPN_), true, true, false, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_PPN_), {.ctrlpol=true, .has_sr=true, .setpol=true}, dont_use_cells);
|
||||||
find_cell_sr(merged.cells, ID($_DFFSR_PPP_), true, true, true, false, false, dont_use_cells);
|
find_cell(merged.cells, ID($_DFFSR_PPP_), {.ctrlpol=true, .has_sr=true, .setpol=true, .clrpol=true}, dont_use_cells);
|
||||||
|
|
||||||
log(" final dff cell mappings:\n");
|
find_cell(merged.cells, ID($_DLATCH_N_), {.is_latch=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_P_), {.is_latch=true, .ctrlpol=true}, dont_use_cells);
|
||||||
|
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_NN0_), {.is_latch=true, .has_reset=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_NN1_), {.is_latch=true, .has_reset=true, .rstval=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_NP0_), {.is_latch=true, .has_reset=true, .rstpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_NP1_), {.is_latch=true, .has_reset=true, .rstpol=true, .rstval=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_PN0_), {.is_latch=true, .ctrlpol=true, .has_reset=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_PN1_), {.is_latch=true, .ctrlpol=true, .has_reset=true, .rstval=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_PP0_), {.is_latch=true, .ctrlpol=true, .has_reset=true, .rstpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCH_PP1_), {.is_latch=true, .ctrlpol=true, .has_reset=true, .rstpol=true, .rstval=true}, dont_use_cells);
|
||||||
|
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_NNN_), {.is_latch=true, .has_sr=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_NNP_), {.is_latch=true, .has_sr=true, .clrpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_NPN_), {.is_latch=true, .has_sr=true, .setpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_NPP_), {.is_latch=true, .has_sr=true, .setpol=true, .clrpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_PNN_), {.is_latch=true, .ctrlpol=true, .has_sr=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_PNP_), {.is_latch=true, .ctrlpol=true, .has_sr=true, .clrpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_PPN_), {.is_latch=true, .ctrlpol=true, .has_sr=true, .setpol=true}, dont_use_cells);
|
||||||
|
find_cell(merged.cells, ID($_DLATCHSR_PPP_), {.is_latch=true, .ctrlpol=true, .has_sr=true, .setpol=true, .clrpol=true}, dont_use_cells);
|
||||||
|
|
||||||
|
log(" final dff/dlatch cell mappings:\n");
|
||||||
logmap_all();
|
logmap_all();
|
||||||
|
|
||||||
if (!map_only_mode) {
|
if (!map_only_mode) {
|
||||||
std::string dfflegalize_cmd = "dfflegalize";
|
std::string dfflegalize_cmd = "dfflegalize";
|
||||||
for (auto it : cell_mappings)
|
for (auto it : cell_mappings)
|
||||||
dfflegalize_cmd += stringf(" -cell %s 01", it.first);
|
dfflegalize_cmd += stringf(" -cell %s 01", it.first);
|
||||||
dfflegalize_cmd += " t:$_DFF* t:$_SDFF*";
|
dfflegalize_cmd += " t:$_DFF* t:$_SDFF* t:$_DLATCH*";
|
||||||
if (info_mode) {
|
if (info_mode) {
|
||||||
log("dfflegalize command line: %s\n", dfflegalize_cmd);
|
log("dfflegalize command line: %s\n", dfflegalize_cmd);
|
||||||
} else {
|
} else {
|
||||||
|
|
|
||||||
|
|
@ -1,29 +1,47 @@
|
||||||
|
|
||||||
-- Running command `dfflibmap -info -liberty dff.lib' --
|
-- Running command `dfflibmap -info -liberty dff.lib' --
|
||||||
|
|
||||||
1. Executing DFFLIBMAP pass (mapping DFF cells to sequential cells from liberty file).
|
1. Executing DFFLIBMAP pass (mapping DFF/DLATCH cells to sequential cells from liberty file).
|
||||||
cell dff (noninv, pins=3, area=1.00) is a direct match for cell type $_DFF_P_.
|
cell dff (noninv, pins=3, area=1.00) is a direct match for cell type $_DFF_P_.
|
||||||
final dff cell mappings:
|
final dff/dlatch cell mappings:
|
||||||
unmapped dff cell: $_DFF_N_
|
unmapped dff/dlatch cell: $_DFF_N_
|
||||||
\dff _DFF_P_ (.CLK( C), .D( D), .Q( Q));
|
\dff _DFF_P_ (.CLK( C), .D( D), .Q( Q));
|
||||||
unmapped dff cell: $_DFF_NN0_
|
unmapped dff/dlatch cell: $_DFF_NN0_
|
||||||
unmapped dff cell: $_DFF_NN1_
|
unmapped dff/dlatch cell: $_DFF_NN1_
|
||||||
unmapped dff cell: $_DFF_NP0_
|
unmapped dff/dlatch cell: $_DFF_NP0_
|
||||||
unmapped dff cell: $_DFF_NP1_
|
unmapped dff/dlatch cell: $_DFF_NP1_
|
||||||
unmapped dff cell: $_DFF_PN0_
|
unmapped dff/dlatch cell: $_DFF_PN0_
|
||||||
unmapped dff cell: $_DFF_PN1_
|
unmapped dff/dlatch cell: $_DFF_PN1_
|
||||||
unmapped dff cell: $_DFF_PP0_
|
unmapped dff/dlatch cell: $_DFF_PP0_
|
||||||
unmapped dff cell: $_DFF_PP1_
|
unmapped dff/dlatch cell: $_DFF_PP1_
|
||||||
unmapped dff cell: $_DFFE_NN_
|
unmapped dff/dlatch cell: $_DFFE_NN_
|
||||||
unmapped dff cell: $_DFFE_NP_
|
unmapped dff/dlatch cell: $_DFFE_NP_
|
||||||
unmapped dff cell: $_DFFE_PN_
|
unmapped dff/dlatch cell: $_DFFE_PN_
|
||||||
unmapped dff cell: $_DFFE_PP_
|
unmapped dff/dlatch cell: $_DFFE_PP_
|
||||||
unmapped dff cell: $_DFFSR_NNN_
|
unmapped dff/dlatch cell: $_DFFSR_NNN_
|
||||||
unmapped dff cell: $_DFFSR_NNP_
|
unmapped dff/dlatch cell: $_DFFSR_NNP_
|
||||||
unmapped dff cell: $_DFFSR_NPN_
|
unmapped dff/dlatch cell: $_DFFSR_NPN_
|
||||||
unmapped dff cell: $_DFFSR_NPP_
|
unmapped dff/dlatch cell: $_DFFSR_NPP_
|
||||||
unmapped dff cell: $_DFFSR_PNN_
|
unmapped dff/dlatch cell: $_DFFSR_PNN_
|
||||||
unmapped dff cell: $_DFFSR_PNP_
|
unmapped dff/dlatch cell: $_DFFSR_PNP_
|
||||||
unmapped dff cell: $_DFFSR_PPN_
|
unmapped dff/dlatch cell: $_DFFSR_PPN_
|
||||||
unmapped dff cell: $_DFFSR_PPP_
|
unmapped dff/dlatch cell: $_DFFSR_PPP_
|
||||||
dfflegalize command line: dfflegalize -cell $_DFF_P_ 01 t:$_DFF* t:$_SDFF*
|
unmapped dff/dlatch cell: $_DLATCH_N_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_P_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_NN0_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_NN1_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_NP0_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_NP1_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_PN0_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_PN1_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_PP0_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCH_PP1_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_NNN_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_NNP_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_NPN_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_NPP_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_PNN_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_PNP_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_PPN_
|
||||||
|
unmapped dff/dlatch cell: $_DLATCHSR_PPP_
|
||||||
|
dfflegalize command line: dfflegalize -cell $_DFF_P_ 01 t:$_DFF* t:$_SDFF* t:$_DLATCH*
|
||||||
|
|
|
||||||
|
|
@ -23,9 +23,11 @@ read_liberty -lib dfflibmap.lib
|
||||||
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
|
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
|
||||||
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
|
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
|
||||||
|
|
||||||
dfflibmap -prepare -liberty dffl*bmap.lib
|
dfflibmap -prepare -liberty dfflibmap.lib
|
||||||
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
|
equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
design -load orig
|
design -load orig
|
||||||
dfflibmap -liberty dfflibmap.lib
|
dfflibmap -liberty dfflibmap.lib
|
||||||
clean
|
clean
|
||||||
|
|
@ -74,6 +76,8 @@ select -assert-count 1 t:dffe
|
||||||
select -assert-count 4 t:dffsr
|
select -assert-count 4 t:dffsr
|
||||||
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
|
select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
design -load orig
|
design -load orig
|
||||||
dfflibmap -liberty dfflibmap.lib -dont_use *ffn
|
dfflibmap -liberty dfflibmap.lib -dont_use *ffn
|
||||||
clean
|
clean
|
||||||
|
|
@ -82,6 +86,12 @@ select -assert-count 0 t:dffn
|
||||||
select -assert-count 5 t:dffsr
|
select -assert-count 5 t:dffsr
|
||||||
select -assert-count 1 t:dffe
|
select -assert-count 1 t:dffe
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
read_liberty -lib dfflibmap.lib dfflibmap_dffsr_mixedpol.lib
|
||||||
|
equiv_opt -map dfflibmap-sim.v -map dfflibmap_dffsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
|
||||||
|
|
||||||
design -load orig
|
design -load orig
|
||||||
dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
|
dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
|
||||||
clean
|
clean
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dffsr) {
|
||||||
|
area : 6;
|
||||||
|
ff("IQ", "IQN") {
|
||||||
|
next_state : "D";
|
||||||
|
clocked_on : "CLK";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : H;
|
||||||
|
clear_preset_var2 : H;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLK) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dffsr) {
|
||||||
|
area : 6;
|
||||||
|
ff("IQ", "IQN") {
|
||||||
|
next_state : "D";
|
||||||
|
clocked_on : "CLK";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : L;
|
||||||
|
clear_preset_var2 : L;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLK) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,10 @@
|
||||||
|
module dffsr_mixedpol(input CLK, D, CLEAR, PRESET, output reg Q, output QN);
|
||||||
|
|
||||||
|
always @(posedge CLK, negedge CLEAR, posedge PRESET)
|
||||||
|
if (PRESET) Q <= 1'b1;
|
||||||
|
else if (~CLEAR) Q <= 1'b0;
|
||||||
|
else Q <= ~D;
|
||||||
|
|
||||||
|
assign QN = ~Q;
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
@ -88,6 +88,86 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||||
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||||
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||||
|
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||||
|
|
||||||
|
assign Q[11:6] = ~Q[5:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dfflibmap_dffsr_l.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dfflibmap_dffsr_l.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input C, D, E, S, R, output [11:0] Q);
|
||||||
|
|
||||||
|
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||||
|
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||||
|
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
|
||||||
|
|
||||||
|
assign Q[11:6] = ~Q[5:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dfflibmap_dffsr_h.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dfflibmap_dffsr_h.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input C, D, E, S, R, output [11:0] Q);
|
||||||
|
|
||||||
|
$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
|
||||||
|
$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
// no assume when mapping to X
|
// no assume when mapping to X
|
||||||
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||||
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
|
||||||
|
|
@ -5,36 +5,24 @@ read_verilog -sv -icells <<EOT
|
||||||
module top(input C, D, E, S, R, output [7:0] Q);
|
module top(input C, D, E, S, R, output [7:0] Q);
|
||||||
|
|
||||||
always @( posedge C, posedge S, posedge R)
|
always @( posedge C, posedge S, posedge R)
|
||||||
if (R)
|
if (R) Q[0] <= 0;
|
||||||
Q[0] <= 0;
|
else if (S) Q[0] <= 1;
|
||||||
else if (S)
|
else Q[0] <= D;
|
||||||
Q[0] <= 1;
|
|
||||||
else
|
|
||||||
Q[0] <= D;
|
|
||||||
|
|
||||||
always @( posedge C, posedge S, posedge R)
|
always @( posedge C, posedge S, posedge R)
|
||||||
if (S)
|
if (S) Q[1] <= 1;
|
||||||
Q[1] <= 1;
|
else if (R) Q[1] <= 0;
|
||||||
else if (R)
|
else Q[1] <= D;
|
||||||
Q[1] <= 0;
|
|
||||||
else
|
|
||||||
Q[1] <= D;
|
|
||||||
|
|
||||||
always @( posedge C, posedge S, posedge R)
|
always @( posedge C, posedge S, posedge R)
|
||||||
if (R)
|
if (R) Q[2] <= 0;
|
||||||
Q[2] <= 0;
|
else if (S) Q[2] <= 1;
|
||||||
else if (S)
|
else if (E) Q[2] <= D;
|
||||||
Q[2] <= 1;
|
|
||||||
else if (E)
|
|
||||||
Q[2] <= D;
|
|
||||||
|
|
||||||
always @( posedge C, posedge S, posedge R)
|
always @( posedge C, posedge S, posedge R)
|
||||||
if (S)
|
if (S) Q[3] <= 1;
|
||||||
Q[3] <= 1;
|
else if (R) Q[3] <= 0;
|
||||||
else if (R)
|
else if (E) Q[3] <= D;
|
||||||
Q[3] <= 0;
|
|
||||||
else if (E)
|
|
||||||
Q[3] <= D;
|
|
||||||
|
|
||||||
assign Q[7:4] = ~Q[3:0];
|
assign Q[7:4] = ~Q[3:0];
|
||||||
|
|
||||||
|
|
@ -81,6 +69,36 @@ sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
##################################################################
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 4" 1
|
||||||
|
dfflibmap -liberty dfflibmap_dffsr_l.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dfflibmap_dffsr_l.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 4" 1
|
||||||
|
dfflibmap -liberty dfflibmap_dffsr_h.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dfflibmap_dffsr_h.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
design -load start
|
design -load start
|
||||||
logger -expect log " mapped 4" 1
|
logger -expect log " mapped 4" 1
|
||||||
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
|
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
|
||||||
|
|
@ -108,3 +126,18 @@ miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
# Prove that this is equivalent
|
# Prove that this is equivalent
|
||||||
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 4" 1
|
||||||
|
dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dfflibmap_dffsr_not_next_l.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,19 @@
|
||||||
|
module dlatchn(input ENA, D, output reg Q, output QN);
|
||||||
|
|
||||||
|
always @*
|
||||||
|
if (~ENA) Q <= D;
|
||||||
|
|
||||||
|
assign QN = ~Q;
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module dlatchsr(input ENA, D, CLEAR, PRESET, output reg Q, output QN);
|
||||||
|
|
||||||
|
always @*
|
||||||
|
if (CLEAR) Q <= 1'b0;
|
||||||
|
else if (PRESET) Q <= 1'b1;
|
||||||
|
else if (ENA) Q <= D;
|
||||||
|
|
||||||
|
assign QN = ~Q;
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
@ -0,0 +1,55 @@
|
||||||
|
library(test) {
|
||||||
|
/* D-type latch with reset and preset */
|
||||||
|
cell (dlatchn) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "!ENA";
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
cell (dlatchsr) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : L;
|
||||||
|
clear_preset_var2 : L;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,107 @@
|
||||||
|
read_verilog -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R(R), .S(S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(R), .S(S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
simplemap
|
||||||
|
|
||||||
|
design -save orig
|
||||||
|
read_liberty -lib dlatchlibmap.lib
|
||||||
|
|
||||||
|
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib
|
||||||
|
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||||
|
|
||||||
|
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||||
|
equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -liberty dlatchlibmap.lib
|
||||||
|
clean
|
||||||
|
|
||||||
|
select -assert-count 4 t:$_NOT_
|
||||||
|
select -assert-count 1 t:dlatchn
|
||||||
|
select -assert-count 4 t:dlatchsr
|
||||||
|
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||||
|
|
||||||
|
select -assert-count 9 t:$_NOT_
|
||||||
|
select -assert-count 1 t:$_DLATCH_N_
|
||||||
|
select -assert-count 4 t:$_DLATCHSR_PPP_
|
||||||
|
select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||||
|
|
||||||
|
select -assert-count 5 t:$_NOT_
|
||||||
|
select -assert-count 0 t:dlatchn
|
||||||
|
select -assert-count 1 t:dlatchsr
|
||||||
|
select -assert-count 1 t:$_DLATCH_P_
|
||||||
|
select -assert-count 1 t:$_DLATCH_PP0_
|
||||||
|
select -assert-count 1 t:$_DLATCH_PP1_
|
||||||
|
select -assert-count 1 t:$_DLATCHSR_NNN_
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -prepare -liberty dlatchlibmap.lib
|
||||||
|
dfflibmap -map-only -liberty dlatchlibmap.lib
|
||||||
|
clean
|
||||||
|
|
||||||
|
select -assert-count 4 t:$_NOT_
|
||||||
|
select -assert-count 1 t:dlatchn
|
||||||
|
select -assert-count 4 t:dlatchsr
|
||||||
|
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -prepare -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
|
||||||
|
dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
|
||||||
|
clean
|
||||||
|
|
||||||
|
select -assert-count 4 t:$_NOT_
|
||||||
|
select -assert-count 1 t:dlatchn
|
||||||
|
select -assert-count 4 t:dlatchsr
|
||||||
|
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -liberty dlatchlibmap.lib -dont_use *latchn
|
||||||
|
clean
|
||||||
|
|
||||||
|
select -assert-count 0 t:dlatchn
|
||||||
|
select -assert-count 5 t:dlatchsr
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
read_liberty -lib dlatchlibmap.lib dlatchlibmap_dlatchsr_mixedpol.lib
|
||||||
|
equiv_opt -map dlatchlibmap-sim.v -map dlatchlibmap_dlatchsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
|
||||||
|
|
||||||
|
design -load orig
|
||||||
|
dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
|
||||||
|
clean
|
||||||
|
|
||||||
|
# We have one more _NOT_ than with the regular dlatchsr
|
||||||
|
select -assert-count 5 t:$_NOT_
|
||||||
|
select -assert-count 1 t:dlatchn
|
||||||
|
select -assert-count 4 t:dlatchsr_mixedpol
|
||||||
|
# The additional NOT is on latch2.
|
||||||
|
# Originally, latch2.R is an active high "preset".
|
||||||
|
# dlatchsr_mixedpol has functionally swapped labels due to the data_in inversion,
|
||||||
|
# so we use its CLEAR port for the "preset",
|
||||||
|
# but we have to invert it because the CLEAR pin is active low.
|
||||||
|
# latch2.CLEAR = !R
|
||||||
|
select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i
|
||||||
|
|
@ -0,0 +1,23 @@
|
||||||
|
library (test_not_data) {
|
||||||
|
cell (dff_not_data) {
|
||||||
|
area: 1.0;
|
||||||
|
pin (QN) {
|
||||||
|
direction : output;
|
||||||
|
function : "STATE";
|
||||||
|
}
|
||||||
|
pin (ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin (D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin (RN) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
latch (STATE, STATEN) {
|
||||||
|
enable: "ENA";
|
||||||
|
data_in: "!D";
|
||||||
|
preset : "!RN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,23 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchn) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "!ENA";
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : H;
|
||||||
|
clear_preset_var2 : H;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : L;
|
||||||
|
clear_preset_var2 : L;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,10 @@
|
||||||
|
module dlatchsr_mixedpol(input ENA, D, CLEAR, PRESET, output reg Q, output QN);
|
||||||
|
|
||||||
|
always @*
|
||||||
|
if (PRESET) Q <= 1'b1;
|
||||||
|
else if (~CLEAR) Q <= 1'b0;
|
||||||
|
else if (ENA) Q <= ~D;
|
||||||
|
|
||||||
|
assign QN = ~Q;
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr_mixedpol) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "!D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "!CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : L;
|
||||||
|
clear_preset_var2 : L;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,27 @@
|
||||||
|
library (test_not_data) {
|
||||||
|
cell (dlatchsr_not_data) {
|
||||||
|
area : 1.0;
|
||||||
|
pin (Q) {
|
||||||
|
direction : output;
|
||||||
|
function : "STATE";
|
||||||
|
}
|
||||||
|
pin (ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin (D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin (RN) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin (SN) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
latch (STATE,STATEN) {
|
||||||
|
clear : "!SN";
|
||||||
|
enable : "ENA";
|
||||||
|
data_in : "!D";
|
||||||
|
preset : "!RN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr_not_data_l) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "!D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : L;
|
||||||
|
clear_preset_var2 : L;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : L;
|
||||||
|
clear_preset_var2 : H;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : H;
|
||||||
|
clear_preset_var2 : L;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,33 @@
|
||||||
|
library(test) {
|
||||||
|
cell (dlatchsr) {
|
||||||
|
area : 6;
|
||||||
|
latch("IQ", "IQN") {
|
||||||
|
data_in : "D";
|
||||||
|
enable : "ENA";
|
||||||
|
clear : "CLEAR";
|
||||||
|
preset : "PRESET";
|
||||||
|
clear_preset_var1 : X;
|
||||||
|
clear_preset_var2 : X;
|
||||||
|
}
|
||||||
|
pin(D) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(ENA) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(CLEAR) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(PRESET) {
|
||||||
|
direction : input;
|
||||||
|
}
|
||||||
|
pin(Q) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQ";
|
||||||
|
}
|
||||||
|
pin(QN) {
|
||||||
|
direction: output;
|
||||||
|
function : "IQN";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -0,0 +1,325 @@
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_s.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_r.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_l.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_h.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_h.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
// no assume when mapping to X
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_x.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_x.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
// no assume when mapping to unset clear_preset_var
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchn.lib
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [9:0] Q);
|
||||||
|
|
||||||
|
$_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0]));
|
||||||
|
$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
|
||||||
|
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
|
||||||
|
|
||||||
|
assume property (~R || ~S);
|
||||||
|
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
|
||||||
|
$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4]));
|
||||||
|
|
||||||
|
assign Q[9:5] = ~Q[4:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_not_data_l.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
hierarchy -top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent with the assumption
|
||||||
|
sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
|
||||||
|
# Prove that this is NOT equivalent WITHOUT the assumption
|
||||||
|
sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output Q);
|
||||||
|
// DLATCHSR with priority R over S
|
||||||
|
always @*
|
||||||
|
if (R) Q <= 1'b0;
|
||||||
|
else if (S) Q <= 1'b1;
|
||||||
|
else if (E) Q <= D;
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchn.lib
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
simplemap top
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
equiv_make top top_unmapped equiv
|
||||||
|
equiv_induct -set-assumes equiv
|
||||||
|
equiv_status -assert equiv
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, R, output Q);
|
||||||
|
// DLATCH with preset
|
||||||
|
always @*
|
||||||
|
if (~R) Q <= 1'b1;
|
||||||
|
else if (E) Q <= D;
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
read_liberty dlatchlibmap_dlatchn.lib
|
||||||
|
read_liberty dlatchlibmap_dlatch_not_data.lib
|
||||||
|
|
||||||
|
copy top top_unmapped
|
||||||
|
simplemap top
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatch_not_data.lib top
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
equiv_make top top_unmapped equiv
|
||||||
|
equiv_induct -set-assumes equiv
|
||||||
|
equiv_status -assert equiv
|
||||||
|
|
@ -0,0 +1,133 @@
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
read_verilog -sv -icells <<EOT
|
||||||
|
|
||||||
|
module top(input E, D, S, R, output [3:0] Q);
|
||||||
|
|
||||||
|
always_latch
|
||||||
|
if (R) Q[0] <= 1'b0;
|
||||||
|
else if (S) Q[0] <= 1'b1;
|
||||||
|
else if (E) Q[0] <= D;
|
||||||
|
|
||||||
|
always_latch
|
||||||
|
if (S) Q[1] <= 1'b1;
|
||||||
|
else if (R) Q[1] <= 1'b0;
|
||||||
|
else if (E) Q[1] <= D;
|
||||||
|
|
||||||
|
assign Q[3:2] = ~Q[1:0];
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt
|
||||||
|
techmap
|
||||||
|
copy top top_unmapped
|
||||||
|
design -save start
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_s.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
opt_clean -purge
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_r.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_l.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_h.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_h.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_mixedpol.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_mixedpol.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_not_data.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
||||||
|
##################################################################
|
||||||
|
|
||||||
|
design -load start
|
||||||
|
logger -expect log " mapped 2" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
|
||||||
|
logger -check-expected
|
||||||
|
read_liberty dlatchlibmap_dlatchsr_not_data_l.lib
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
flatten
|
||||||
|
miter -equiv -make_assert -flatten top_unmapped top miter
|
||||||
|
|
||||||
|
# Prove that this is equivalent
|
||||||
|
sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
|
||||||
|
|
@ -0,0 +1,5 @@
|
||||||
|
read_verilog ../sim/dlatch.v
|
||||||
|
proc
|
||||||
|
logger -expect error "not supported" 1
|
||||||
|
dfflibmap -liberty dlatchlibmap.lib
|
||||||
|
logger -check-expected
|
||||||
Loading…
Reference in New Issue