riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #1567 from YosysHQ/eddie/sat_init_warning 

sat: suppress 'Warning: ignoring initial value on non-register: ...' when init[i] = 1'bx
This commit is contained in:
Claire Wolf 2020-01-28 17:40:28 +01:00 committed by GitHub
parent 086c133ea5 4a80510877
commit 4ddaa70fd6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
passes/sat/sat.cc
View File

@ -269,6 +269,7 @@ struct SatHelper
for (int i = 0; i < lhs.size(); i++) { for (int i = 0; i < lhs.size(); i++) {
RTLIL::SigSpec bit = lhs.extract(i, 1); 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)) {
if (rhs[i] != State::Sx)
removed_bits.append(bit); removed_bits.append(bit);
lhs.remove(i, 1); lhs.remove(i, 1);
rhs.remove(i, 1); rhs.remove(i, 1);

11
tests/sat/initval.ys
View File

@ -2,3 +2,14 @@ read_verilog -sv initval.v
proc;; proc;;
sat -seq 10 -prove-asserts 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