Add tests for closed issues

regression/Makefile

@@ -469,6 +469,30 @@ $(eval $(call template,issue_01135,issue_01135))
 #issue_01144
 $(eval $(call template,issue_01144,issue_01144))
 
+#issue_01145
+$(eval $(call template,issue_01145,issue_01145))
+
+#issue_01220
+$(eval $(call template,issue_01220,issue_01220))
+
+#issue_01223
+$(eval $(call template,issue_01223,issue_01223))
+
+#issue_01231
+$(eval $(call template,issue_01231,issue_01231))
+
+#issue_01243
+$(eval $(call template,issue_01243,issue_01243))
+
+#issue_01273
+$(eval $(call template,issue_01273,issue_01273))
+
+#issue_01284
+$(eval $(call template,issue_01284,issue_01284))
+
+#issue_01329
+$(eval $(call template,issue_01329,issue_01329))
+
 
 
 

regression/issue_01145/top.sv

+
+
+module TopModule(
+    input logic clk,
+    input logic rst,
+    output logic [21:0] outOther,
+    input logic [1:0] sig,
+    input logic flip,
+    output logic [1:0] sig_out,
+    output logic [15:0] passThrough);
+
+  MyInterface #(.WIDTH(4)) MyInterfaceInstance();
+
+  SubModule1 u_SubModule1 (
+    .clk(clk),
+    .rst(rst),
+    .u_MyInterface(MyInterfaceInstance),
+    .outOther(outOther),
+    .sig (sig)
+  );
+
+  assign sig_out = MyInterfaceInstance.mysig_out;
+
+
+  assign MyInterfaceInstance.setting = flip;
+
+  assign passThrough = MyInterfaceInstance.passThrough;
+
+endmodule
+
+interface MyInterface #(
+  parameter WIDTH = 3)(
+  );
+
+  logic setting;
+  logic [WIDTH-1:0] other_setting;
+
+  logic [1:0] mysig_out;
+
+  logic [15:0] passThrough;
+
+    modport submodule1 (
+        input  setting,
+        output other_setting,
+        output mysig_out,
+        output passThrough
+    );
+
+    modport submodule2 (
+        input  setting,
+        output other_setting,
+        input  mysig_out,
+        output passThrough
+    );
+
+endinterface
+
+
+module SubModule1(
+    input logic clk,
+    input logic rst,
+    MyInterface.submodule1 u_MyInterface,
+    input logic [1:0] sig,
+    output logic [21:0] outOther
+
+  );
+
+  always_ff @(posedge clk or posedge rst)
+    if(rst)
+      u_MyInterface.mysig_out <= 0;
+    else begin
+      if(u_MyInterface.setting)
+        u_MyInterface.mysig_out <= sig;
+      else
+        u_MyInterface.mysig_out <= ~sig;
+    end
+
+  MyInterface #(.WIDTH(22)) MyInterfaceInstanceInSub();
+
+  SubModule2 u_SubModule2 (
+    .clk(clk),
+    .rst(rst),
+    .u_MyInterfaceInSub2(u_MyInterface),
+    .u_MyInterfaceInSub3(MyInterfaceInstanceInSub)
+  );
+
+    assign outOther = MyInterfaceInstanceInSub.other_setting;
+
+    assign MyInterfaceInstanceInSub.setting = 0;
+    assign MyInterfaceInstanceInSub.mysig_out = sig;
+
+endmodule
+
+module SubModule2(
+
+    input logic clk,
+    input logic rst,
+    MyInterface.submodule2 u_MyInterfaceInSub2,
+    MyInterface.submodule2 u_MyInterfaceInSub3
+
+  );
+
+   always_comb begin
+      if (u_MyInterfaceInSub3.mysig_out == 2'b00)
+        u_MyInterfaceInSub3.other_setting[21:0] = 1000;
+      else if (u_MyInterfaceInSub3.mysig_out == 2'b01)
+        u_MyInterfaceInSub3.other_setting[21:0] = 2000;
+      else if (u_MyInterfaceInSub3.mysig_out == 2'b10)
+        u_MyInterfaceInSub3.other_setting[21:0] = 3000;
+      else
+        u_MyInterfaceInSub3.other_setting[21:0] = 4000;
+   end
+
+    assign u_MyInterfaceInSub2.passThrough[7:0] = 124;
+    assign u_MyInterfaceInSub2.passThrough[15:8] = 200;
+
+endmodule

regression/issue_01220/top.v

+module submod(output q);
+wire aa = 1'b1;
+assign q = aa;
+endmodule
+
+module top(output q);
+wire \submod_i.aa ;
+submod submod_i(.q(\submod_i.aa ));
+assign q = \submod_i.aa ;
+endmodule

regression/issue_01223/top.v

+`default_nettype none
+
+module top
+        (
+         inout wire [7:0] data_io,
+         output reg [7:0] rdata_o,
+         input wire [7:0] wdata_i,
+         input wire       rxf_n_i,
+         input wire       txe_n_i,
+         output reg       rd_n_o,
+         output reg       wr_n_o,
+         output reg       siwua_n_o,
+         input wire       clk_i,
+         output reg       oe_n_o,
+         input wire       suspend_n_i
+         );
+
+        initial begin
+                rdata_o = {8{1'b0}};
+                rd_n_o = 1;
+                wr_n_o = 1;
+                siwua_n_o = 1; /* Never flush TX data. */
+        end
+
+        assign data_io = (!txe_n_i && !wr_n_o) ? wdata_i : {8{1'bz}};
+
+        always @(posedge clk_i, negedge suspend_n_i) begin
+                if (!suspend_n_i) begin
+                        wr_n_o <= 1;
+                        rd_n_o <= 1;
+                        oe_n_o <= 1;
+                        rdata_o <= {8{1'b0}};
+                end
+                else begin
+                        // Give TX bus precedence.
+                        if (!txe_n_i) begin
+                                wr_n_o <= 0;
+                                rd_n_o <= 1;
+                                oe_n_o <= 1;
+                                rdata_o <= {8{1'b0}};
+                        end
+                        // oe_n_o must be driven low at least one period before we can read.
+                        else if (!rxf_n_i && oe_n_o) begin
+                                wr_n_o <= 1;
+                                rd_n_o <= 1;
+                                oe_n_o <= 0;
+                                rdata_o <= {8{1'b0}};
+                        end
+                        else if (!rxf_n_i && !oe_n_o) begin
+                                wr_n_o <= 1;
+                                rd_n_o <= 0;
+                                oe_n_o <= 0;
+                                rdata_o <= data_io;
+                        end
+                        else begin
+                                wr_n_o <= 1;
+                                rd_n_o <= 1;
+                                oe_n_o <= 1;
+                                rdata_o <= {8{1'b0}};
+                        end
+                end // else: !if(!suspend_n_i)
+        end
+
+endmodule // usb

regression/issue_01231/top.v

+module	fnmcve(o_crc);
+	output	reg	[7:0]	o_crc;
+
+	always @(*)
+		o_crc = gencrc({ 2'b01, 6'h11, 32'h00 });
+
+	function [7:0]	gencrc;
+		input	[39:0]	i_cmdword;
+		integer	icrc;
+
+		gencrc = 0;
+		for(icrc=0; icrc<40; icrc=icrc+1)
+		if (i_cmdword[39-icrc] ^ gencrc[7])
+			gencrc[7:1] = { gencrc[6:1], 1'b0 } ^ 7'h09;
+		else
+			gencrc[7:1] = { gencrc[6:1], 1'b0 };
+		gencrc = { gencrc[7:1], 1'b1 };
+	endfunction
+endmodule

regression/issue_01243/top.v

+module top  (y, clk, sel);
+   output wire y  ;
+   input       clk;
+   input       sel;
+   reg         reg_assign = (1'h0) ;
+   reg [1:0]   reg_count = (1'h0) ;
+   assign y = reg_assign ;
+   always @(posedge clk)
+     if (sel)
+       for (reg_count = 0; reg_count < 2; reg_count = reg_count + 1'h1)
+         if (0);
+         else reg_assign <= 1;
+     else reg_assign <=  0;
+endmodule

regression/issue_01273/top.v

+module top (
+    input [5:0] S,
+    input [63:0] D,
+    output M256
+);
+    assign M256 = D[S];
+endmodule

regression/issue_01284/testbench.v

+module testbench;
+    reg [2:0] in;
+
+	wire patt_out,out;
+	wire patt_carry_out,carryout;
+
+    initial begin
+        // $dumpfile("testbench.vcd");
+        // $dumpvars(0, testbench);
+
+        #5 in = 0;
+        repeat (10000) begin
+            #5 in = in + 1;
+        end
+
+        $display("OKAY");
+    end
+
+    top uut (
+	.x(in[0]),
+	.y(in[1]),
+	.cin(in[2]),
+	.A(out),
+	.cout(carryout)
+	);
+	
+	assign {patt_carry_out,patt_out} =  in[2] + in[1] + in[0];
+
+	assert_comb out_test(.A(patt_out), .B(out));
+	assert_comb carry_test(.A(patt_carry_out), .B(carryout));
+
+endmodule

regression/issue_01284/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+`ifndef BUG
+assign {cout,A} =  cin + y + x;
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule

regression/issue_01329/dff.v

+// Design
+// D flip-flop
+// https://www.edaplayground.com/x/5dzJ
+
+// If (asynchronous 'reset_sync' & enable') are true on the same clock, 
+// and then 'reset_sync' is low on the next clock,
+// then the asynchronous 'reset_sync' gets ignored and the 'enable' applied
+
+module dff (clk, reset, enable, d, q);
+	  
+	input      clk;
+	input      reset;
+	input 	 enable;
+	input      d;
+	output reg q;
+
+
+  	always @(posedge clk or posedge reset_sync)
+  	begin
+    	if (reset_sync) begin
+      		// Asynchronous reset when reset goes high
+	      	q <= 1'b0;      
+	    end 
+
+		else if(enable) 
+		begin
+      		// Assign D to Q on positive clock edge
+      		q <= d;
+    	end
+  	end
+
+	wire reset_sync;
+
+    synchronizer #(.RESET_STATE(1)) reset_synchronizer(
+        .clk(clk),
+        .reset(reset),
+        .data_i(0),
+        .data_o(reset_sync));
+
+
+`ifdef FORMAL
+
+	always @($global_clock) assume(clk != $past(clk));
+
+	localparam MAX_CNT = 16;
+
+	reg[$clog2(MAX_CNT)-1:0] counter;
+	initial counter = 0;
+
+	always @(posedge clk) counter <= counter + 1;
+
+	initial assume(reset);
+	initial assume(enable);
+
+	always @(posedge clk) if(counter == (MAX_CNT >> 1)) assume(reset != $past(reset));
+
+
+	//always @(*) assume(d == 1'b1);
+
+	always @(clk) 
+	begin
+		if(clk) assume(d == 1'b0); 
+		
+		else assume(d == 1'b1);
+	end
+
+	always @(clk) 
+	begin
+		if(clk) assume(!enable); 
+		
+		else assume(enable);
+	end
+
+	always @(posedge clk) 
+	begin
+		if(reset_sync) assert(q == 0);
+
+		else if(enable) assert(q == d);
+
+		else assert(q == $past(q));
+	end
+
+	always @(posedge clk) cover(reset && enable && d && !clk);
+
+`endif
+
+endmodule

regression/issue_01329/synchronizer.sv

+// https://github.com/jbush001/NyuziProcessor/blob/master/hardware/core/synchronizer.sv
+//
+// Copyright 2011-2015 Jeff Bush
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+
+//
+// Transfer a signal into a clock domain, avoiding metastability and
+// race conditions due to propagation delay.
+//
+
+module synchronizer
+    #(parameter WIDTH = 1,
+    parameter RESET_STATE = 0)
+
+    (input                      clk,
+    input                       reset,
+    output logic[WIDTH - 1:0]   data_o,
+    input [WIDTH - 1:0]         data_i);
+
+    logic[WIDTH - 1:0] sync0;
+    logic[WIDTH - 1:0] sync1;
+
+    always_ff @(posedge clk, posedge reset)
+    begin
+        if (reset)
+        begin
+            sync0 <= {WIDTH{RESET_STATE}};
+            sync1 <= {WIDTH{RESET_STATE}};
+            data_o <= {WIDTH{RESET_STATE}};
+        end
+        else
+        begin
+            sync0 <= data_i;
+            sync1 <= sync0;
+            data_o <= sync1;
+        end
+    end
+endmodule
\ No newline at end of file

regression/run.sh

@@ -121,7 +121,14 @@ elif [ "$1" = "issue_00502" ] ||\
 	 [ "$1" = "issue_01118" ] ||\
 	 [ "$1" = "issue_01128" ] ||\
 	 [ "$1" = "issue_01132" ] ||\
-	 [ "$1" = "issue_01135" ]; then
+	 [ "$1" = "issue_01135" ] ||\
+	 [ "$1" = "issue_01145" ] ||\
+	 [ "$1" = "issue_01220" ] ||\
+	 [ "$1" = "issue_01223" ] ||\
+	 [ "$1" = "issue_01231" ] ||\
+	 [ "$1" = "issue_01243" ] ||\
+	 [ "$1" = "issue_01273" ] ||\
+	 [ "$1" = "issue_01329" ]; then
 
 	expected_string=""
 	expected="1"
@@ -246,6 +253,19 @@ elif [ "$1" = "issue_00502" ] ||\
 		expected_string="\$_MUX4_                         1"
 	elif [ "$1" = "issue_01135" ]; then
 		expected_string="\$pmux                           1"
+	elif [ "$1" = "issue_01145" ] ||\
+		 [ "$1" = "issue_01220" ]; then
+		expected_string="Executing FLATTEN pass (flatten design)."
+	elif [ "$1" = "issue_01223" ]; then
+		expected_string=" Executing CHECK pass (checking for obvious problems)."
+	elif [ "$1" = "issue_01231" ]; then
+		expected_string="Successfully finished Verilog frontend."
+	elif [ "$1" = "issue_01243" ]; then
+		expected_string="assign y = reg_assign;"
+	elif [ "$1" = "issue_01273" ]; then
+		expected_string="\$_MUX8_                         9"
+	elif [ "$1" = "issue_01329" ]; then
+		expected_string="\$mux                            1"
 	fi
 
 	if [ "$1" = "issue_01118" ]; then

regression/scripts/issue_01145.ys

+read_verilog -sv ../top.sv
+hierarchy -check -top TopModule
+proc
+tee -o result.log flatten

regression/scripts/issue_01220.ys

+read_verilog ../top.v
+hierarchy -top top
+proc
+tee -o result.log flatten

regression/scripts/issue_01223.ys

+read_verilog ../top.v
+tee -o result.log synth_xilinx

regression/scripts/issue_01231.ys

+tee -o result.log read -formal ../top.v

regression/scripts/issue_01241.ys

+read_verilog ../top.v
+synth
+write_verilog -noattr result.log

regression/scripts/issue_01243.ys

+read_verilog ../top.v
+synth
+write_verilog -noattr result.log

regression/scripts/issue_01273.ys

+read_verilog ../top.v
+synth -top top
+muxcover -mux8
+tee -o result.log stat

regression/scripts/issue_01284.ys

+read_verilog ../top.v
+proc
+synth -top top
+extract_fa -ha -v
+tee -o result.log dump
+synth -top top
+write_verilog synth.v

regression/scripts/issue_01329.ys

+# read design
+read_verilog ../dff.v
+read_verilog -sv ../synchronizer.sv
+hierarchy -check
+
+# high-level synthesis
+proc; opt; fsm; opt; memory; opt
+flatten
+cd dff # Constrain all select calls below inside the top module
+select -assert-count 4 t:$adff
+select -assert-count 1 t:$mux
+select -assert-none t:$adff t:$mux %% t:* %D
+
+tee -o result.log stat