Close

Presentation

FORMAL VERIFICATION CONTRACT BASED SoC SECURITY VALIDATION
DescriptionThe validation of complex SoC relies heavily on coverage analysis and debugging of missed coverage. Existing debug and coverage analysis methodology already published as ("129, Formal verification contract based micro-architectural analysis of Server SoC's, Front-End Design Track 2022”) in DAC has below limitations: 1) Manual effort is required to write properties which justify design specifications. 2) For complex SoC flows, creating a composition of these properties is also a manual task. 3) Result analysis includes manual wave dump analysis at failure timestamps for respective properties, which makes static reasoning difficult. We have scaled up the contract compositional framework for features like SoC Security with below features: 1) We have added a template for formal operators to write formal properties. 2)Based on the template, the automated composition is created for these properties. 3) Result is shown in pictorial wave representation with respect to failure timestamps, making static reasoning more efficient. The proposed framework uses a temporal logic-based query mechanism. This mechanism provides us to write system-level contracts which are decomposed of component-level guarantees. These are defined using Linear Temporal Logic (LTL) properties (called queries in this case) to Timed LTL and help realize an offline property justification framework.
Event Type
Engineering Track Poster
TimeWednesday, July 12th5:30pm - 5:32pm PDT
LocationLevel 2 Exhibit Hall
Topics
Back-End Design
Embedded Systems
Front-End Design
IP
RISC-V