1. A method for formally verifying a hardware/software co-design, the method comprising: providing in a co-design, a first model, and a second model, wherein the first model is one of a hardware model, and the second model is one of a software model, or vice versa; performing an abstraction on the first model, wherein the abstraction comprises refining the first model to a lower abstraction level; specifying a safety property comprising one or more conditions to be satisfied by a composed hardware/software model; combining the abstraction of the first model and the safety property to obtain an abstracted first model; translating the abstracted first model and a corresponding interface model into a Property Specification Language, wherein the Property Specification Language is capable of describing a model environment for the second model; based on the described model environment, composing, by a model checker, the abstracted first model and the second model to obtain the composed hardware/software model, wherein the model checker automatically composes the abstracted first model and the second model using a construct in the Property Specification Language; verifying whether the composed hardware/software model satisfies the safety property; in response to the composed hardware/software model not satisfying the safety property, projecting, by the model checker, a counterexample on the first model, wherein the counterexample is projected on variables of the abstracted first model, the interface model, and the second model such that a sequence of model states is obtained as a consequence of projecting the counterexample; verifying whether the counterexample projected on the first model comprises a real error trace in the first model; based on the counterexample being a real error trace, signaling that the hardware/software co-design violates the safety property; and based on the counterexample not being a real error trace, refining the abstraction of the first model to eliminate the error trace.
1. A method for formally verifying a hardware/software co-design, the method comprising: providing in a co-design, a first model, and a second model, wherein the first model is one of a hardware model, and the second model is one of a software model, or vice versa; performing an abstraction on the first model, wherein the abstraction comprises refining the first model to a lower abstraction level; specifying a safety property comprising one or more conditions to be satisfied by a composed hardware/software model; combining the abstraction of the first model and the safety property to obtain an abstracted first model; translating the abstracted first model and a corresponding interface model into a Property Specification Language, wherein the Property Specification Language is capable of describing a model environment for the second model; based on the described model environment, composing, by a model checker, the abstracted first model and the second model to obtain the composed hardware/software model, wherein the model checker automatically composes the abstracted first model and the second model using a construct in the Property Specification Language; verifying whether the composed hardware/software model satisfies the safety property; in response to the composed hardware/software model not satisfying the safety property, projecting, by the model checker, a counterexample on the first model, wherein the counterexample is projected on variables of the abstracted first model, the interface model, and the second model such that a sequence of model states is obtained as a consequence of projecting the counterexample; verifying whether the counterexample projected on the first model comprises a real error trace in the first model; based on the counterexample being a real error trace, signaling that the hardware/software co-design violates the safety property; and based on the counterexample not being a real error trace, refining the abstraction of the first model to eliminate the error trace. 5. The method according to claim 1 , wherein verifying whether the counterexample projected on the first model comprises a real error trace in the first model comprises using Bounded Model Checking to leverage the success of fast propositional SAT solvers.