Abstract Formal hardware verification ensures that a design satisfies its specifications, but writing these specifications requires substantial manual effort. Specification mining automates this process, and existing work has their own merits. The classic approaches rely on pre-defined templates, which have limited expressiveness and lack formal correctness guarantees. However, recent years have seen the emergence of using formal program synthesis for specification mining, which provides general and correct specifications but struggles to scale to complex designs. In this work, we present MAPminer, a parallel framework for synthesis-based hardware specification mining. MAPminer exploits its novel algorithm based on the Maximal Universal Subset and partitions the synthesis problem into efficient sub-problems. These sub-problems are automatically scheduled across multiple threads for parallel synthesis. Experimental results show that MAPminer produces more effective assertions, improving verification coverage while reducing assertion size.

When modifying an existing codebase to handle new functionality, programmers will often debug the program until the insertion point for the new code. This method, termed Debugging into Existence, helps programmers familiarize themselves with the surrounding code and runtime state. Despite its realworld usage, it is limited by the inability to test potential code past the first time the location is called, since added functionality would change the future state making it irrelevant. Prior work has pioneered Live Execution over partial programs, with extensions using the provided values for synthesis by Programming by Example. In this work, we present DeSynt, a debugger extension that integrates live execution and program synthesis to extend the Debugging into Existence interaction model. DeSynt grants programmers meaningful runtime information across many executions, by allowing them to manipulate program state according to the desired functionality. Based on the state provided by the programmer, DeSynt then synthesizes programs that capture this functionality. We evaluated DeSynt in a between-subjects study on 10 users, and found that in tasks that do not involve complex fault localization, deSynt reduces time to completion and concentrates programmer effort into fewer code locations. In addition, we found that users that used DeSynt spent more of their task time debugging, indicating DeSynt supports Debugging into Existence for those that already use it.