1. A method for verifying a system against an assertion in a specification, the method comprising the steps of: generating a propositional formula representing an assertion in the specification using Boolean propositions, each Boolean proposition being associated with an atomic assertion in the assertion; generating a test case designed to assess the a behavior of the system with respect to the assertion; generating configuration data in response to a simulation of the test case on the system; converting the configuration data into propositional symbols; generating a run of the system using the propositional symbols; converting the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and verifying the assertion using the propositional symbols and the propositional formula.
4. The method of claim 1 , further including generating an association list that identifies the relationship between the atomic assertions and the propositional symbols.