diff options
| author | Claire Wolf <clifford@clifford.at> | 2020-01-28 17:40:28 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-28 17:40:28 +0100 |
| commit | 4ddaa70fd6363096bf0cb1bc5e7cb8fa8ed21ad2 (patch) | |
| tree | 1ee2ffb6abec353f6a04a878c4ef60449576669e | |
| parent | 086c133ea58179b1b1a14bff972355c68f926e8d (diff) | |
| parent | 4a805108776f563bcd7550d1331a73a50512fbe2 (diff) | |
| download | yosys-4ddaa70fd6363096bf0cb1bc5e7cb8fa8ed21ad2.tar.gz yosys-4ddaa70fd6363096bf0cb1bc5e7cb8fa8ed21ad2.tar.bz2 yosys-4ddaa70fd6363096bf0cb1bc5e7cb8fa8ed21ad2.zip | |
Merge pull request #1567 from YosysHQ/eddie/sat_init_warning
sat: suppress 'Warning: ignoring initial value on non-register: ...' when init[i] = 1'bx
| -rw-r--r-- | passes/sat/sat.cc | 3 | ||||
| -rw-r--r-- | tests/sat/initval.ys | 11 |
2 files changed, 13 insertions, 1 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 430bba1e8..436ac1b01 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -269,7 +269,8 @@ struct SatHelper 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)) { - removed_bits.append(bit); + if (rhs[i] != State::Sx) + removed_bits.append(bit); lhs.remove(i, 1); rhs.remove(i, 1); i--; diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..1436724b0 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,3 +2,14 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts + +design -reset +read_verilog -icells <<EOT +module top(input clk, i, output [1:0] o); +(* init = 2'bx0 *) +wire [1:0] o; +assign o[1] = o[0]; +$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0])); +endmodule +EOT +sat -seq 1 |