Computer implemented method of high-level synthesis for the efficient verification of computer software
AssigneeNEC Laboratories America, Inc.
InventorsMalay Ganai, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
Verification friendly models for SAT-based formal verification are generated from a given high-level design wherein during construction the following guidelines are enforced: 1) No re-use of functional units and registers; 2) Minimize the use of muxes and sharing; 3) Reduce the number of control steps; 4) Avoid pipelines; 5) Chose functional units from “verification friendly” library; 6) Re-use operations; 7) Perform property-preserving slicing; 8) Support “assume” and “assert” in the language specification; and 8) Use external memory modules instead of register arrays.
Claims7
A computer-implemented method of verifying computer software comprising the steps of:
- generating a verification aware model of the software using High-Level Synthesis (HLS) tools including the steps of:
- prioritizing any HLS criteria wherein the criteria include:
- timing, area, power and verification performance;
- and
- assigning the highest priority to the verification performance criteria irrespective of any effect that assignment has on the other criteria;
- verifying the generated model using a formal verification methodology;
- and
- outputting an indicia of correctness of the software resulting from the model verification.
Dependencies are inferred from the claim text.