Computer implemented method of high-level synthesis for the efficient verification of computer software
View Patent ↗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.
1. 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.
2. The computer-implemented method of claim 1 wherein the generated model exhibits no re-use of functional units and registers.
3. The computer-implemented method of claim 1 wherein the generated model exhibits a minimal use of muxes and sharing.
4. The computer-implemented method of claim 1 wherein the generated model exhibits a reduced number of control steps.
5. The computer-implemented method of claim 1 wherein the generated model exhibits limited pipeline usage.
6. The computer-implemented method of claim 1 wherein the generated model uses external memory modules instead of register arrays.
7. The computer-implemented method of claim 1 wherein the generated model has a reduced number of reachable control states at each depth.