module add4 (input [3:0] a, input [3:0] b, input cin, output [3:0] s, output cout);
  assign {cout, s} = a + b + cin;
endmodule

// Gate netlist with one wrong gate somewhere in the carry chain.

module add4_gate(a, b, cin, s, cout);
  input [3:0] a;
  wire [3:0] a;
  input [3:0] b;
  wire [3:0] b;
  input cin;
  wire cin;
  output [3:0] s;
  wire [3:0] s;
  output cout;
  wire cout;
  wire _00_;
  wire _01_;
  wire _02_;
  wire _03_;
  wire _04_;
  wire _05_;
  wire _06_;
  wire _07_;
  wire _08_;
  wire _09_;
  wire _10_;
  wire _11_;
  wire _12_;
  wire _13_;
  wire _14_;
  assign _00_ = a[3] & b[3];
  assign _01_ = a[2] & b[2];
  assign _02_ = a[1] & b[1];
  assign _03_ = a[0] & b[0];
  assign _04_ = a[0] ^ b[0];
  assign _05_ = cin | _04_;
  assign _06_ = _03_ | _05_;
  assign _07_ = a[1] ^ b[1];
  assign _08_ = _06_ & _07_;
  assign _09_ = _02_ | _08_;
  assign _10_ = a[2] ^ b[2];
  assign _11_ = _09_ & _10_;
  assign _12_ = _01_ | _11_;
  assign _13_ = a[3] ^ b[3];
  assign _14_ = _12_ & _13_;
  assign cout = _00_ | _14_;
  assign s[3] = _12_ ^ _13_;
  assign s[2] = _09_ ^ _10_;
  assign s[1] = _06_ ^ _07_;
  assign s[0] = cin ^ _04_;
endmodule

module add4_miter (input [3:0] a, input [3:0] b, input cin);
  // the same inputs drive both versions
  wire [3:0] s_rtl, s_gate;
  wire       c_rtl, c_gate;
  add4      u_rtl  (.a(a), .b(b), .cin(cin), .s(s_rtl),  .cout(c_rtl));
  add4_gate u_gate (.a(a), .b(b), .cin(cin), .s(s_gate), .cout(c_gate));
`ifdef FORMAL
  // the outputs must always be equal
  always @(*) assert (s_rtl == s_gate && c_rtl == c_gate);
`endif
endmodule