From 51ffb093b5beeb5e2c687d2bf34b13d246f3fc7d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 22 Aug 2019 16:42:19 -0700 Subject: [PATCH 1/5] In sat: 'x' in init attr should not override constant --- passes/sat/sat.cc | 2 ++ tests/sat/initval.v | 4 ++++ tests/sat/initval.ys | 2 +- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index dd56d8c71..bcc690fa3 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -268,6 +268,8 @@ struct SatHelper RTLIL::SigSpec removed_bits; for (int i = 0; i < lhs.size(); i++) { RTLIL::SigSpec bit = lhs.extract(i, 1); + if (bit.is_fully_const() && rhs[i] == State::Sx) + rhs[i] = bit; if (!satgen.initial_state.check_all(bit)) { removed_bits.append(bit); lhs.remove(i, 1); diff --git a/tests/sat/initval.v b/tests/sat/initval.v index 5b661f8d6..d46ccae48 100644 --- a/tests/sat/initval.v +++ b/tests/sat/initval.v @@ -1,6 +1,7 @@ module test(input clk, input [3:0] bar, output [3:0] foo); reg [3:0] foo = 0; reg [3:0] last_bar = 0; + reg [3:0] asdf = 4'b1xxx; always @* foo[1:0] <= bar[1:0]; @@ -11,5 +12,8 @@ module test(input clk, input [3:0] bar, output [3:0] foo); always @(posedge clk) last_bar <= bar; + always @* + asdf[2:0] <= 3'b111; + assert property (foo == {last_bar[3:2], bar[1:0]}); endmodule diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..3d88aa971 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -1,4 +1,4 @@ read_verilog -sv initval.v -proc;; +proc; sat -seq 10 -prove-asserts From 10c41a5cf51427d96f465113decb752e501e926e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 23 Aug 2019 09:11:04 -0700 Subject: [PATCH 2/5] Blocking assignment --- tests/sat/initval.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/sat/initval.v b/tests/sat/initval.v index d46ccae48..fcec9dd8c 100644 --- a/tests/sat/initval.v +++ b/tests/sat/initval.v @@ -13,7 +13,7 @@ module test(input clk, input [3:0] bar, output [3:0] foo); last_bar <= bar; always @* - asdf[2:0] <= 3'b111; + asdf[2:0] = 3'b111; assert property (foo == {last_bar[3:2], bar[1:0]}); endmodule From dc87372a97d515563ccccd517ef8f35662870fe6 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sat, 24 Aug 2019 15:05:44 -0700 Subject: [PATCH 3/5] Wire with init on FF part, 1'bx on non-FF part --- tests/sat/initval.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/sat/initval.v b/tests/sat/initval.v index fcec9dd8c..81f71b5ba 100644 --- a/tests/sat/initval.v +++ b/tests/sat/initval.v @@ -1,4 +1,4 @@ -module test(input clk, input [3:0] bar, output [3:0] foo); +module test(input clk, input [3:0] bar, output [3:0] foo, asdf); reg [3:0] foo = 0; reg [3:0] last_bar = 0; reg [3:0] asdf = 4'b1xxx; @@ -12,6 +12,8 @@ module test(input clk, input [3:0] bar, output [3:0] foo); always @(posedge clk) last_bar <= bar; + always @(posedge clk) + asdf[3] <= bar[3]; always @* asdf[2:0] = 3'b111; From 00387f39277ab817b3b17e72b59793e6d5dfcde8 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 27 Aug 2019 09:24:32 -0700 Subject: [PATCH 4/5] Revert to using clean --- tests/sat/initval.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 3d88aa971..2079d2f34 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -1,4 +1,4 @@ read_verilog -sv initval.v -proc; +proc;; sat -seq 10 -prove-asserts From 28133432bea4a3fa01cd2f5e82a52a853cfccb84 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 27 Aug 2019 09:24:59 -0700 Subject: [PATCH 5/5] Ignore all 1'bx in (* init *) --- passes/sat/sat.cc | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index bcc690fa3..430bba1e8 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -268,9 +268,7 @@ struct SatHelper RTLIL::SigSpec removed_bits; for (int i = 0; i < lhs.size(); i++) { RTLIL::SigSpec bit = lhs.extract(i, 1); - if (bit.is_fully_const() && rhs[i] == State::Sx) - rhs[i] = bit; - if (!satgen.initial_state.check_all(bit)) { + if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit)) { removed_bits.append(bit); lhs.remove(i, 1); rhs.remove(i, 1);