From c6d15c9aade55a87595693ecb9170ae8b595e28c Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:07:03 -0700 Subject: Revert "Update doc for equiv_opt" This reverts commit a274b7cc86d4f64541d3d2903b4eeed4616ab1d8. --- passes/equiv/equiv_opt.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index 4ab5b1a3e..9fe3bbd57 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -32,8 +32,7 @@ struct EquivOptPass:public ScriptPass log("\n"); log(" equiv_opt [options] [command]\n"); log("\n"); - log("This command uses temporal induction to check circuit equivalence before and\n"); - log("after an optimization pass.\n"); + log("This command checks circuit equivalence before and after an optimization pass.\n"); log("\n"); log(" -run :\n"); log(" only run the commands between the labels (see below). an empty\n"); @@ -157,7 +156,7 @@ struct EquivOptPass:public ScriptPass if (check_label("prove")) { if (multiclock || help_mode) run("clk2fflogic", "(only with -multiclock)"); - if (!multiclock || help_mode) + else run("async2sync", "(only without -multiclock)"); run("equiv_make gold gate equiv"); if (help_mode) -- cgit v1.2.3 From 8765ec3c27f38e6fb57d057be9605788e144388b Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:07:15 -0700 Subject: Revert "equiv_opt to call async2sync when not -multiclock like SymbiYosys" This reverts commit a39505e329cc05dbd4ad624a1cf0f6caf664fd9a. --- passes/equiv/equiv_opt.cc | 2 -- 1 file changed, 2 deletions(-) diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index 9fe3bbd57..d4c7f7953 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -156,8 +156,6 @@ struct EquivOptPass:public ScriptPass if (check_label("prove")) { if (multiclock || help_mode) run("clk2fflogic", "(only with -multiclock)"); - else - run("async2sync", "(only without -multiclock)"); run("equiv_make gold gate equiv"); if (help_mode) run("equiv_induct [-undef] equiv"); -- cgit v1.2.3 From 5d680590d6bccd929ed3909248dbb73fb3876e65 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:30:33 -0700 Subject: Use equiv_opt -async2sync for xilinx --- tests/xilinx/latches.ys | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/tests/xilinx/latches.ys b/tests/xilinx/latches.ys index ac1102896..bd1dffd21 100644 --- a/tests/xilinx/latches.ys +++ b/tests/xilinx/latches.ys @@ -2,9 +2,7 @@ read_verilog latches.v proc flatten -equiv_opt -assert -run :prove -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -async2sync -equiv_opt -assert -run prove: -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check design -load preopt synth_xilinx -- cgit v1.2.3 From 7a6dec1cef9c6a44dafe83d884abaf06dc77ab07 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:30:51 -0700 Subject: Add new -async2sync option --- passes/equiv/equiv_opt.cc | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index d4c7f7953..d13e46ce4 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -58,7 +58,7 @@ struct EquivOptPass:public ScriptPass } std::string command, techmap_opts; - bool assert, undef, multiclock; + bool assert, undef, multiclock, async2sync; void clear_flags() YS_OVERRIDE { @@ -67,6 +67,7 @@ struct EquivOptPass:public ScriptPass assert = false; undef = false; multiclock = false; + async2sync = false; } void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE @@ -100,6 +101,10 @@ struct EquivOptPass:public ScriptPass multiclock = true; continue; } + if (args[argidx] == "-async2sync") { + async2sync = true; + continue; + } break; } @@ -119,6 +124,9 @@ struct EquivOptPass:public ScriptPass if (!design->full_selection()) log_cmd_error("This command only operates on fully selected designs!\n"); + if (async2sync && multiclock) + log_cmd_error("The '-async2sync' and '-multiclock' options are mutually exclusive!\n"); + log_header(design, "Executing EQUIV_OPT pass.\n"); log_push(); @@ -156,6 +164,8 @@ struct EquivOptPass:public ScriptPass if (check_label("prove")) { if (multiclock || help_mode) run("clk2fflogic", "(only with -multiclock)"); + if (async2sync || help_mode) + run("async2sync", "(only with -async2sync)"); run("equiv_make gold gate equiv"); if (help_mode) run("equiv_induct [-undef] equiv"); -- cgit v1.2.3 From bd5889640bbcbb11c80360893fcf17d9399cef8a Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:45:53 -0700 Subject: Disable equiv check for ice40 latches --- tests/ice40/latches.ys | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys index f3562559e..708734e44 100644 --- a/tests/ice40/latches.ys +++ b/tests/ice40/latches.ys @@ -1,14 +1,11 @@ read_verilog latches.v -design -save read proc -async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock flatten -synth_ice40 -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +# Can't run any sort of equivalence check because latches are blown to LUTs +#equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check -design -load read +#design -load preopt synth_ice40 cd top select -assert-count 4 t:SB_LUT4 -- cgit v1.2.3 From a9efd2e81cd502665ee034f64c85b11e34dfd9bb Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:51:53 -0700 Subject: Restore part of doc --- passes/equiv/equiv_opt.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index d13e46ce4..ec1200488 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -32,7 +32,8 @@ struct EquivOptPass:public ScriptPass log("\n"); log(" equiv_opt [options] [command]\n"); log("\n"); - log("This command checks circuit equivalence before and after an optimization pass.\n"); + log("This command uses temporal induction to check circuit equivalence before and\n"); + log("after an optimization pass.\n"); log("\n"); log(" -run :\n"); log(" only run the commands between the labels (see below). an empty\n"); -- cgit v1.2.3 From 84f978bdc20494167a6a2c5f654b96c4f565a5e0 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 4 Oct 2019 10:17:46 -0700 Subject: Add -async2sync to help text as per @daveshah1 --- passes/equiv/equiv_opt.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index ec1200488..c7e6d71a6 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -50,6 +50,9 @@ struct EquivOptPass:public ScriptPass log(" -multiclock\n"); log(" run clk2fflogic before equivalence checking.\n"); log("\n"); + log(" -async2sync\n"); + log(" run async2sync before equivalence checking.\n"); + log("\n"); log(" -undef\n"); log(" enable modelling of undef states during equiv_induct.\n"); log("\n"); @@ -166,7 +169,7 @@ struct EquivOptPass:public ScriptPass if (multiclock || help_mode) run("clk2fflogic", "(only with -multiclock)"); if (async2sync || help_mode) - run("async2sync", "(only with -async2sync)"); + run("async2sync", " (only with -async2sync)"); run("equiv_make gold gate equiv"); if (help_mode) run("equiv_induct [-undef] equiv"); -- cgit v1.2.3