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

Use equiv for memory and dpram

This commit is contained in:
Eddie Hung 2019-08-28 12:30:35 -07:00
parent ebd0a1875b
commit 87d5d9b8c8
4 changed files with 2 additions and 168 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
tests/ice40/dpram.ys
View File

@ -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

81
tests/ice40/dpram_tb.v
View File

@ -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

5
tests/ice40/memory.ys
View File

@ -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

79
tests/ice40/memory_tb.v
View File

@ -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