Use equiv_opt for latches

This commit is contained in:
Eddie Hung 2019-08-28 12:21:15 -07:00
parent 32eef26ee2
commit ebd0a1875b
2 changed files with 10 additions and 58 deletions

View File

@ -1,6 +1,15 @@
read_verilog latches.v 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 synth_ice40
cd top cd top
select -assert-count 4 t:SB_LUT4 select -assert-count 4 t:SB_LUT4
select -assert-none t:SB_LUT4 %% t:* %D select -assert-none t:SB_LUT4 %% t:* %D
write_verilog latches_synth.v

View File

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