Presentation
Approach For Quality DV Using C2RTL For Algorithmic Designs Authors: Neema Agarwal, Himanshu Chauhan, Harsh Setia, Atharva Mahesh Kakde, Ketki Gosavi
DescriptionData path design with algorithmic logic have their own challenges in verification. DV sign off using simulation alone can have holes as it is nearly impossible to cover all scenarios in limited DV time frame. By formally verifying the equivalence check between RTL and its reference C++ model algorithm provides an edge over traditional simulation approach. The paper describes the advantages of using C2RTL equivalence for this verification.
Design Use Case-De-Compression IP:
The decompression IP uses the LZO RLE algorithm for decompressing the data up to 4KB Input compressed data stream, can have input size between 19 bytes to 4KB which makes it difficult to cover all input data values with functional simulation. This can lead to some uncovered scenarios in algorithm and hence bug escapes.
Approach Taken:
1) Instruction based formal verification
2) Reduced number of properties in FV setup
3) Unique Mapping Requirement of C variables with RTL cycle-based signal
Results:
Verified 3 random instructions sequence with Input vector size ranging from 19 – 64 bytes. This resulted in a failure case.
Compressed Input data 60 bytes insize: 240'h00000000d09002000a360088004010111
Decompressed Output Data:
RTL Output: 128'h0000 0009 0020 6060 6060 6060 6008 8004
C++ Output: 128'h0020 6009 0020 6060 6060 6060 6008 8004
After analyzing the LZO algorithm encoding of compressed instruction, C++ decompressed output data is correct, but RTL output data is incorrect. This could not be covered in simulation-based approach even when thousands of input vectors were simulated for more than a month to decompressor RTL.
Design Use Case-De-Compression IP:
The decompression IP uses the LZO RLE algorithm for decompressing the data up to 4KB Input compressed data stream, can have input size between 19 bytes to 4KB which makes it difficult to cover all input data values with functional simulation. This can lead to some uncovered scenarios in algorithm and hence bug escapes.
Approach Taken:
1) Instruction based formal verification
2) Reduced number of properties in FV setup
3) Unique Mapping Requirement of C variables with RTL cycle-based signal
Results:
Verified 3 random instructions sequence with Input vector size ranging from 19 – 64 bytes. This resulted in a failure case.
Compressed Input data 60 bytes insize: 240'h00000000d09002000a360088004010111
Decompressed Output Data:
RTL Output: 128'h0000 0009 0020 6060 6060 6060 6008 8004
C++ Output: 128'h0020 6009 0020 6060 6060 6060 6008 8004
After analyzing the LZO algorithm encoding of compressed instruction, C++ decompressed output data is correct, but RTL output data is incorrect. This could not be covered in simulation-based approach even when thousands of input vectors were simulated for more than a month to decompressor RTL.
Event Type
Engineering Poster
TimeTuesday, June 245:00pm - 6:00pm PDT
LocationEngineering Posters, Level 2 Exhibit Hall