mirror of https://github.com/YosysHQ/yosys.git
abc9_map.v to transform INIT=1 to INIT=0
This commit is contained in:
Eddie Hung
parent
258a34e6f1
commit
19bc429482
|
|
@ -71,27 +71,39 @@
|
|||
// state
|
||||
// (e) a special _TECHMAP_REPLACE_.$abc9_currQ wire that will be used for feedback
|
||||
// into the (combinatorial) FD* cell to facilitate clock-enable behaviour
|
||||
//
|
||||
// In order to perform sequential synthesis, `abc9' also requires that
|
||||
// the initial value of all flops be zero.
|
||||
|
||||
module FDRE (output Q, input C, CE, D, R);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
parameter [0:0] IS_C_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_D_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_R_INVERTED = 1'b0;
|
||||
wire DD, QQ, $nextQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
wire QQ, $nextQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDSE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_S_INVERTED(IS_R_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .S(R)
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDRE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_R_INVERTED(IS_R_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .R(R)
|
||||
);
|
||||
end
|
||||
endgenerate
|
||||
FDRE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_R_INVERTED(IS_R_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .R(R)
|
||||
);
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
|
||||
|
||||
// Special signals
|
||||
|
|
@ -102,17 +114,24 @@ module FDRE (output Q, input C, CE, D, R);
|
|||
endmodule
|
||||
module FDRE_1 (output Q, input C, CE, D, R);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
wire DD, QQ, $nextQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
wire QQ, $nextQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDSE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .S(R)
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDRE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .R(R)
|
||||
);
|
||||
end
|
||||
endgenerate
|
||||
FDRE_1 #(
|
||||
.INIT(1'b0),
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .R(R)
|
||||
);
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
|
||||
|
||||
// Special signals
|
||||
|
|
@ -127,25 +146,39 @@ module FDCE (output Q, input C, CE, D, CLR);
|
|||
parameter [0:0] IS_C_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_D_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_CLR_INVERTED = 1'b0;
|
||||
wire DD, QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
endgenerate
|
||||
FDCE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_CLR_INVERTED(IS_CLR_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
wire QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDPE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_PRE_INVERTED(IS_CLR_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .PRE(CLR)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDCE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_CLR_INVERTED(IS_CLR_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end endgenerate
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
|
||||
// Since this is an async flop, async behaviour is also dealt with
|
||||
// using the $_ABC9_ASYNC box by abc9_map.v
|
||||
|
|
@ -159,22 +192,32 @@ module FDCE (output Q, input C, CE, D, CLR);
|
|||
endmodule
|
||||
module FDCE_1 (output Q, input C, CE, D, CLR);
|
||||
parameter [0:0] INIT = 1'b0;
|
||||
wire DD, QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
endgenerate
|
||||
FDCE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDPE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .PRE(CLR)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDCE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end endgenerate
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
|
||||
\$__ABC9_ASYNC abc_async (.A($abc9_currQ), .S(CLR), .Y(QQ));
|
||||
|
||||
|
|
@ -190,25 +233,39 @@ module FDPE (output Q, input C, CE, D, PRE);
|
|||
parameter [0:0] IS_C_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_D_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_PRE_INVERTED = 1'b0;
|
||||
wire DD, QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
endgenerate
|
||||
FDPE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_PRE_INVERTED(IS_PRE_INVERTED),
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
wire QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDCE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_CLR_INVERTED(IS_PRE_INVERTED),
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .CLR(PRE)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDPE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_PRE_INVERTED(IS_PRE_INVERTED),
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end endgenerate
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
|
||||
\$__ABC9_ASYNC abc_async (.A($abc9_currQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
|
||||
|
||||
|
|
@ -220,22 +277,33 @@ module FDPE (output Q, input C, CE, D, PRE);
|
|||
endmodule
|
||||
module FDPE_1 (output Q, input C, CE, D, PRE);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
wire DD, QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
endgenerate
|
||||
FDPE_1 #(
|
||||
.INIT(1'b0),
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
wire QQ, $nextQ, $abc9_currQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDCE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .CLR(PRE)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDPE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
|
||||
// ^^^ Note that async
|
||||
// control is not directly
|
||||
// supported by abc9 but its
|
||||
// behaviour is captured by
|
||||
// $__ABC9_ASYNC below
|
||||
);
|
||||
end endgenerate
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
|
||||
\$__ABC9_ASYNC abc_async (.A($abc9_currQ), .S(PRE), .Y(QQ));
|
||||
|
||||
|
|
@ -251,20 +319,29 @@ module FDSE (output Q, input C, CE, D, S);
|
|||
parameter [0:0] IS_C_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_D_INVERTED = 1'b0;
|
||||
parameter [0:0] IS_S_INVERTED = 1'b0;
|
||||
wire DD, QQ, $nextQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
endgenerate
|
||||
FDSE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_S_INVERTED(IS_S_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .S(S)
|
||||
);
|
||||
wire QQ, $nextQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDRE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_R_INVERTED(IS_S_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .R(S)
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDSE #(
|
||||
.INIT(1'b0),
|
||||
.IS_C_INVERTED(IS_C_INVERTED),
|
||||
.IS_D_INVERTED(IS_D_INVERTED),
|
||||
.IS_S_INVERTED(IS_S_INVERTED)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .S(S)
|
||||
);
|
||||
end endgenerate
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
|
||||
|
||||
// Special signals
|
||||
|
|
@ -275,17 +352,23 @@ module FDSE (output Q, input C, CE, D, S);
|
|||
endmodule
|
||||
module FDSE_1 (output Q, input C, CE, D, S);
|
||||
parameter [0:0] INIT = 1'b1;
|
||||
wire DD, QQ, $nextQ;
|
||||
generate if (INIT == 1'b1)
|
||||
assign DD = ~D, Q = ~QQ;
|
||||
else
|
||||
assign DD = D, Q = QQ;
|
||||
endgenerate
|
||||
FDSE_1 #(
|
||||
.INIT(1'b0),
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(DD), .Q($nextQ), .C(C), .CE(CE), .S(S)
|
||||
);
|
||||
wire QQ, $nextQ;
|
||||
generate if (INIT == 1'b1) begin
|
||||
assign Q = ~QQ;
|
||||
FDRE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(~D), .Q($nextQ), .C(C), .CE(CE), .R(S)
|
||||
);
|
||||
end
|
||||
else begin
|
||||
assign Q = QQ;
|
||||
FDSE_1 #(
|
||||
.INIT(1'b0)
|
||||
) _TECHMAP_REPLACE_ (
|
||||
.D(D), .Q($nextQ), .C(C), .CE(CE), .S(S)
|
||||
);
|
||||
end endgenerate
|
||||
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
|
||||
|
||||
// Special signals
|
||||
|
|
|
|||
|
|
@ -0,0 +1,91 @@
|
|||
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
|
||||
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
|
||||
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
|
||||
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
|
||||
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
|
||||
Loading…
Reference in New Issue