Building Efficient Portfolio-based Hardware Model Checker via And-Inverter Graph Structure Encoding
TimeTuesday, July 12th6pm - 7pm PDT
LocationLevel 2 Lobby
Event Type
Networking Reception
Work-in-Progress Poster
DescriptionAnd-Inverter Graph (AIG)–a representation of electrical circuits–is the standard input format for hardware model checkers. In this paper, we propose And-Inverter Graph Structure Encoding (AIGSE) to extract the features of AIGs and build a portfolio-based hardware model checker Liquid based on this encoding. The key idea of AIGSE is to encode a vector that represents the numbers of sub-structures in an AIG. By using random forest, Liquid can choose a relatively fast hardware model checker in the portfolio according to the vector. In our experiments, Liquid outperforms all state-of-the-art hardware model checkers in the portfolio.