Browse Prior Art Database

Formal Verification of a Data Compression Accelerator

IP.com Disclosure Number: IPCOM000243034D
Publication Date: 2015-Sep-09
Document File: 1 page(s) / 28K

Publishing Venue

The IP.com Prior Art Database

Abstract

Disclosed is an effective and novel method for the Formal Verification (FV) of a data compressor accelerator. The approach is to abstract the tables and follow certain rules that ensure the correctness of the transformation.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 72% of the total text.

Page 01 of 1

Formal Verification of a Data Compression Accelerator

A hardware data compression implementation necessarily puts stringent requirements on the verification of correctness of the logic and circuit implementation . It is desirable to verify such logic with Formal Verification (FV) to conclusively prove the correctness thereof; however, this suffers from the state explosion problem , given the complexity of the implementations, and the presence of large memory arrays to maintain a history of examined data sets.

Disclosed herein is an effective and novel method to formally verify such circuits with leveraging suitable abstraction to drastically improve the scalability of FV methods .

A data compression engine comprises two parts: a compressor, which generates a reduced encoded form of the data , and a decompressor, which expands the data to its original. A verification test bench needs to at least verify that the tandem operation of the compressor and the decompressor returns the input data stream . In addition, it is desirable to verify the correctness of the compression engine by assessing the conformance of the compressed strings to a specified format . The main source of difficulty when trying to formally verify data compression is the presence of large memory arrays.

The novel solution addresses this by abstracting the memory arrays and following certain rules that ensure the correctness of the abstraction . The abstraction rules are based on legal encoding of...