diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index b39d7a785..1995be3cd 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -79,10 +79,12 @@ struct EquivInductWorker } if (set_assumes) { - RTLIL::SigSpec assumes_a, assumes_en; - satgen.getAssumes(assumes_a, assumes_en, step); - for (int i = 0; i < GetSize(assumes_a); i++) - log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); + if (step == 1) { + RTLIL::SigSpec assumes_a, assumes_en; + satgen.getAssumes(assumes_a, assumes_en, step); + for (int i = 0; i < GetSize(assumes_a); i++) + log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); + } ez->assume(satgen.importAssumes(step)); } diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index bdb39172b..1bebf5454 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -243,10 +243,12 @@ struct EquivSimpleWorker } if (set_assumes) { - RTLIL::SigSpec assumes_a, assumes_en; - satgen.getAssumes(assumes_a, assumes_en, step+1); - for (int i = 0; i < GetSize(assumes_a); i++) - log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); + if (verbose && step == max_seq) { + RTLIL::SigSpec assumes_a, assumes_en; + satgen.getAssumes(assumes_a, assumes_en, step+1); + for (int i = 0; i < GetSize(assumes_a); i++) + log(" Import constraint from assume cell: %s when %s (%d).\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]), step); + } ez->assume(satgen.importAssumes(step+1)); }