A computer-implemented method of exhaustively verifying a counter of a hardware design, the method comprising: (a) receiving the hardware design, a test bench counter designed to simulate a desired behavior of the counter, and an inductive assertion establishing a relationship between the counter and the test bench counter at two or more points in time, wherein the inductive assertion asserts that if a value of the counter is equal to a value of the test bench counter at a first point in time that the value of the counter is equal to the value of the test bench counter at a second point in time, the first and second points in time being different clock cycles; (b) formally verifying, using a formal verification tool, the inductive assertion for the counter starting from a non-reset state of the counter; and (c) in response to the formal verification tool identifying at least one valid state of the counter in which the inductive assertion is not true, outputting information indicating a location of a bug in the counter or the test bench counter; (d) in response to outputting the information, receiving at least one of a modified counter and a modified test bench counter and repeating (b) using the modified counter or the modified test bench counter; and (e) in response to the formal verification tool determining the inductive assertion is true for all valid states of the counter, exhaustively verifying the counter by formally verifying, using the formal verification tool, a non-inductive assertion for the counter starting from a reset state of the counter, the non-inductive assertion establishing equivalence of the counter and the test bench counter. (a) receiving the hardware design, a test bench counter designed to simulate a desired behavior of the counter, and an inductive assertion establishing a relationship between the counter and the test bench counter at two or more points in time, wherein the inductive assertion asserts that if a value of the counter is equal to a value of the test bench counter at a first point in time that the value of the counter is equal to the value of the test bench counter at a second point in time, the first and second points in time being different clock cycles; (b) formally verifying, using a formal verification tool, the inductive assertion for the counter starting from a non-reset state of the counter; and (c) in response to the formal verification tool identifying at least one valid state of the counter in which the inductive assertion is not true, outputting information indicating a location of a bug in the counter or the test bench counter; (d) in response to outputting the information, receiving at least one of a modified counter and a modified test bench counter and repeating (b) using the modified counter or the modified test bench counter; and (e) in response to the formal verification tool determining the inductive assertion is true for all valid states of the counter, exhaustively verifying the counter by formally verifying, using the formal verification tool, a non-inductive assertion for the counter starting from a reset state of the counter, the non-inductive assertion establishing equivalence of the counter and the test bench counter.