Larger N for input but less time used

Users
1

Hi everyone,
I came across something quite interesting while verifying two adders using EQY. I observed that when N=7168, which is larger than N=7040, the verification time dropped significantly instead of increasing. Intuitively, as N increases, the circuit becomes more complex, so we would expect the checking time to increase as well. But in this case, even though N increased, the verification time actually decreased. Does anyone know what happened?

Here, N refers to the bit-width of the adder — that is, the number of bits of the two inputs being added.

In addition, I also showed the number of gates in each implementation.

image
image854×666 12.1 KB

2

There’s no clear reason why EQY would show this behavior but generally it’s not surprising for the runtime to change somewhat chaotically when the input circuits or config changes. I’m not sure whether that alone could explain the drop in verification time, though, how long does it take to verify each of the two adders? It would help if you could share your design and/or the log oututs, since without knowing more about the circuits and config you’re running EQY with and without seeing EQY’s log output, it’s not really possible to tell whether there’s anything more going on here.

3

Sure! Sorry I just saw this message. Here are the adder and EQY script I’m using. In addition, I drew a graph of the runtime. What’s more interesting, I tried many times and the graph is very similar. I mean the spike of runtime appears in certain data width. X-axis is data width, y is runtime in second.

module adder1 #(

parameter N = 7168

)(

input  \[N-1:0\] a,

input  \[N-1:0\] b,

input          cin,

output \[N-1:0\] sum,

output         cout

);

assign {cout, sum} = a + b + cin;

endmodule

//—————————————————————————//

module adder2 #(

parameter N = 7168

)(

input  \[N-1:0\] a,

input  \[N-1:0\] b,

input          cin,

output \[N-1:0\] sum,

output         cout

);

wire \[N:0\] carry;

assign carry\[0\] = cin;

genvar i;

generate

    for (i = 0; i < N; i = i + 1) begin : full_adder_stage

        assign sum\[i\]     = a\[i\] ^ b\[i\] ^ carry\[i\];

        assign carry\[i+1\] = (a\[i\] & b\[i\]) | (a\[i\] & carry\[i\]) | (b\[i\] & carry\[i\]);

    end

endgenerate

assign cout = carry\[N\];

endmodule

//————————————————————————–//

[gold]
read_verilog adder1.v
rename adder1 top
prep -top top
stat

[gate]
read_verilog adder2.v
rename adder2 top
prep -top top
stat

[partition *]
amend *

[strategy simple]
use sat
depth 10

image
image2553×770 52.2 KB

4

That’s to be expected. Formal verification runtimes can be very chaotic, SMT solver runtimes on bounded inputs can explode as they’re based on kind of opportunistic heuristics. The general problem they’re based on is famously computationally difficult, meaning the time to solve an instance just a tiny bit larger can suddenly take far more effort for any solver

EDIT: Yes, a larger instance can even take a shorter amount of time, since the unpredictable exploration of possible solutions can happen to notice some pattern. I expect that all of the solution times account for many orders of magnitudes less work than the worst cases of SAT problem instances of the same size with the given solver. Some just happen to work out better or worse

5

Thank you so much of it. I’m very confused of it.