Verifying hardware in its software context and vice-versa

A method for verifying design of a system having both software and hardware parts comprising the steps of:

• accepting into storage an input of a specification of the software part in a software-centric language, a specification of the hardware part in a hardware-centric language, a specification of properties that the system is to possess, and an initial set of constraints;
• selecting a property to be verified,
• verifying the selected property,
• when the step of verifying fails, displaying said failing and offering an opportunity to provide modifications to said constraints and/or specifications,
• accepting said modifications,
• returning to said step of verifying, and
• selecting another property to be verified when said step of verifying succeeds.

A method for verifying design of a system that includes software comprising the steps of:

• performing static partial order reduction on a specification of said system;
• converting results of said static partial order reduction to synchronous form;
• verifying design represented by results of said step of converting;
• and
• presenting visual results of said step of verifying.

Apparatus for verifying a design comprising:

• a memory for storing a specification of said design, a collection of properties, and constraints;
• a controller;
• a first processor responsive to those portions in said specification, obtained from said memory, that describe software, for performing static partial order reduction analysis under control of said controller;
• a second processor, responsive to control signals from said controller, for converting to synchronous form those portions in said specification that describe software or for converting to synchronous form output signals of said first processor;
• a verification tool responsive to those portions in said specification, obtained from said memory, that describe hardware, and to output signals of said second processor;
• and
• a display responsive to said verification tool.

Apparatus for verifying a design comprising:

• a memory for storing a specification of said design, a collection of properties, and constraints;
• a stored program processor responsive to signals stored in said memory for performing static partial order reduction on said design followed by symbolic verification;
• and
• a display responsive to signals provided by said processor indicative of whether said design verifies.

Apparatus for verifying a design comprising:

• a memory for storing a specification of said design, a collection of properties, and constraints;
• a controller;
• first means responsive to those portions in said specification, obtained from said memory, that describe software, for performing static partial order reduction analysis;
• second means for converting to synchronous form those portions in said specification that describe software or for converting to synchronous form output signals of said first processor;
• third means responsive to those portions in said specification, obtained from said memory, that describe hardware, and to output signals of said second processor;
• fourth means for controlling said first means, said second means, and said third means;
• and
• a display responsive to said third means.