Typically in hardware design you'd use combinational equivalence checking (CEC) to formally prove that a synthesized design is correct. See https://en.wikipedia

Typically in hardware design you'd use combinational equivalence checking (CEC) to formally prove that a synthesized design is correct. See https://en.wikipedia.org/wiki/Formal_equivalence_checking https://en.wikipedia.org/wiki/Formal_equivalence_checking. In CEC you use a SAT solver to prove that a new (synthesized and optimized) circuit is equivalent to some reference model (aka golden model) which you know is correct. So instead of relying on just testing (which is incomplete) you have a formal proof that your design is correct. Of course you still have to trust that the SAT solver works correctly... :-)