Equivalence checking in C-based system-level design by sequentializing concurrent behaviors
Equivalence checking in C-based system-level design by sequentializing concurrent behaviors
复制标题
通过对并发行为进行排序来进行基于 C 的系统级设计中的等效性检查
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
M. Fujita
中科院分区：
文献类型：
--
作者：
T. Sakunkonchak;Takeshi Matsumoto;H. Saito;S. Komatsu;M. Fujita
在系统级设计中，由于许多增量改进应用于设计，因此应该应用每个改进之间的等效性检查。然而，证明两个并发设计是否等效是一项困难的任务，更不用说并发设计本身可能容易出错。本文提出了一种基于c语言的系统级设计描述的等价性检验方法。在对并发行为进行排序之前，我们需要检查设计必须既不包含死锁也不包含竞争条件。序列化后，通过符号仿真进行等价性检验。为了证明我们的方法可以应用于实际设计，我们用加州大学欧文分校（UCI）开发的一些spec设计进行了实验。结果表明，该方法是可行的。虽然一些设计的规模较大，但通过启发式的并发和同步搜索，设计的规模相应减小，从而可以对顺序化的设计进行等价性检查。
In system-level designs, since many incremental refinements are applied to the designs, equivalence checking between each refinement should be applied. However, proving whether two concurrent designs are equivalent is a difficult task, not to mention that the concurrent design itself can be error-prone. In this paper, we propose an equivalence checking method for C-based descriptions of system-level designs by sequentializing the concurrent behaviors. Before sequentializing concurrent behaviors, we need to check that the design must not contain neither deadlock nor race condition. After the sequentialization, equivalence checking is performed by symbolic simulation. To show that our methodology can be applied to practical designs, we experiment with some SpecC designs developed by University of California Irvine (UCI). The results show that the proposed method is promising. Although the size of some designs are large, with heuristic search for concurrency and synchronization, the size of designs are reduced accordingly and hence we can perform equivalence checking with the sequentialized ones.
使用 ILP 求解器进行系统级设计的同步验证
DOI：
--
发表时间：
2006
期刊：
IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences E89-A・12
影响因子：
--
作者：
T.Sakunkonchak;S.Komatsu;M.Fujita
通讯作者：
M.Fujita