kirancodes.me
To Proof Maintenance & Beyond!

Automatic Test Case Generation for Jasper App HDL Compiler: An Industry Experience

Mirlaine Crepalde, Augusto Mafra, Lucas Cavalini, Lucas Martins, Guilherme Amorim, Pedro Henrique Santos, Fabiano Peixoto

Abstract

Random test case generation is a challenging subject in compiler testing. Due to the structured and strict nature of the languages required for compiler inputs, using randomization techniques for hunting bugs in compiler implementation represents a big challenge that requires trading off correctness and generation biases against fuzzing techniques for broader exploratory randomization. This paper shares the technology and the practical industry experience on two random testing frameworks developed for the Hardware Description Language (HDL) compiler of Jasper® App, a production formal verification software applied in Electronic Design Automation (EDA) industry. The two frameworks impact distinct parts of the compiler stack and provide different features and strengths for randomization: SystemVerilog Generator script, which creates random and formally provable HDL code, and Fuzz HDL Testing, a fuzzing solution applying LLVM’s libFuzzer to explore random textual inputs.

Related papers