Presentation
Formal Verification Engineering for Integer Vector Neural Network Instructions
DescriptionIntel has been doing full formal verification of CPU execution datapaths for over 25 years. We present as a case study in verification engineering, the formal verification of the integer subset of VNNI instruction set that was introduced as part of Intel Deep Learning Boost. An example of an Int16 SIMD MUL (SiMUL) VNNI instruction is VPDPWSSD, which multiplies the individual signed words of the first source operand by the corresponding signed words of the second source operand, producing intermediate signed, doubleword results. The adjacent doubleword results are then summed and accumulated in the destination operand. These Int16 and Int8 instructions come in different flavors based on whether sources are signed or unsigned, and whether the intermediate sums on overflowing are saturated to maximum magnitude with the correct sign, for the result. The underlying FV engine is powered by symbolic simulation, which provides the verification engineer the ability to concretely debug verification complexity, and the ability to program around verification complexity. Our verification flow built on top of symbolic simulation using "FV as first class software" approach has enabled us to develop flexible, reusable proofs while providing full data space coverage for all flavors of SiMUL VNNI instructions.
Event Type
Engineering Poster
TimeWednesday, July 293:00pm - 4:00pm PDT
LocationDAC Pavilion, Exhibit Floor