From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 28 Aug 2019 19:30:35 +0000 (-0700)
Subject: Use equiv for memory and dpram
X-Git-Tag: working-ls180~1084^2~11^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87d5d9b8c80df696c836831df9d9eff6f20476fa;p=yosys.git

Use equiv for memory and dpram
---

diff --git a/tests/ice40/dpram.ys b/tests/ice40/dpram.ys
index 77364e5ae..4f6a253ea 100644
--- a/tests/ice40/dpram.ys
+++ b/tests/ice40/dpram.ys
@@ -6,13 +6,10 @@ equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
 memory
 opt -full
 
-# TODO
-#equiv_opt -run prove: -assert null
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
 
 design -load postopt
 cd top
 select -assert-count 1 t:SB_RAM40_4K
 select -assert-none t:SB_RAM40_4K %% t:* %D
-write_verilog dpram_synth.v
diff --git a/tests/ice40/dpram_tb.v b/tests/ice40/dpram_tb.v
deleted file mode 100644
index dede64614..000000000
--- a/tests/ice40/dpram_tb.v
+++ /dev/null
@@ -1,81 +0,0 @@
-module testbench;
-    reg clk;
-
-    initial begin
-       //  $dumpfile("testbench.vcd");
-       //  $dumpvars(0, testbench);
-
-        #5 clk = 0;
-        repeat (10000) begin
-            #5 clk = 1;
-            #5 clk = 0;
-        end
-    end
-
-
-    reg [7:0] data_a = 0;
-	reg [7:0] addr_a = 0;
-	reg [7:0] addr_b = 0;
-    reg we_a = 0;
-    reg re_a = 1;
-	wire [7:0] q_a;
-	reg mem_init = 0;
-
-	reg [7:0] pq_a;
-
-    always @(posedge clk) begin
-    #3;
-    data_a <= data_a + 17;
-
-    addr_a <= addr_a + 1;
-    addr_b <= addr_b + 1;
-    end
-
-    always @(posedge addr_a) begin
-    #10;
-        if(addr_a > 6'h3E)
-            mem_init <= 1;
-    end
-
-	always @(posedge clk) begin
-    //#3;
-    we_a <= !we_a;
-    end
-
-    reg [7:0] mem [(1<<8)-1:0];
-
-    always @(posedge clk) // Write memory.
-	begin
-	if (we_a)
-	mem[addr_a] <= data_a; // Using write address bus.
-	end
-	always @(posedge clk) // Read memory.
-	begin
-	pq_a <= mem[addr_b]; // Using read address bus.
-	end
-
-	top uut (
-		.din(data_a),
-		.write_en(we_a),
-		.waddr(addr_a),
-		.wclk(clk),
-		.raddr(addr_b),
-		.rclk(clk),
-		.dout(q_a)
-		);
-
-	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a));
-
-endmodule
-
-module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B);
-    always @(posedge clk)
-    begin
-        #1;
-        if (en == 1 & init == 1 & A !== B)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
-            $stop;
-        end
-    end
-endmodule
diff --git a/tests/ice40/memory.ys b/tests/ice40/memory.ys
index 9b7490cd8..a66afbae6 100644
--- a/tests/ice40/memory.ys
+++ b/tests/ice40/memory.ys
@@ -6,13 +6,10 @@ equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
 memory
 opt -full
 
-# TODO
-#equiv_opt -run prove: -assert null
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
+sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
 
 design -load postopt
 cd top
 select -assert-count 1 t:SB_RAM40_4K
 select -assert-none t:SB_RAM40_4K %% t:* %D
-write_verilog memory_synth.v
diff --git a/tests/ice40/memory_tb.v b/tests/ice40/memory_tb.v
deleted file mode 100644
index be69374eb..000000000
--- a/tests/ice40/memory_tb.v
+++ /dev/null
@@ -1,79 +0,0 @@
-module testbench;
-    reg clk;
-
-    initial begin
-       //  $dumpfile("testbench.vcd");
-       //  $dumpvars(0, testbench);
-
-        #5 clk = 0;
-        repeat (10000) begin
-            #5 clk = 1;
-            #5 clk = 0;
-        end
-    end
-
-
-    reg [7:0] data_a = 0;
-	reg [5:0] addr_a = 0;
-    reg we_a = 0;
-    reg re_a = 1;
-	wire [7:0] q_a;
-	reg mem_init = 0;
-
-	reg [7:0] pq_a;
-
-    top uut (
-    .data_a(data_a),
-	.addr_a(addr_a),
-	.we_a(we_a),
-	.clk(clk),
-	.q_a(q_a)
-    );
-
-    always @(posedge clk) begin
-    #3;
-    data_a <= data_a + 17;
-
-    addr_a <= addr_a + 1;
-    end
-
-    always @(posedge addr_a) begin
-    #10;
-        if(addr_a > 6'h3E)
-            mem_init <= 1;
-    end
-
-	always @(posedge clk) begin
-    //#3;
-    we_a <= !we_a;
-    end
-
-    // Declare the RAM variable for check
-	reg [7:0] ram[63:0];
-
-	// Port A for check
-	always @ (posedge clk)
-	begin
-		if (we_a)
-		begin
-			ram[addr_a] <= data_a;
-			pq_a <= data_a;
-		end
-		pq_a <= ram[addr_a];
-	end
-
-	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a));
-
-endmodule
-
-module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B);
-    always @(posedge clk)
-    begin
-        #1;
-        if (en == 1 & init == 1 & A !== B)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
-            $stop;
-        end
-    end
-endmodule