Automatic generation of assertions for formal verification of PowerPC/sup TM /microprocessor arrays using symbolic trajectory evaluation
- Year
- 1998
- Authors
- L.-C. Wang, M.S. Abadir, N. Krishnamurthy
- DOI
- 10.1109/DAC.1998.724529
Related
[[vasudevanGoldMineAutomaticAssertion2010]]
Persistent Notes
In-text annotations
“Creating assertions usually requires a deep understanding of the overall functionality of the array so that each array operation can be expressed properly into an assertion. Such a process can be very tedious and potentially incomplete." Page 534
“For complex array designs, assertion creation can be a complicated, tedious, and unreliable process. First, a person needs to fully understand the functionality of a unit before creating the assertions. Assertions themselves can be long and tedious in order to specify all aspects of a design in details. Very often, a verification engineer would create assertions to verify only what he/she understood as the normal operations. Hence, assertions can be incomplete. To avoid all these problems, a way to automatically generate assertions is required." Page 535
%% Import Date: 2026-06-05T17:46:41.506-04:00 %%