矛盾软约束的行为答案

【问题标题】：Behavior of contradicting soft constraints矛盾软约束的行为
【发布时间】：2015-07-22 09:01:39
【问题描述】：

我有一个测试用例，其中的行为似乎是错误的。我看到所有世代的 num_of_red_shoes 都很高，而我希望分布更均匀。这种行为的原因是什么？如何解决？

<'
struct closet {
    kind:[SMALL,BIG];

    num_of_shoes:uint;
    num_of_red_shoes:uint;
    num_of_black_shoes:uint;
    num_of_yellow_shoes:uint;

    keep soft num_of_red_shoes < 10;
    keep soft num_of_black_shoes < 10;
    keep soft num_of_yellow_shoes < 10;

    keep num_of_yellow_shoes + num_of_black_shoes + num_of_red_shoes == num_of_shoes;

    when BIG closet {
        keep num_of_shoes in [50..100];
    };
};

extend sys {
    closets[100]:list of BIG closet;
};
'>

生成结果：

item   type        kind        num_of_sh*  num_of_re*  num_of_bl*  num_of_ye* 
---------------------------------------------------------------------------
0.     BIG closet  BIG         78          73          1           4           
1.     BIG closet  BIG         67          50          8           9           
2.     BIG closet  BIG         73          68          0           5           
3.     BIG closet  BIG         73          66          3           4           
4.     BIG closet  BIG         51          50          0           1           
5.     BIG closet  BIG         78          76          1           1           
6.     BIG closet  BIG         55          43          7           5           
7.     BIG closet  BIG         88          87          1           0           
8.     BIG closet  BIG         99          84          6           9           
9.     BIG closet  BIG         92          92          0           0           
10.    BIG closet  BIG         63          55          3           5           
11.    BIG closet  BIG         59          50          9           0           
12.    BIG closet  BIG         51          44          2           5           
13.    BIG closet  BIG         82          76          1           5           
14.    BIG closet  BIG         81          74          2           5           
15.    BIG closet  BIG         97          93          2           2           
16.    BIG closet  BIG         54          41          8           5           
17.    BIG closet  BIG         55          44          5           6           
18.    BIG closet  BIG         70          55          9           6           
19.    BIG closet  BIG         63          57          1           5

【问题讨论】：

标签： specman e

【解决方案1】：

当存在相互矛盾的软约束时，Specman 不会随机化强制执行的软约束，而是优先考虑最后写入的约束。由于 soft on red shoes 在测试中是第一个，所以它总是被覆盖。

如果已知软体是互斥的（这里不是这种情况），您可以使用一个简单的标志来随机选择应该保留的软体。例如代码如下所示：

flag:uint[0..2];

keep soft read_only(flag==0) => num_of_red_shoes < 10;
keep soft read_only(flag==1) => num_of_black_shoes < 10;
keep soft read_only(flag==2) => num_of_yellow_shoes < 10;

但是，由于这里事先不知道预计要容纳多少个软体（并且有可能满足两个或三个都满足），因此应该制定更复杂的解决方案。这是执行此随机化的代码：

struct closet {
    kind:[SMALL,BIG];

    num_of_shoes:uint;
    num_of_red_shoes:uint;
    num_of_black_shoes:uint;
    num_of_yellow_shoes:uint;

    //replaces the original soft constraints (if a flag is true the correlating
    //right-side implication will be enforced
    soft_flags[3]:list of bool;
    keep for each in soft_flags {
        soft it == TRUE;
    };

    //this list is used to shuffle the flags so their enforcement will be done
    //with even distribution
    soft_indices:list of uint;
    keep soft_indices.is_a_permutation({0;1;2});

    keep soft_flags[soft_indices[0]] => num_of_red_shoes < 10;
    keep soft_flags[soft_indices[1]] => num_of_black_shoes < 10;
    keep soft_flags[soft_indices[2]] => num_of_yellow_shoes < 10;

    keep num_of_yellow_shoes + num_of_black_shoes + num_of_red_shoes == num_of_shoes;
};

【讨论】：

【解决方案2】：

我不支持Cadence，所以我不能给你一个明确的答案。我认为求解器会尝试打破尽可能少的约束，如果找到它只会选择第一个（在你的情况下是红鞋的那个）。尝试更改顺序，看看是否会发生变化（如果首先是黑色约束，我想你总会得到更多的黑色鞋子）。

作为一种解决方案，当你有一个大壁橱时，你可以移除软约束：

when BIG closet {
    keep num_of_red_shoes.reset_soft();
    keep num_of_black_shoes.reset_soft();
    keep num_of_yellow_shoes.reset_soft();
    keep num_of_shoes in [50..100];
};

如果你想随机选择禁用哪一个（有时超过 10 只红鞋，有时超过 10 只黑鞋等），那么你需要一个辅助字段：

when BIG closet {
    more_shoes : [ RED, BLACK, YELLOW ];

    keep more_shoes == RED => num_of_red_shoes.reset_soft();
    keep more_shoes == BLACK => num_of_black_shoes.reset_soft();
    keep more_shoes == YELLOW => num_of_yellow_shoes.reset_soft();
    keep num_of_shoes in [50..100];
};

这取决于您所说的“更均匀的分布”是什么意思。

【讨论】：

【解决方案3】：

没有办法满足您对大衣柜的所有硬性和软性限制。因此，Specman 试图通过忽略一些软约束来找到解决方案。 IntelliGen 约束求解器不会忽略所有软约束，而是尝试在仍使用子集的同时找到解决方案。这在“Specman Generation 用户指南”(sn_igenuser.pdf) 中有说明：

稍后加载的 [S]oft 约束被认为具有比先前加载的软约束更高的优先级。"

在这种情况下，这意味着 Specman 放弃了对红鞋的软约束，因为它可以找到仍然遵守其他软约束的解决方案，所以它不会放弃它们。

如果您将所有软约束合并为一个，那么您可能会得到您希望的结果：

 keep soft ((num_of_red_shoes    < 10) and (num_of_black_shoes < 10) and
            (num_of_yellow_shoes < 10));

给后面的约束优先级有好处：这意味着使用 AOP 您可以添加新的软约束，它们将获得最高优先级。

【讨论】：

【解决方案4】：

对于更多分布的值，我建议如下。我相信你也可以遵循预期的逻辑。

var1, var2 : uint;
keep var1 in [0..30];
keep var2 in [0..30];

when BIG closet {
    keep num_of_shoes in [50..100];
    keep num_of_yellow_shoes == (num_of_shoes/3) - 15 + var1;
    keep num_of_black_shoes == (num_of_shoes - num_of_yellow_shoes)/2 - 15 + var2;
    keep num_of_red_shoes == num_of_shoes - (num_of_yellow_shoes - num_of_black_shoes);

keep gen (var1, var2) before (num_of_shoes);
    keep gen (num_of_shoes) before (num_of_yellow_shoes, num_of_black_shoes, num_of_red_shoes);
    keep gen (num_of_yellow_shoes) before (num_of_black_shoes, num_of_red_shoes);
    keep gen (num_of_black_shoes) before (num_of_red_shoes);
};

【讨论】：