diff options
author | Eddie Hung <eddie@fpgeh.com> | 2019-10-02 18:07:38 -0700 |
---|---|---|
committer | Eddie Hung <eddie@fpgeh.com> | 2019-10-02 18:07:38 -0700 |
commit | c6a55d948aebc8993cc3e33372b9c403b0b90554 (patch) | |
tree | 9806b6ff139a604e8c89ea5b8972a755f15e0fb2 | |
parent | f6fabc8fda1eb00b0227f1a91d85b837a0609728 (diff) | |
parent | f46ac1df9f8847dac9d9851f2f948d93a1064ff1 (diff) | |
download | yosys-c6a55d948aebc8993cc3e33372b9c403b0b90554.tar.gz yosys-c6a55d948aebc8993cc3e33372b9c403b0b90554.tar.bz2 yosys-c6a55d948aebc8993cc3e33372b9c403b0b90554.zip |
Merge branch 'eddie/fix_sat_init' into eddie/fix1427
-rw-r--r-- | passes/sat/sat.cc | 5 | ||||
-rw-r--r-- | tests/sat/initval.ys | 20 |
2 files changed, 24 insertions, 1 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 430bba1e8..93a4f225e 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -265,15 +265,18 @@ struct SatHelper RTLIL::SigSpec rhs = it.second->attributes.at("\\init"); log_assert(lhs.size() == rhs.size()); + dict<RTLIL::SigBit,SigBit> seen_init; RTLIL::SigSpec removed_bits; for (int i = 0; i < lhs.size(); i++) { RTLIL::SigSpec bit = lhs.extract(i, 1); - if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit)) { + if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit) || seen_init.at(bit, rhs[i]) != rhs[i]) { removed_bits.append(bit); lhs.remove(i, 1); rhs.remove(i, 1); i--; } + else + seen_init[bit] = rhs[i]; } if (removed_bits.size()) diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..1627a37e3 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,3 +2,23 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts + +read_verilog <<EOT +module gold(input clk, input i, output reg [1:0] o); +initial o = 2'b10; +always @(posedge clk) + o[0] <= {i,i}; +endmodule + +module gate(input clk, input i, output reg [1:0] o); +initial o = 2'b10; +always @(posedge clk) + o[0] <= i; +always @* + o[1] <= o[0]; +endmodule +EOT + +proc +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 1 -falsify -prove-asserts -show-ports miter |