Modeling system-level behaviors of intricate System-on-Chip (SoC) designs is crucial for design analysis, testing, and validation. However, the complexity and volume of SoC traces pose significant challenges in this task. This paper proposes an approach to automatically infer concise and abstract models from SoC communication traces, capturing the system-level protocols that govern message exchange and coordination between design blocks for various system functions. This approach, referred to as model synthesis, constructs a causality graph with annotations obtained from the SoC traces. The annotated causality graph represents all potential causality relations among messages under consideration. Next, a constraint satisfaction problem is formulated from the causality graph, which is then solved by a satisfiability modulo theories (SMT) solver to find satisfying solutions. Finally, finite state models are extracted from the generated solutions, which can be used to explain and understand the input traces. The proposed approach is validated through experiments using synthetic traces obtained from simulating a transaction-level model of a multicore SoC design and traces collected from running real programs on a realistic multicore SoC modeled with gem5.

翻译：建模复杂片上系统（SoC）设计的系统级行为对于设计分析、测试与验证至关重要。然而，SoC迹的复杂性与规模对此任务提出了重大挑战。本文提出一种方法，可从SoC通信迹中自动推断简洁且抽象的模型，捕获各系统功能下设计模块间消息交换与协调所遵循的系统级协议。该方法称为模型合成，首先从SoC迹中构建带注释的因果图——该图表示所考虑消息间所有潜在的因果关系，随后从因果图形式化约束满足问题，并通过可满足性模理论（SMT）求解器求解以获得满足解，最后从生成解中提取有限状态模型——该模型可用于解释和理解输入迹。通过模拟多核SoC设计的事务级模型获取的合成迹，以及基于gem5建模的真实多核SoC上运行实际程序采集的迹，对所提方法进行实验验证。