Presentation
A Novel Flow to Verify SoC Integration with Formal Property Verification
DescriptionFormal Verification is widely applied at IP level. FPV and its Apps are largely used (Linting, Register check, Coverage). IPs are often signed-off only with Formal. Our aim is to use FPV at SoC level.
Our top-level verification tasks:
1. IP integration:
Check that all the IPs are correctly connected on the bus and accessible by the masters.
2. IP operation:
Check that all the IPs are functionally working in SoC.
3. System behavior:
Check that the main application is working.
The tests are usually developed in C code and executed by a CPU in a UVM test bench.
The paper is focused on step 1; the idea is to use the Formal Property Verification to prove the IP integration. Internally developed Python utility generates specific SVA assertions by a simple SoC description excel file. It produces read-write properties that check the accessibility of the peripheral registers and memory spaces from the CPU bus master.
This approach verifies the SoC integration early in the flow, with no UVM; the bugs commonly discovered are:
- Wrong memory map
- Wrong data bus connection
- IP clock and/or reset stuck-at
- Wrong peripheral's reset value
Our top-level verification tasks:
1. IP integration:
Check that all the IPs are correctly connected on the bus and accessible by the masters.
2. IP operation:
Check that all the IPs are functionally working in SoC.
3. System behavior:
Check that the main application is working.
The tests are usually developed in C code and executed by a CPU in a UVM test bench.
The paper is focused on step 1; the idea is to use the Formal Property Verification to prove the IP integration. Internally developed Python utility generates specific SVA assertions by a simple SoC description excel file. It produces read-write properties that check the accessibility of the peripheral registers and memory spaces from the CPU bus master.
This approach verifies the SoC integration early in the flow, with no UVM; the bugs commonly discovered are:
- Wrong memory map
- Wrong data bus connection
- IP clock and/or reset stuck-at
- Wrong peripheral's reset value
Event Type
Engineering Track Poster
TimeTuesday, June 255:16pm - 5:17pm PDT
LocationLevel 2 Exhibit Hall
Back-End Design
Embedded Systems
Front-End Design
IP