1. A digital circuit design verification method comprising: determining, for each property of a non-reduced RTL model, a reduced RTL model for a design specification, the reduced RTL model retaining the signal property of the non-reduced RTL model; and subjecting the reduced RTL model to a property checking process.