From db7fc0e32d905e7447b7f9f93d611d3d09ad7b24 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 27 Feb 2017 13:25:28 +0100 Subject: [PATCH] Add "chformal" pass --- passes/cmds/Makefile.inc | 1 + passes/cmds/chformal.cc | 238 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 239 insertions(+) create mode 100644 passes/cmds/chformal.cc diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc index 01ada7739..0a4ed1537 100644 --- a/passes/cmds/Makefile.inc +++ b/passes/cmds/Makefile.inc @@ -25,4 +25,5 @@ OBJS += passes/cmds/plugin.o OBJS += passes/cmds/check.o OBJS += passes/cmds/qwp.o OBJS += passes/cmds/edgetypes.o +OBJS += passes/cmds/chformal.o diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc new file mode 100644 index 000000000..4200a5583 --- /dev/null +++ b/passes/cmds/chformal.cc @@ -0,0 +1,238 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct ChformalPass : public Pass { + ChformalPass() : Pass("chformal", "change formal constraints of the design") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" chformal [types] [mode] [options] [selection]\n"); + log("\n"); + log("Make changes to the formal constraints of the design. The [types] options\n"); + log("the type of constraint to operate on. If none of the folling options is given,\n"); + log("the command will operate on all constraint types:\n"); + log("\n"); + log(" -assert $assert cells, representing assert(...) constraints\n"); + log(" -assume $assume cells, representing assume(...) constraints\n"); + log(" -live $live cells, representing assert(s_eventually ...)\n"); + log(" -fair $fair cells, representing assume(s_eventually ...)\n"); + log(" -cover $cover cells, representing cover() statements\n"); + log("\n"); + log("Exactly one of the following modes must be specified:\n"); + log("\n"); + log(" -remove\n"); + log(" remove the cells and thus constraints from the design\n"); + log("\n"); + log(" -early\n"); + log(" bypass FFs that only delay the activation of a constraint\n"); + log("\n"); + log(" -delay \n"); + log(" delay activation of the constraint by clock cycles\n"); + log("\n"); + log(" -skip \n"); + log(" ignore activation of the constraint in the first clock cycles\n"); + log("\n"); + } + virtual void execute(std::vector args, RTLIL::Design *design) + { + pool constr_types; + char mode = 0; + int mode_arg; + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-assert") { + constr_types.insert("$assert"); + continue; + } + if (args[argidx] == "-assume") { + constr_types.insert("$assume"); + continue; + } + if (args[argidx] == "-live") { + constr_types.insert("$live"); + continue; + } + if (args[argidx] == "-fair") { + constr_types.insert("$fair"); + continue; + } + if (args[argidx] == "-cover") { + constr_types.insert("$cover"); + continue; + } + if (mode == 0 && args[argidx] == "-remove") { + mode = 'r'; + continue; + } + if (mode == 0 && args[argidx] == "-early") { + mode = 'e'; + continue; + } + if (mode == 0 && args[argidx] == "-delay" && argidx+1 < args.size()) { + mode = 'd'; + mode_arg = atoi(args[++argidx].c_str()); + continue; + } + if (mode == 0 && args[argidx] == "-skip" && argidx+1 < args.size()) { + mode = 's'; + mode_arg = atoi(args[++argidx].c_str()); + continue; + } + break; + } + extra_args(args, argidx, design); + + if (constr_types.empty()) { + constr_types.insert("$assert"); + constr_types.insert("$assume"); + constr_types.insert("$live"); + constr_types.insert("$fair"); + constr_types.insert("$cover"); + } + + if (mode == 0) + log_cmd_error("Mode option is missing.\n"); + + for (auto module : design->selected_modules()) + { + vector constr_cells; + + for (auto cell : module->selected_cells()) + if (constr_types.count(cell->type)) + constr_cells.push_back(cell); + + if (mode == 'r') + { + for (auto cell : constr_cells) + module->remove(cell); + } + else + if (mode == 'e') + { + SigMap sigmap(module); + dict>> ffmap; + pool init_zero, init_one; + + for (auto wire : module->wires()) + { + if (wire->attributes.count("\\init") == 0) + continue; + + SigSpec initsig = sigmap(wire); + Const initval = wire->attributes.at("\\init"); + + for (int i = 0; i < GetSize(initsig) && i < GetSize(initval); i++) { + if (initval[i] == State::S0) + init_zero.insert(initsig[i]); + if (initval[i] == State::S1) + init_one.insert(initsig[i]); + } + } + + for (auto cell : module->selected_cells()) + { + if (cell->type == "$ff") { + SigSpec D = sigmap(cell->getPort("\\D")); + SigSpec Q = sigmap(cell->getPort("\\Q")); + for (int i = 0; i < GetSize(D); i++) + ffmap[Q[i]] = make_pair(D[i], make_pair(State::Sm, false)); + } + if (cell->type == "$dff") { + SigSpec D = sigmap(cell->getPort("\\D")); + SigSpec Q = sigmap(cell->getPort("\\Q")); + SigSpec C = sigmap(cell->getPort("\\CLK")); + bool clockpol = cell->getParam("\\CLK_POLARITY").as_bool(); + for (int i = 0; i < GetSize(D); i++) + ffmap[Q[i]] = make_pair(D[i], make_pair(C, clockpol)); + } + } + + for (auto cell : constr_cells) + while (true) + { + SigSpec A = sigmap(cell->getPort("\\A")); + SigSpec EN = sigmap(cell->getPort("\\EN")); + + if (ffmap.count(A) == 0 || ffmap.count(EN) == 0) + break; + + if (!init_zero.count(EN)) { + if (cell->type == "$cover") break; + if (cell->type.in("$assert", "$assume") && !init_one.count(A)) break; + } + + const auto &A_map = ffmap.at(A); + const auto &EN_map = ffmap.at(EN); + + if (A_map.second != EN_map.second) + break; + + cell->setPort("\\A", A_map.first); + cell->setPort("\\EN", EN_map.first); + } + } + else + if (mode == 'd') + { + for (auto cell : constr_cells) + for (int i = 0; i < mode_arg; i++) + { + SigSpec orig_a = cell->getPort("\\A"); + SigSpec orig_en = cell->getPort("\\EN"); + + Wire *new_a = module->addWire(NEW_ID); + Wire *new_en = module->addWire(NEW_ID); + new_en->attributes["\\init"] = State::S0; + + module->addFf(NEW_ID, orig_a, new_a); + module->addFf(NEW_ID, orig_en, new_en); + + cell->setPort("\\A", new_a); + cell->setPort("\\EN", new_en); + } + } + else + if (mode == 's') + { + SigSpec en = State::S1; + + for (int i = 0; i < mode_arg; i++) { + Wire *w = module->addWire(NEW_ID); + w->attributes["\\init"] = State::S0; + module->addFf(NEW_ID, en, w); + en = w; + } + + for (auto cell : constr_cells) + cell->setPort("\\EN", module->LogicAnd(NEW_ID, en, cell->getPort("\\EN"))); + } + } + } +} ChformalPass; + +PRIVATE_NAMESPACE_END -- 2.30.2