1

我一直在尝试验证 Chalmers Lava 中两个电路之间的等效性。我已经声明了一个类型位：

type Bit = Signal Bool

我有两个电路，每个电路都有一个位列表作为输入和一个位列表元组，以及一个检查它们等价性的函数：

circuit1:: [Bit] ->([Bit],[Bit])
circuit2:: [Bit] ->([Bit],[Bit])
propEquiv input = ok
    where 
        out1 = circuit1 input 
        out2 = circuit2 input 
        ok = out1 <==> out2

这两个电路将输入作为 64 个元素的列表。我能够使用模拟用一个输入来模拟它们，并使用模拟序列用多个输入来模拟它们，但是对于孔域我无法做到，我得到了这个错误：

<interactive>:7:20:
    No instance for (Finite [Bit]) arising from a use of `domain'
    In the second argument of `simulateSeq', namely `domain'
    In the expression: simulateSeq ipSpec domain
    In an equation for `it': it = simulateSeq ipSpec domain

（在第 7 行我有类型声明）

同样对于 propEquiv，我可以模拟它，但我无法使用 satzoo 验证它，并且出现此错误：

*Main> satzoo propEquiv 
<interactive>:9:1:
    No instance for (Fresh [Bit]) arising from a use of `satzoo'
    In the expression: satzoo propEquiv
    In an equation for `it': it = satzoo propEquiv
*Main>

我不明白他们俩在网上搜索时都找不到任何东西，有人可以帮我解决这个问题吗？我试图在列表中定义具有 64 个元素的电路，但它没有用。

问候。

4

0 回答 0