mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

Add equiv_opt -multiclock

Browse source 
Signed-off-by: David Shah <dave@ds0.me>
This commit is contained in:
David Shah 2019-09-11 13:55:16 +01:00
parent c7f1368cd2
commit c43e52d2d7
2 changed files with 23 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
passes/equiv/equiv_opt.cc
View file

@ -46,6 +46,9 @@ struct EquivOptPass:public ScriptPass
log(" -assert\n");
log(" produce an error if the circuits are not equivalent.\n");
log("\n");
log(" -multiclock\n");
log(" run clk2fflogic before equivalence checking.\n");
log("\n");
log(" -undef\n");
log(" enable modelling of undef states during equiv_induct.\n");
log("\n");
@ -55,7 +58,7 @@ struct EquivOptPass:public ScriptPass
}
std::string command, techmap_opts;
bool assert, undef;
bool assert, undef, multiclock;
void clear_flags() YS_OVERRIDE
{
@ -63,6 +66,7 @@ struct EquivOptPass:public ScriptPass
techmap_opts = "";
assert = false;
undef = false;
multiclock = false;
}
void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@ -92,6 +96,10 @@ struct EquivOptPass:public ScriptPass
undef = true;
continue;
}
if (args[argidx] == "-multiclock") {
multiclock = true;
continue;
}
break;
}
@ -146,6 +154,8 @@ struct EquivOptPass:public ScriptPass
}
if (check_label("prove")) {
if (multiclock || help_mode)
run("clk2fflogic", "(only with -multiclock)");
run("equiv_make gold gate equiv");
if (help_mode)
run("equiv_induct [-undef] equiv");

12
tests/various/equiv_opt_multiclock.ys Normal file
View file

@ -0,0 +1,12 @@
read_verilog <<EOT
module top(input clk, pre, d, output reg q);
always @(posedge clk, posedge pre)
if (pre)
q <= 1'b1;
else
q <= d;
endmodule
EOT
prep
equiv_opt -assert -multiclock -map +/simcells.v synth