# Ensure all sync-only DFFs have usable SAT models.

read_verilog -icells <<EOT

module top(...);

input C, D, R, E;
output [4:0] Q;

\$dff #(.WIDTH(1), .CLK_POLARITY(1'b1)) ff0 (.CLK(C), .D(D), .Q(Q[0]));
\$dffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .EN_POLARITY(1'b1)) ff1 (.CLK(C), .D(D), .EN(E), .Q(Q[1]));
\$sdff #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0)) ff2 (.CLK(C), .D(D), .SRST(R), .Q(Q[2]));
\$sdffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff3 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[3]));
\$sdffce #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff4 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[4]));

endmodule

EOT

# This ensures that 1) coarse cells have SAT models, 2) fine cells have SAT models, 3) they're equivalent
equiv_opt -assert simplemap