We describe a relatively simple method for strengthening invariants
when verifying infinite-state hardware systems called {\em symbolic
consistency testing}.  The method requires a high-level symbolic
simulator and a decision procedure for quantifier-free first-order
logic.  The user only needs to provide a small number of simple
symbolic test vectors that expose internal inconsistencies in the
system state.  A verification system then uses symbolic simulation
with these test vectors to strengthen the original invariant to an
inductive one, which is discharged using $k$-step induction.  The main
advantage of our method is that the user input is usually very simple
and intuitive, and the user does not need to be exposed to the actual
complexity of the verification, which then proceeds completely
automatically.  The method is applied to several typical
microarchitectures for cached memories.