Using augmented BDI models for intelligent stimuli generation

受限随机验证(CRV)和形式化验证是目前最先进的功能验证方法。CRV的优势在于不受大小限制。因此，它可以应用于大型设计。然而，CRV的效率很低，许多模拟周期都花费在探索相同的状态空间上。此外，将工具引导到有趣的角落案例中通常需要验证工程师付出相当大的人工努力。相反，形式验证可以发现转角情况，几乎不需要手动转向；但由于复杂性的限制，它只能详尽地应用于相对较小的设计。本研究旨在利用BDI(Believe-Desire-Intent)智能，并结合机器学习技术，探讨CRV与正式验证之间的中间地带。基于BDI的方法提供高层的、目标导向的计划，并通过回溯来实现设定的目标。用奖惩系统扩展BDI模型可以促进基于代理的智能测试刺激的生成，该刺激可以自动发现并命中复杂设计(如CPU)上有趣的角落案例。这减少了对手写约束和随机测试生成的依赖。该解决方案还将适用于其他验证用例，例如硅片后调试和集群级别的测试用例自动化。

Constrained random verification (CRV) and formal verification are currently the state-of-the-art approaches to functional verification. CRV's advantage is that does not suffer from size restrictions. Hence it can be applied to large designs. However, CRV is inefficient, with many simulation cycles spent exploring the same state space. Furthermore, guiding the tools into interesting corner cases typically requires considerable manual effort from verification engineers. Conversely, formal verification can find corner cases with little manual steering; but due to complexity limits, it can only be applied exhaustively to relatively small designs. This research aims to employ BDI (Belief-Desire-Intention) intelligence, augmented by machine learning techniques, to investigate the middle ground between CRV and formal verification. A BDI-based approach offers high-level, goal-directed planning with backtracking to achieve set goals. Augmenting a BDI model with a reward/punishment system can facilitate intelligent, agent-based generation of test stimuli which can automatically find and hit the interesting corner cases on a complex design, such as a CPU. This results in less reliance on hand-written constraints and random test generation. The solution would also be applicable to other verification use-cases such as post-silicon debug and test case automation at cluster level.