mirror of
https://github.com/YosysHQ/yosys
synced 2025-08-26 13:06:12 +00:00
Merge pull request #3 from YosysHQ/Sergey/tests_ice40
Merge my changes to tests_ice40 branch
This commit is contained in:
commit
d360693040
74 changed files with 3640 additions and 824 deletions
|
@ -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
|
||||
|
|
|
@ -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
|
|
@ -1,6 +1,15 @@
|
|||
read_verilog latches.v
|
||||
design -save read
|
||||
|
||||
proc
|
||||
async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock
|
||||
flatten
|
||||
synth_ice40
|
||||
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
|
||||
design -load read
|
||||
synth_ice40
|
||||
cd top
|
||||
select -assert-count 4 t:SB_LUT4
|
||||
select -assert-none t:SB_LUT4 %% t:* %D
|
||||
write_verilog latches_synth.v
|
||||
|
|
|
@ -1,57 +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 [2:0] dinA = 0;
|
||||
wire doutB,doutB1,doutB2;
|
||||
reg lat,latn,latsr = 0;
|
||||
|
||||
top uut (
|
||||
.clk (clk ),
|
||||
.a (dinA[0] ),
|
||||
.pre (dinA[1] ),
|
||||
.clr (dinA[2] ),
|
||||
.b (doutB ),
|
||||
.b1 (doutB1 ),
|
||||
.b2 (doutB2 )
|
||||
);
|
||||
|
||||
always @(posedge clk) begin
|
||||
#3;
|
||||
dinA <= dinA + 1;
|
||||
end
|
||||
|
||||
always @*
|
||||
if ( clk )
|
||||
lat <= dinA[0];
|
||||
|
||||
|
||||
always @*
|
||||
if ( !clk )
|
||||
latn <= dinA[0];
|
||||
|
||||
|
||||
always @*
|
||||
if ( dinA[2] )
|
||||
latsr <= 1'b0;
|
||||
else if ( dinA[1] )
|
||||
latsr <= 1'b1;
|
||||
else if ( clk )
|
||||
latsr <= dinA[0];
|
||||
|
||||
assert_dff lat_test(.clk(clk), .test(doutB), .pat(lat));
|
||||
assert_dff latn_test(.clk(clk), .test(doutB1), .pat(latn));
|
||||
assert_dff latsr_test(.clk(clk), .test(doutB2), .pat(latsr));
|
||||
|
||||
endmodule
|
|
@ -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
|
||||
|
|
|
@ -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
|
|
@ -21,13 +21,13 @@ for x in *.ys; do
|
|||
fi
|
||||
done
|
||||
|
||||
for s in *.sh; do
|
||||
if [ "$s" != "run-test.sh" ]; then
|
||||
echo "all:: run-$s"
|
||||
echo "run-$s:"
|
||||
echo " @echo 'Running $s..'"
|
||||
echo " @bash $s"
|
||||
fi
|
||||
done
|
||||
#for s in *.sh; do
|
||||
# if [ "$s" != "run-test.sh" ]; then
|
||||
# echo "all:: run-$s"
|
||||
# echo "run-$s:"
|
||||
# echo " @echo 'Running $s..'"
|
||||
# echo " @bash $s"
|
||||
# fi
|
||||
#done
|
||||
} > run-test.mk
|
||||
exec ${MAKE:-make} -f run-test.mk
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue