US Patent No. 10,169,495

METHOD FOR VERIFYING HARDWARE/SOFTWARE CO-DESIGNS


Patent No. 10,169,495
Issue Date January 01, 2019
Title Method For Verifying Hardware/software Co-designs
Inventorship Mitra Purandare, Zurich (CH)
Assignee International Business Machines Corporation, Armonk, NY (US)

Claim of US Patent No. 10,169,495

1. A computer system for formally verifying a hardware/software co-design, the computer system comprising:one or more processors, one or more computer-readable memories, one or more computer-readable tangible storage devices, and program instructions stored on at least one of the one or more storage devices for execution by at least one of the one or more processors via at least one of the one or more memories, wherein the computer system is capable of performing a 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.