Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: b72a7e110455
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: e91548b33e62
Choose a head ref
  • 3 commits
  • 3 files changed
  • 1 contributor

Commits on Apr 26, 2017

  1. Copy the full SHA
    f0db8ff View commit details

Commits on Apr 28, 2017

  1. Copy the full SHA
    3bbac5c View commit details

Commits on Apr 30, 2017

  1. Copy the full SHA
    e91548b View commit details
Showing with 55 additions and 11 deletions.
  1. +7 −0 frontends/verilog/preproc.cc
  2. +7 −1 frontends/verilog/verilog_parser.y
  3. +41 −10 passes/equiv/equiv_simple.cc
7 changes: 7 additions & 0 deletions frontends/verilog/preproc.cc
Original file line number Diff line number Diff line change
@@ -438,6 +438,13 @@ std::string frontend_verilog_preproc(std::istream &f, std::string filename, cons
continue;
}

if (tok == "`resetall") {
defines_map.clear();
defines_with_args.clear();
global_defines_cache.clear();
continue;
}

if (tok.size() > 1 && tok[0] == '`' && defines_map.count(tok.substr(1)) > 0) {
std::string name = tok.substr(1);
// printf("expand: >>%s<< -> >>%s<<\n", name.c_str(), defines_map[name].c_str());
8 changes: 7 additions & 1 deletion frontends/verilog/verilog_parser.y
Original file line number Diff line number Diff line change
@@ -272,7 +272,13 @@ single_module_para:
if (astbuf1) delete astbuf1;
astbuf1 = new AstNode(AST_PARAMETER);
astbuf1->children.push_back(AstNode::mkconst_int(0, true));
} param_signed param_integer param_range single_param_decl | single_param_decl;
} param_signed param_integer param_range single_param_decl |
TOK_LOCALPARAM {
if (astbuf1) delete astbuf1;
astbuf1 = new AstNode(AST_LOCALPARAM);
astbuf1->children.push_back(AstNode::mkconst_int(0, true));
} param_signed param_integer param_range single_param_decl |
single_param_decl;

module_args_opt:
'(' ')' | /* empty */ | '(' module_args optional_comma ')';
51 changes: 41 additions & 10 deletions passes/equiv/equiv_simple.cc
Original file line number Diff line number Diff line change
@@ -35,13 +35,14 @@ struct EquivSimpleWorker
ezSatPtr ez;
SatGen satgen;
int max_seq;
bool short_cones;
bool verbose;

pool<pair<Cell*, int>> imported_cells_cache;

EquivSimpleWorker(const vector<Cell*> &equiv_cells, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool verbose, bool model_undef) :
EquivSimpleWorker(const vector<Cell*> &equiv_cells, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool short_cones, bool verbose, bool model_undef) :
module(equiv_cells.front()->module), equiv_cells(equiv_cells), equiv_cell(nullptr),
sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), verbose(verbose)
sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), short_cones(short_cones), verbose(verbose)
{
satgen.model_undef = model_undef;
}
@@ -142,22 +143,44 @@ struct EquivSimpleWorker
pool<SigBit> short_bits_cone_a, short_bits_cone_b;
pool<SigBit> input_bits;

for (auto bit_a : seed_a)
find_input_cone(next_seed_a, short_cells_cone_a, short_bits_cone_a, full_cells_cone_b, full_bits_cone_b, &input_bits, bit_a);
next_seed_a.swap(seed_a);
if (short_cones)
{
for (auto bit_a : seed_a)
find_input_cone(next_seed_a, short_cells_cone_a, short_bits_cone_a, full_cells_cone_b, full_bits_cone_b, &input_bits, bit_a);
next_seed_a.swap(seed_a);

for (auto bit_b : seed_b)
find_input_cone(next_seed_b, short_cells_cone_b, short_bits_cone_b, full_cells_cone_a, full_bits_cone_a, &input_bits, bit_b);
next_seed_b.swap(seed_b);
for (auto bit_b : seed_b)
find_input_cone(next_seed_b, short_cells_cone_b, short_bits_cone_b, full_cells_cone_a, full_bits_cone_a, &input_bits, bit_b);
next_seed_b.swap(seed_b);
}
else
{
short_cells_cone_a = full_cells_cone_a;
short_bits_cone_a = full_bits_cone_a;
next_seed_a.swap(seed_a);

short_cells_cone_b = full_cells_cone_b;
short_bits_cone_b = full_bits_cone_b;
next_seed_b.swap(seed_b);
}

pool<Cell*> problem_cells;
problem_cells.insert(short_cells_cone_a.begin(), short_cells_cone_a.end());
problem_cells.insert(short_cells_cone_b.begin(), short_cells_cone_b.end());

if (verbose)
{
log(" Adding %d new cells to the problem (%d A, %d B, %d shared).\n",
GetSize(problem_cells), GetSize(short_cells_cone_a), GetSize(short_cells_cone_b),
(GetSize(short_cells_cone_a) + GetSize(short_cells_cone_b)) - GetSize(problem_cells));
#if 0
for (auto cell : short_cells_cone_a)
log(" A-side cell: %s\n", log_id(cell));

for (auto cell : short_cells_cone_b)
log(" B-side cell: %s\n", log_id(cell));
#endif
}

for (auto cell : problem_cells) {
auto key = pair<Cell*, int>(cell, step+1);
@@ -264,6 +287,10 @@ struct EquivSimplePass : public Pass {
log(" -undef\n");
log(" enable modelling of undef states\n");
log("\n");
log(" -short\n");
log(" create shorter input cones that stop at shared nodes. This yields\n");
log(" simpler SAT problems but sometimes fails to prove equivalence.\n");
log("\n");
log(" -nogroup\n");
log(" disabling grouping of $equiv cells by output wire\n");
log("\n");
@@ -273,7 +300,7 @@ struct EquivSimplePass : public Pass {
}
virtual void execute(std::vector<std::string> args, Design *design)
{
bool verbose = false, model_undef = false, nogroup = false;
bool verbose = false, short_cones = false, model_undef = false, nogroup = false;
int success_counter = 0;
int max_seq = 1;

@@ -285,6 +312,10 @@ struct EquivSimplePass : public Pass {
verbose = true;
continue;
}
if (args[argidx] == "-short") {
short_cones = true;
continue;
}
if (args[argidx] == "-undef") {
model_undef = true;
continue;
@@ -346,7 +377,7 @@ struct EquivSimplePass : public Pass {
for (auto it2 : it.second)
cells.push_back(it2.second);

EquivSimpleWorker worker(cells, sigmap, bit2driver, max_seq, verbose, model_undef);
EquivSimpleWorker worker(cells, sigmap, bit2driver, max_seq, short_cones, verbose, model_undef);
success_counter += worker.run();
}
}