1

I've been trying to verify equivalence property between two circuits in Chalmers Lava. I have declared a type bit:

type Bit = Signal Bool

And I have two circuits each has a list of bits as input and a tuple of lists of bits, and a function that checks their equivalence:

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

These two circuits take inputs as lists of 64 elements. I was able to simulate them with one input using simulate, ans simulate them with multiple using simulateSeq, but for the hole domain i wasn't able and I got this error: 

<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

(in line 7 i have the type declaration)

Also for the propEquiv, I can simulate it, but I couldn't verify it using satzoo, and i got this error: 

*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>

I counldn't understand both of them neither find anything when searching on the web, can someone help me with this? i tried to define the circuits with 64 elemnts in stand of a list , but it didn't work.

Regards.

Cactus
  • 27,075
  • 9
  • 69
  • 149
Balkis
  • 103
  • 7
  • 1
    There's no good way to fix the first error; indeed, a `[Bit]` is not finite. You'll have to rethink your approach. The second error is easier; define an instance `Fresh a => Fresh [a]` – user2407038 Feb 14 '18 at 13:11
  • Can you tighten the type of `circuit1` and `circuit2` to express the fact that they both require 64 `Bit`s of input, not an arbitrary number? E.g. using [`vector-sized`](https://hackage.haskell.org/package/vector-sized)? Then it shouldn't be too difficult to make an `instance (Finite a, KnownNat n) => Finite (Vector n a)`. – Cactus Aug 02 '18 at 02:32
  • @Cactus yes that' what I am trying to do, as I am not familier with Haskell, I couln't figure out what was the problem when I use vector.sized. Thank you for your response. – Balkis Nov 15 '18 at 08:17

0 Answers0