A new and convenient methodology for proving the correctness of multiplier and multiply-accumulate circuit designs in a full custom design flow. Such an approach utilizes a basic description of the implemented algorithm, which is created in early phases of the design flow and requires only little extra work for the designer who spends most of the time in full-custom optimizations. Such an approach also defines arithmetic circuit at the arithmetic bit level and allows for the generation of a gate level netlist. Given a structural similarity between the specification and design under verification, a large amount of structural similarity between the generated netlists is obtained so that a standard equivalence checker can be utilized to verify the design against the specification.