Formal verification contract based micro architectural analysis of Server SoC's
TimeMonday, July 11th11:30am - 11:45am PDT
Location2010, Level 2
DescriptionThe most challenging task in System on Chip (SoC) design is in it’s validation and an assurance that validation covers entire design exhaustively, is ensured using various assertion property and coverage metrics. Server System on Chip (SoC) are power and performance greedy designs. Consequently, micro analysis such SoC Holds prominence. Such analysis with existing validation infrastructure cannot be achieved because of the enabling all assertions at SoC leads to increase in simulation time and logs have huge data and difficult to analysis. Also, assertion enabled test takes huge amount of time for simulation. Moreover, selective assertions enablement is not seamless in validation infrastructure. Functional coverage analysis of such features must be timing accurate from IP to SOC, such type of coverage analysis is not done in standard coverage paradigm on SoC. We address this problem by developing an offline Temporal logic-based query mechanism. This mechanism provides us to write simple Linear Temporal Logic (LTL) properties (called as queries in this case) to Timed Linear Temporal Logic (TTL) and helps realize an offline formal verification engine. The framework helps debug the waveform database as TTL queries and results are returned within few minutes, consequently, making micro architecture analysis easy. Moreover, this solution comes with a package of many allied benefits. We claim to improve the micro architecture analysis effort as we get a speedup of the order of 4x while debugging failed scenarios, as well as significant improvement in coverage analysis.