Random Interleaver and Design Verifier

Hello,

I'm trying to model something in Simulink and have it verified with Design Verifier. I am very confused by what I can get DV to prove.

The example I provided may not be minimal but still the property gets proven.

On the upper part, we have a 1:32 array that gets randomly permuted and then fed back to the interleaver. On the bottom part, we start with a fresh 1:32 array and then permute using a second interleaver. The two interleavers have different seeds.

The property seems to hold when running simulations but I would expect the property to not be true for Design Verifier (and no counter examples provided). Does someone know what's going on or if there's a way to access what's being sent to the prover ?

[Adam Whitmill]

Hello Romain, There is no free inport to make any extraction here. Replacing the constant with an inport with port dimensions of 32 gave a falsified result and a counter example. I think possibly with no free import, Design verifier is just running the simulation and basing the analysis result on that simulation run.