High level verification of software and hardware description and sharing resources among concurrent processes
AssigneeFujitsu Limited
InventorSreeranga P. Rajan
Life of this patent
Estimating the term…
Abstract
A state-transition system is extracted from a high-level description of a design. Assumptions regarding states of the design are determined for an initial clock cycle. Linear arithmetic relations are introduced to these assumptions. Guarantees are determine that provide properties of the design that hold after a fixed number of clock cycles. Symbolic simulation is performed for a limited number of clock cycles on the state transition system of the design. If the guarantees hold once simulation is performed, the design is verified. Otherwise, counter-examples are generated.
Claims19
A verification system for verifying correctness of a design, the system comprising:
- a translator extracting a state transition system from a high-level description representing the design, the state transition system comprising a plurality of states;
- and
- a checker establishing assumptions for the extracted state transition system at an initial clock cycle in which at least one linear arithmetic relation is determined for the plurality of states of the state transition system, establishing guarantees for the state transition system in which predetermined conditions hold after a fixed number of clock cycles and simulating the state transition system.
A method of verifying correctness of a design provided as a high-level description, the method comprising:
- extracting from a high-level description a state transition system, the state transition system comprising a plurality of states;
- establishing assumptions for the state transition system at an initial clock cycle in which at least one linear arithmetic relation is provided for a plurality of states defined in the state transition system;
- establishing guarantees for the state transition system in which predetermined conditions hold after a fixed number of clock cycles;
- simulating the state transition system;
- and
- comparing the simulation results to expected results.
Dependencies are inferred from the claim text.