ATPG4SV
A prototype of Concolic Testing engine for SystemVerilog, developed as part of PFN summer internship 2018.
Tech stack & purpose
ATPG4SV is a prototype concolic testing engine for SystemVerilog that automatically generates test cases achieving 100% line-of-code coverage for circuits by alternating between concrete and symbolic execution. The system is built in OCaml and uses the Z3 SMT solver to generate input vectors that exercise unexecuted code paths, following approaches similar to DART and HYBRO. It was developed by Hiroki Oshikawa as part of Preferred Networks' summer internship program in 2018 and operates by parsing SystemVerilog source code into control flow graphs, executing the program with random inputs, analyzing execution traces from VCD dumps, and iteratively solving symbolic constraints to discover new test cases.
Community & reference links
Languages
Contributors
- Hiroki Oshikawa1 commits