Merge pull request #1505 from YosysHQ/eddie/xaig_dff_adff

xaig_dff to support async flops $_DFF_[NP][NP][01]_
This commit is contained in:
Eddie Hung 2019-11-23 08:22:03 -08:00 committed by GitHub
commit 23fcdd96b3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 53 additions and 13 deletions

View File

@ -863,7 +863,8 @@ struct XAigerWriter
dict<SigSig, SigSig> replace;
for (auto it = holes_module->cells_.begin(); it != holes_module->cells_.end(); ) {
auto cell = it->second;
if (cell->type.in("$_DFF_N_", "$_DFF_P_")) {
if (cell->type.in("$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1", "$_DFF_PP0_", "$_DFF_PP1_")) {
SigBit D = cell->getPort("\\D");
SigBit Q = cell->getPort("\\Q");
// Remove the DFF cell from what needs to be a combinatorial box

View File

@ -120,10 +120,11 @@ module FDCE (output reg Q, input C, CE, D, CLR);
.IS_D_INVERTED(IS_D_INVERTED),
.IS_CLR_INVERTED(IS_CLR_INVERTED)
) _TECHMAP_REPLACE_ (
.D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(IS_CLR_INVERTED)
.D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
// ^^^ Note that async
// control is disabled
// here but captured by
// control is not directly
// supported by abc9 but its
// behaviour is captured by
// $__ABC9_ASYNC below
);
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
@ -142,10 +143,11 @@ module FDCE_1 (output reg Q, input C, CE, D, CLR);
FDCE_1 #(
.INIT(INIT)
) _TECHMAP_REPLACE_ (
.D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(1'b0)
.D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
// ^^^ Note that async
// control is disabled
// here but captured by
// control is not directly
// supported by abc9 but its
// behaviour is captured by
// $__ABC9_ASYNC below
);
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
@ -169,10 +171,11 @@ module FDPE (output reg Q, input C, CE, D, PRE);
.IS_D_INVERTED(IS_D_INVERTED),
.IS_PRE_INVERTED(IS_PRE_INVERTED),
) _TECHMAP_REPLACE_ (
.D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(IS_PRE_INVERTED)
.D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
// ^^^ Note that async
// control is disabled
// here but captured by
// control is not directly
// supported by abc9 but its
// behaviour is captured by
// $__ABC9_ASYNC below
);
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
@ -189,10 +192,11 @@ module FDPE_1 (output reg Q, input C, CE, D, PRE);
FDPE_1 #(
.INIT(INIT)
) _TECHMAP_REPLACE_ (
.D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(1'b0)
.D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
// ^^^ Note that async
// control is disabled
// here but captured by
// control is not directly
// supported by abc9 but its
// behaviour is captured by
// $__ABC9_ASYNC below
);
\$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));

View File

@ -272,3 +272,15 @@ module abc9_test029(input clk1, clk2, input d, output reg q1, q2);
always @(posedge clk1) q1 <= d;
always @(negedge clk2) q2 <= q1;
endmodule
module abc9_test030(input clk, d, r, output reg q);
always @(posedge clk or posedge r)
if (r) q <= 1'b0;
else q <= d;
endmodule
module abc9_test031(input clk, d, r, output reg q);
always @(negedge clk or posedge r)
if (r) q <= 1'b1;
else q <= d;
endmodule

View File

@ -9,3 +9,10 @@ wire w;
unknown u(~i, w);
unknown2 u2(w, o);
endmodule
module abc9_test032(input clk, d, r, output reg q);
initial q = 1'b0;
always @(negedge clk or negedge r)
if (!r) q <= 1'b0;
else q <= d;
endmodule

View File

@ -22,3 +22,19 @@ abc9 -lut 4
select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
select -assert-count 1 t:unknown
select -assert-none t:$lut t:unknown %% t: %D
design -load read
hierarchy -top abc9_test032
proc
clk2fflogic
design -save gold
abc9 -lut 4
check
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 10 -verify -prove-asserts -show-ports miter