1. A method for verifying properties of a circuit model, the method comprising the steps of: a. specifying at least one property to be checked; b. specifying a set of environmental constraints; c. generating a synthesized netlist composed of combinational logic and registers from the circuit model; for each property performing steps d-e; d. identifying an analysis region in context of which the property is satisfied under the set of environmental constraints; and e. providing a result to the user.