3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 00:55:32 +00:00

Merge remote-tracking branch 'origin/master' into xaig_dff

This commit is contained in:
Eddie Hung 2019-12-20 13:56:13 -08:00
commit 1ea1e8e54f
11 changed files with 339 additions and 216 deletions

View file

@ -7,11 +7,9 @@ module MyMem #(
input Clk_i,
input [AddrWidth-1:0] Addr_i,
input [DataWidth-1:0] Data_i,
output [DataWidth-1:0] Data_o,
output reg [DataWidth-1:0] Data_o,
input WR_i);
reg [DataWidth-1:0] Data_o;
localparam Size = 2**AddrWidth;
(* mem2reg *)

34
tests/various/bug1531.ys Normal file
View file

@ -0,0 +1,34 @@
read_verilog <<EOT
module top (y, clk, w);
output reg y = 1'b0;
input clk, w;
reg [1:0] i = 2'b00;
always @(posedge clk)
// If the constant below is set to 2'b00, the correct output is generated.
// vvvv
for (i = 1'b0; i < 2'b01; i = i + 2'b01)
y <= w || i[1:1];
endmodule
EOT
synth
design -stash gate
read_verilog <<EOT
module gold (y, clk, w);
input clk;
wire [1:0] i;
input w;
output y;
reg y = 1'h0;
always @(posedge clk)
y <= w;
assign i = 2'h0;
endmodule
EOT
proc gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 10 -verify -prove-asserts -show-ports miter