mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-05 22:14:08 +00:00
725038d315
The old test tried to find two primes that are 7 apart. It is supposed to time out after 1 second but on newer hardware the test completes too quickly. This commit replaces it with a new test that tries to find a non-trivial solution to the diophantine equation a**3 + b**3 == c**3, which is a lot more difficult.
42 lines
609 B
Plaintext
42 lines
609 B
Plaintext
[tasks]
|
|
syntax error
|
|
solver error
|
|
timeout
|
|
|
|
[options]
|
|
mode cover
|
|
depth 1
|
|
timeout: timeout 1
|
|
error: expect error
|
|
timeout: expect timeout
|
|
|
|
[engines]
|
|
~solver: smtbmc --dumpsmt2 --progress --stbv z3
|
|
solver: smtbmc foo
|
|
|
|
[script]
|
|
read -noverific
|
|
syntax: read -define SYNTAX_ERROR
|
|
read -sv diophantine.sv
|
|
prep -top diophantine
|
|
|
|
[file diophantine.sv]
|
|
module diophantine;
|
|
(* anyconst *) reg [15:0] a, b, c;
|
|
|
|
`ifdef SYNTAX_ERROR
|
|
foo
|
|
`endif
|
|
|
|
wire [48:0] x = a*a*a + b*b*b;
|
|
wire [48:0] y = c*c*c;
|
|
|
|
always @* begin
|
|
assume (a > 0);
|
|
assume (b > 0);
|
|
assume (c > 0);
|
|
assume (x == y);
|
|
cover (1);
|
|
end
|
|
endmodule
|