From 725038d3156fe0ed6d046218e04e4228674b3f82 Mon Sep 17 00:00:00 2001 From: Emily Schmidt Date: Tue, 2 Apr 2024 11:28:54 +0100 Subject: [PATCH] Replace the 'primes' test in junit_timeout_error.sby with a new test that solves a**3 + b**3 == c**3. 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. --- tests/junit/junit_timeout_error.sby | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/tests/junit/junit_timeout_error.sby b/tests/junit/junit_timeout_error.sby index 551de49..bc7df9c 100644 --- a/tests/junit/junit_timeout_error.sby +++ b/tests/junit/junit_timeout_error.sby @@ -17,26 +17,25 @@ solver: smtbmc foo [script] read -noverific syntax: read -define SYNTAX_ERROR -read -sv primes.sv -prep -top primes +read -sv diophantine.sv +prep -top diophantine -[file primes.sv] -module primes; - parameter [8:0] offset = 7; - (* anyconst *) reg [8:0] prime1; - wire [9:0] prime2 = prime1 + offset; - (* allconst *) reg [4:0] factor; +[file diophantine.sv] +module diophantine; + (* anyconst *) reg [15:0] a, b, c; -`ifdef SYNTAX_ERROR + `ifdef SYNTAX_ERROR foo -`endif + `endif + + wire [48:0] x = a*a*a + b*b*b; + wire [48:0] y = c*c*c; always @* begin - if (1 < factor && factor < prime1) - assume ((prime1 % factor) != 0); - if (1 < factor && factor < prime2) - assume ((prime2 % factor) != 0); - assume (1 < prime1); + assume (a > 0); + assume (b > 0); + assume (c > 0); + assume (x == y); cover (1); end endmodule