Presentation
The Pursuit of Golden Specification: Leveraging Architecture Formal
DescriptionThe problem of finding specification bugs during RTL verification is two-fold: (1) It involves weeks of effort to debug, identify and fix architecture bugs. (2) As much as ~20% deviations in project timelines could be caused by fixing the architecture specification. Furthermore, hardware architecture is increasingly complex due to advanced memory schemes and multi-agent systems and are more prone to spec bugs.
These problems could be overcome by embracing architecture-level formal verification (ArchFV). ArchFV adds value to RTL verification not only by shifting left, but also by automating the RTL reference model development.
ArchFV is conducted by creating an executable formal model of specification represented as a collection of tables. The tables are exhaustively verified by model-checkers for passing safety properties and absence of deadlock.
Some of the key outcomes of adopting ArchFV at Intel are:
1. ArchFV of a critical IP, comprising of ~30 tables were formally verified in ~8 weeks
2. ~4050 safety properties proven and ~60 spec bugs fixed
3. ~7 stalled table transitions detected and rectified
4. Saved ~3 weeks of manual effort in reference model development
Overall, ArchFV prevents ripple effects in verification, improves quality of the design and saves product time to market.
These problems could be overcome by embracing architecture-level formal verification (ArchFV). ArchFV adds value to RTL verification not only by shifting left, but also by automating the RTL reference model development.
ArchFV is conducted by creating an executable formal model of specification represented as a collection of tables. The tables are exhaustively verified by model-checkers for passing safety properties and absence of deadlock.
Some of the key outcomes of adopting ArchFV at Intel are:
1. ArchFV of a critical IP, comprising of ~30 tables were formally verified in ~8 weeks
2. ~4050 safety properties proven and ~60 spec bugs fixed
3. ~7 stalled table transitions detected and rectified
4. Saved ~3 weeks of manual effort in reference model development
Overall, ArchFV prevents ripple effects in verification, improves quality of the design and saves product time to market.
Event Type
Engineering Poster
TimeWednesday, July 293:00pm - 4:00pm PDT
LocationDAC Pavilion, Exhibit Floor