Design And Implementation Of Feedback-Guided Fuzzing Framework For Hardware Model Checkers

Hardware model checker is one of the important tools to ensure the correctness of the hardware design.However,as a software,hardware model checker may also have some bugs.These bugs may cause model checker crash or give an incorrect result.While it is inefficient to find these bugs by writing testcases manually,we need an automated testing approach to test the hardware model checker.Fuzzing is one of the important ways in the field of software automated testing.It can generate test cases automatically and randomly.Fuzzing has been proved its useful to test lots kinds of software,so it can be one of the possible ways to test hardware model checkers.However,the existing fuzzing tools still have the following problem for hardware model checker:(1)The generated test cases may invalid for hardware model checker.(2)Because of mutation without a target guided,our testing may be inefficiency.(3)Testing mainly concerned about crash,regardless of the correctness of theprogram.In order to solve these problems,the paper develops a hardware model checker testing tool which named hammer.Hammer make use of code execution paths to guide mutation direction to the new path.In order to develop hammer,the paper has done the following work:(1)We use aiger format as our testing tool input,and put a mutation algorithm for aiger format.The mutation algorithm can generate test cases which meet aiger format standard,so that these test cases can be vaild input for hardware model checkers.(2)We use feed-back guided strategy to guide fuzzing testing,including coverage guide and performance guide.(3)We developed differential testing script to find soundness bugs in hardware model checkers.(4)We tested hardware model checkers actually and found some crash and soundness bugs,that verified our testing tool is effective.(5)Testing different ways of hardware model checking fuzzing to verify the efficiency of Hammer.