mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 00:55:32 +00:00
Merge pull request #1926 from YosysHQ/eddie/abc9_auto_dff
abc9: support seq synthesis when module has (* abc9_flop *) and bypass non-combinatorial (* abc9_box *)
This commit is contained in:
Eddie Hung
GitHub
commit
2d573a0ff6
34 changed files with 1663 additions and 1860 deletions
|
|
@ -1,32 +1,85 @@
|
|||
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
|
||||
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
|
||||
FDSE fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
|
||||
FDCE fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
|
||||
FDPE fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
|
||||
FDRE_1 fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
|
||||
FDSE_1 fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
|
||||
FDCE_1 fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
|
||||
FDPE_1 fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
|
||||
FDRE /*#(.INIT(0))*/ fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
|
||||
FDSE #(.INIT(0)) fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
|
||||
FDCE #(.INIT(0)) fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
|
||||
FDPE #(.INIT(0)) fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
|
||||
FDRE_1 #(.INIT(0)) fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
|
||||
FDSE_1 #(.INIT(0)) fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
|
||||
FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
|
||||
FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-none t:FD*
|
||||
select -assert-count 6 t:FD*
|
||||
select -assert-count 6 c:fd2 c:fd3 c:fd4 c:fd6 c:fd7 c:fd8
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
FDRE #(.INIT(0)) fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE #(.INIT(0)) fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE #(.INIT(0)) fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE #(.INIT(0)) fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 /*#(.INIT(0))*/ fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 #(.INIT(0)) fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-none t:FD*
|
||||
select -assert-count 4 t:FD*
|
||||
select -assert-count 4 c:fd3 c:fd4 c:fd7 c:fd8
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE #(.INIT(1)) fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE /*#(.INIT(1))*/ fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE #(.INIT(1)) fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE #(.INIT(1)) fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 #(.INIT(1)) fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 #(.INIT(1)) fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 /*#(.INIT(1))*/ fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 #(.INIT(1)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
logger -expect warning "Module '\$paramod\\FDRE\\INIT=1' contains a \$dff cell .*" 1
|
||||
logger -expect warning "Module '\$paramod\\FDRE_1\\INIT=1' contains a \$dff cell .*" 1
|
||||
logger -expect warning "Module 'FDSE' contains a \$dff cell .*" 1
|
||||
logger -expect warning "Module '\$paramod\\FDSE_1\\INIT=1' contains a \$dff cell .*" 1
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-count 8 t:FD*
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input clk, clr, pre, output reg q0 = 1'b0, output reg q1 = 1'b1);
|
||||
always @(posedge clk or posedge clr)
|
||||
if (clr)
|
||||
q0 <= 1'b0;
|
||||
else
|
||||
q0 <= ~q0;
|
||||
always @(posedge clk or posedge pre)
|
||||
if (pre)
|
||||
q1 <= 1'b1;
|
||||
else
|
||||
q1 <= ~q1;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:FDPE
|
||||
select -assert-count 2 t:INV
|
||||
select -assert-count 0 t:FD* t:INV %% t:* %D
|
||||
|
||||
logger -expect-no-warnings
|
||||
|
|
|
|||
|
|
@ -1,91 +0,0 @@
|
|||
read_verilog <<EOT
|
||||
module top(input C, CE, D, R, output [1:0] Q);
|
||||
FDRE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0]));
|
||||
FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:FDSE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, S, output [1:0] Q);
|
||||
FDSE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0]));
|
||||
FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:FDRE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, PRE, output [1:0] Q);
|
||||
FDPE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0]));
|
||||
FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:FDCE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
clk2fflogic
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, CLR, output [1:0] Q);
|
||||
FDCE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0]));
|
||||
FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDPE
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
clk2fflogic
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
3
tests/simple_abc9/abc9.box
Normal file
3
tests/simple_abc9/abc9.box
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
MUXF8 1 0 3 1
|
||||
#I0 I1 S
|
||||
0 0 0 # O
|
||||
|
|
@ -213,7 +213,7 @@ module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encode
|
|||
input rst;
|
||||
endmodule
|
||||
|
||||
(* abc9_box, blackbox *)
|
||||
(* abc9_box_id=1, blackbox *)
|
||||
module MUXF8(input I0, I1, S, output O);
|
||||
specify
|
||||
(I0 => O) = 0;
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p
|
|||
synth -run coarse; \
|
||||
opt -full; \
|
||||
techmap; \
|
||||
abc9 -lut 4; \
|
||||
abc9 -lut 4 -box ../abc9.box; \
|
||||
clean; \
|
||||
check -assert; \
|
||||
select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%; \
|
||||
|
|
|
|||
|
|
@ -45,14 +45,16 @@ sat -seq 10 -verify -prove-asserts -show-ports miter
|
|||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module abc9_test036(input clk, d, output q);
|
||||
(* keep *) reg w;
|
||||
$__ABC9_FF_ ff(.D(d), .Q(w));
|
||||
wire \ff.clock = clk;
|
||||
wire \ff.init = 1'b0;
|
||||
(* keep, init=1'b0 *) wire w;
|
||||
$_DFF_P_ ff(.C(clk), .D(d), .Q(w));
|
||||
assign q = w;
|
||||
endmodule
|
||||
EOT
|
||||
abc9 -lut 4 -dff
|
||||
equiv_opt -assert abc9 -lut 4 -dff
|
||||
design -load postopt
|
||||
cd abc9_test036
|
||||
select -assert-count 1 t:$_DFF_P_
|
||||
select -assert-none t:* t:$_DFF_P_ %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -67,8 +69,32 @@ specify
|
|||
endspecify
|
||||
endmodule
|
||||
|
||||
module top(input [1:0] i, output o);
|
||||
module abc9_test037(input [1:0] i, output o);
|
||||
LUT2 #(.mask(4'b0)) lut (.i(i), .o(o));
|
||||
endmodule
|
||||
EOT
|
||||
abc9
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module abc9_test038(input clk, output w, x, y, z);
|
||||
(* init=1'b1 *) wire w;
|
||||
$_DFF_N_ ff1(.C(clk), .D(1'b1), .Q(w));
|
||||
(* init=1'bx *) wire x;
|
||||
$_DFF_N_ ff2(.C(clk), .D(1'b0), .Q(x));
|
||||
(* init=1'b0 *) wire y;
|
||||
$_DFF_N_ ff3(.C(clk), .D(1'b0), .Q(y));
|
||||
(* init=1'b0 *) wire z;
|
||||
$_DFF_N_ ff4(.C(clk), .D(1'b1), .Q(z));
|
||||
endmodule
|
||||
EOT
|
||||
simplemap
|
||||
equiv_opt abc9 -lut 4 -dff
|
||||
design -load postopt
|
||||
cd abc9_test038
|
||||
select -assert-count 3 t:$_DFF_N_
|
||||
select -assert-none c:ff1 c:ff2 c:ff4 %% c:* %D
|
||||
clean
|
||||
select -assert-count 2 a:init
|
||||
select -assert-none w:w w:z %% a:init %D
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue