DescriptionFor a high-performance LZ4 Compression System implementation, we take on the task of proving key data coherency requirements of the design. Attempting this proof on the RTL of the Compression System is impractical because of the size and complexity of the hardware design. To overcome this barrier, we deployed the Architectural Formal Sign-off methodology.
The Compression System has a deep pipeline, which is composed of five major blocks. The compression ratio is data dependent, so the final data size is only known at the last of the blocks in the pipeline. However, the earlier blocks in the pipeline play a role in keeping the pipeline full, and any data already launched into the pipeline must also be compressed without overwhelming resources and breaking data coherency in the later stages.
We formally verified the Compression System resource sizing choices, which delivered the utmost confidence in the design implementation. We also demonstrated where there was margin in the system, and to what limit that margin could be trimmed and still maintain the proof.