diff options
| -rw-r--r-- | passes/sat/clk2fflogic.cc | 83 | ||||
| -rw-r--r-- | tests/sat/clk2fflogic.ys | 66 |
2 files changed, 143 insertions, 6 deletions
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 4bb4aa047..f9e7783a9 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -214,14 +214,38 @@ struct Clk2fflogicPass : public Pass { continue; } - if (cell->type.in("$dff", "$adff", "$dffsr")) + bool word_dff = cell->type.in("$dff", "$adff", "$dffsr"); + if (word_dff || cell->type.in(ID($_DFF_N_), ID($_DFF_P_), + ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), + ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_), + ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), + ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_))) { - bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool(); + bool clkpol; + SigSpec clk; + if (word_dff) { + clkpol = cell->parameters["\\CLK_POLARITY"].as_bool(); + clk = cell->getPort("\\CLK"); + } + else { + if (cell->type.in(ID($_DFF_P_), ID($_DFF_N_), + ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), + ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_))) + clkpol = cell->type[6] == 'P'; + else if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), + ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_))) + clkpol = cell->type[8] == 'P'; + else log_abort(); + clk = cell->getPort("\\C"); + } - SigSpec clk = cell->getPort("\\CLK"); Wire *past_clk = module->addWire(NEW_ID); past_clk->attributes["\\init"] = clkpol ? State::S1 : State::S0; - module->addFf(NEW_ID, clk, past_clk); + + if (word_dff) + module->addFf(NEW_ID, clk, past_clk); + else + module->addFfGate(NEW_ID, clk, past_clk); SigSpec sig_d = cell->getPort("\\D"); SigSpec sig_q = cell->getPort("\\Q"); @@ -244,8 +268,14 @@ struct Clk2fflogicPass : public Pass { Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d)); Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q)); - module->addFf(NEW_ID, sig_d, past_d); - module->addFf(NEW_ID, sig_q, past_q); + if (word_dff) { + module->addFf(NEW_ID, sig_d, past_d); + module->addFf(NEW_ID, sig_q, past_q); + } + else { + module->addFfGate(NEW_ID, sig_d, past_d); + module->addFfGate(NEW_ID, sig_q, past_q); + } if (cell->type == "$adff") { @@ -266,6 +296,26 @@ struct Clk2fflogicPass : public Pass { module->addMux(NEW_ID, rstval, qval, arst, sig_q); } else + if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), + ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_))) + { + SigSpec arst = cell->getPort("\\R"); + SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); + SigBit rstval = (cell->type[8] == '1'); + + Wire *past_arst = module->addWire(NEW_ID); + module->addFfGate(NEW_ID, arst, past_arst); + if (cell->type[7] == 'P') + arst = module->OrGate(NEW_ID, arst, past_arst); + else + arst = module->AndGate(NEW_ID, arst, past_arst); + + if (cell->type[7] == 'P') + module->addMuxGate(NEW_ID, qval, rstval, arst, sig_q); + else + module->addMuxGate(NEW_ID, rstval, qval, arst, sig_q); + } + else if (cell->type == "$dffsr") { SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); @@ -282,9 +332,30 @@ struct Clk2fflogicPass : public Pass { module->addAnd(NEW_ID, qval, clrval, sig_q); } else + if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), + ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_))) + { + SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); + SigSpec setval = cell->getPort("\\S"); + SigSpec clrval = cell->getPort("\\R"); + + if (cell->type[9] != 'P') + setval = module->Not(NEW_ID, setval); + + if (cell->type[10] == 'P') + clrval = module->Not(NEW_ID, clrval); + + qval = module->OrGate(NEW_ID, qval, setval); + module->addAndGate(NEW_ID, qval, clrval, sig_q); + } + else if (cell->type == "$dff") { module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q); } + else + { + module->addMuxGate(NEW_ID, past_q, past_d, clock_edge, sig_q); + } Const initval; bool assign_initval = false; diff --git a/tests/sat/clk2fflogic.ys b/tests/sat/clk2fflogic.ys new file mode 100644 index 000000000..6d6d9e490 --- /dev/null +++ b/tests/sat/clk2fflogic.ys @@ -0,0 +1,66 @@ +read_verilog -icells <<EOT +module top(input clk, d, s, r, output reg [17:0] q); +always @(posedge clk or posedge s) if ( s) q[ 0] <= 1'b1; else q[ 0] <= d; +always @(posedge clk or negedge s) if (!s) q[ 1] <= 1'b1; else q[ 1] <= d; +always @(posedge clk or posedge r) if ( r) q[ 2] <= 1'b0; else q[ 2] <= d; +always @(posedge clk or negedge r) if (!r) q[ 3] <= 1'b0; else q[ 3] <= d; +always @(negedge clk or posedge s) if ( s) q[ 4] <= 1'b1; else q[ 4] <= d; +always @(negedge clk or negedge s) if (!s) q[ 5] <= 1'b1; else q[ 5] <= d; +always @(negedge clk or posedge r) if ( r) q[ 6] <= 1'b0; else q[ 6] <= d; +always @(negedge clk or negedge r) if (!r) q[ 7] <= 1'b0; else q[ 7] <= d; + +// Seems like proc_dlatch always sets {SET,CLR}_POLARITY to true +always @(posedge clk or posedge s or posedge r) if ( r) q[ 8] <= 1'b0; else if ( s) q[ 8] <= 1'b1; else q[ 8] <= d; +//always @(posedge clk or posedge s or negedge r) if (!r) q[ 9] <= 1'b0; else if ( s) q[ 9] <= 1'b1; else q[ 9] <= d; +//always @(posedge clk or negedge s or posedge r) if ( r) q[10] <= 1'b0; else if (!s) q[10] <= 1'b1; else q[10] <= d; +//always @(posedge clk or negedge s or negedge r) if (!r) q[11] <= 1'b0; else if (!s) q[11] <= 1'b1; else q[11] <= d; +$dffsr #(.CLK_POLARITY(1'h1), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h1), .WIDTH(32'd1)) ppn (.CLK(clk), .CLR(r), .D(d), .Q(q[ 9]), .SET(s)); +$dffsr #(.CLK_POLARITY(1'h1), .CLR_POLARITY(1'h1), .SET_POLARITY(1'h0), .WIDTH(32'd1)) pnp (.CLK(clk), .CLR(r), .D(d), .Q(q[10]), .SET(s)); +$dffsr #(.CLK_POLARITY(1'h1), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h0), .WIDTH(32'd1)) pnn (.CLK(clk), .CLR(r), .D(d), .Q(q[11]), .SET(s)); + +always @(negedge clk or posedge s or posedge r) if ( r) q[12] <= 1'b0; else if ( s) q[12] <= 1'b1; else q[12] <= d; +//always @(negedge clk or posedge s or negedge r) if (!r) q[13] <= 1'b0; else if ( s) q[13] <= 1'b1; else q[13] <= d; +//always @(negedge clk or negedge s or posedge r) if ( r) q[14] <= 1'b0; else if (!s) q[14] <= 1'b1; else q[14] <= d; +//always @(negedge clk or negedge s or negedge r) if (!r) q[15] <= 1'b0; else if (!s) q[15] <= 1'b1; else q[15] <= d; +$dffsr #(.CLK_POLARITY(1'h0), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h1), .WIDTH(32'd1)) npn (.CLK(clk), .CLR(r), .D(d), .Q(q[13]), .SET(s)); +$dffsr #(.CLK_POLARITY(1'h0), .CLR_POLARITY(1'h1), .SET_POLARITY(1'h0), .WIDTH(32'd1)) nnp (.CLK(clk), .CLR(r), .D(d), .Q(q[14]), .SET(s)); +$dffsr #(.CLK_POLARITY(1'h0), .CLR_POLARITY(1'h0), .SET_POLARITY(1'h0), .WIDTH(32'd1)) nnn (.CLK(clk), .CLR(r), .D(d), .Q(q[15]), .SET(s)); + +always @(posedge clk) q[16] <= d; +always @(negedge clk) q[17] <= d; +endmodule +EOT +proc +select -assert-count 8 t:$adff +select -assert-count 8 t:$dffsr +select -assert-count 2 t:$dff +design -save gold + +simplemap +select -assert-count 1 t:$_DFF_NN0_ +select -assert-count 1 t:$_DFF_NN1_ +select -assert-count 1 t:$_DFF_NP0_ +select -assert-count 1 t:$_DFF_NP1_ +select -assert-count 1 t:$_DFF_PN0_ +select -assert-count 1 t:$_DFF_PN1_ +select -assert-count 1 t:$_DFF_PP0_ +select -assert-count 1 t:$_DFF_PP1_ +stat +select -assert-count 1 t:$_DFFSR_NNN_ +select -assert-count 1 t:$_DFFSR_NNP_ +select -assert-count 1 t:$_DFFSR_NPN_ +select -assert-count 1 t:$_DFFSR_NPP_ +select -assert-count 1 t:$_DFFSR_PNN_ +select -assert-count 1 t:$_DFFSR_PNP_ +select -assert-count 1 t:$_DFFSR_PPN_ +select -assert-count 1 t:$_DFFSR_PPP_ +select -assert-count 1 t:$_DFF_N_ +select -assert-count 1 t:$_DFF_P_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate +clk2fflogic + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -set-init-undef -seq 10 miter |