Проверка эквивалентности с использованием Lava

Question

Я пытался проверить свойство эквивалентности между двумя цепями в 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 элементов. Я смог смоделировать их с одним входом, используя имитацию, и имитировать их с несколькими, используя simulateSeq, но для дырочной области я не смог, и я получил эту ошибку:

<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 elemnts в списке, но это не сработало.

С уважением.