Specman e中用Keep复制列表：是否有更简洁的单行实现方式？

你当前用两行keep语句实现了复制已生成列表的逻辑，其实有更简洁的实现方式，完全可以用单行keep语句搞定：

原实现代码 #

<'
struct A {
    ListA : list of uint;
    keep ListA.size() == 5;
    keep ListA.sum(it) <= 20;
};

struct B {
    ListB : list of uint;
};

extend sys {
    A1 : A;
    B1 : B;

    // Keeps
    keep B1.ListB.size() == read_only(A1.ListA.size());
    keep for each in B1.ListB {
        it == read_only(A1.ListA[index]);
    };
};
'>

简洁实现 #

直接让B1.ListB等于read_only(A1.ListA)即可，这一行约束会同时保证列表长度一致、每个位置的元素完全相同：

<'
struct A {
    ListA : list of uint;
    keep ListA.size() == 5;
    keep ListA.sum(it) <= 20;
};

struct B {
    ListB : list of uint;
};

extend sys {
    A1 : A;
    B1 : B;

    // 单行完成复制逻辑
    keep B1.ListB == read_only(A1.ListA);
};
'>

这种写法和你原来的两行约束逻辑完全等价，Specman e的列表相等约束会自动检查两个列表的长度是否一致，并且逐个位置比较元素值，省去了手动遍历和长度检查的冗余代码。

内容的提问来源于stack exchange，提问作者Ank