mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-07 06:44:06 +00:00
Test autotune
This commit is contained in:
parent
b4458d43d7
commit
48a02f9cc4
2
tests/autotune/Makefile
Normal file
2
tests/autotune/Makefile
Normal file
|
@ -0,0 +1,2 @@
|
|||
SUBDIR=autotune
|
||||
include ../make/subdir.mk
|
85
tests/autotune/autotune_div.sby
Normal file
85
tests/autotune/autotune_div.sby
Normal file
|
@ -0,0 +1,85 @@
|
|||
[tasks]
|
||||
bmc
|
||||
cover
|
||||
prove
|
||||
|
||||
[options]
|
||||
bmc: mode bmc
|
||||
cover: mode cover
|
||||
prove: mode prove
|
||||
expect pass
|
||||
|
||||
[engines]
|
||||
smtbmc boolector
|
||||
|
||||
[script]
|
||||
read -sv autotune_div.sv
|
||||
prep -top top
|
||||
|
||||
[file autotune_div.sv]
|
||||
module top #(
|
||||
parameter WIDTH = 4 // Reduce this if it takes too long on CI
|
||||
) (
|
||||
input clk,
|
||||
input load,
|
||||
input [WIDTH-1:0] a,
|
||||
input [WIDTH-1:0] b,
|
||||
output reg [WIDTH-1:0] q,
|
||||
output reg [WIDTH-1:0] r,
|
||||
output reg done
|
||||
);
|
||||
|
||||
reg [WIDTH-1:0] a_reg = 0;
|
||||
reg [WIDTH-1:0] b_reg = 1;
|
||||
|
||||
initial begin
|
||||
q <= 0;
|
||||
r <= 0;
|
||||
done <= 1;
|
||||
end
|
||||
|
||||
reg [WIDTH-1:0] q_step = 1;
|
||||
reg [WIDTH-1:0] r_step = 1;
|
||||
|
||||
// This is not how you design a good divider circuit!
|
||||
always @(posedge clk) begin
|
||||
if (load) begin
|
||||
a_reg <= a;
|
||||
b_reg <= b;
|
||||
q <= 0;
|
||||
r <= a;
|
||||
q_step <= 1;
|
||||
r_step <= b;
|
||||
done <= b == 0;
|
||||
end else begin
|
||||
if (r_step <= r) begin
|
||||
q <= q + q_step;
|
||||
r <= r - r_step;
|
||||
|
||||
if (!r_step[WIDTH-1]) begin
|
||||
r_step <= r_step << 1;
|
||||
q_step <= q_step << 1;
|
||||
end
|
||||
end else begin
|
||||
if (!q_step[0]) begin
|
||||
r_step <= r_step >> 1;
|
||||
q_step <= q_step >> 1;
|
||||
end else begin
|
||||
done <= 1;
|
||||
end
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
always @(posedge clk) begin
|
||||
assert (r_step == b_reg * q_step); // Helper invariant
|
||||
|
||||
assert (q * b_reg + r == a_reg); // Main invariant & correct output relationship
|
||||
if (done) assert (r <= b_reg - 1); // Output range
|
||||
|
||||
cover (done);
|
||||
cover (done && b_reg == 0);
|
||||
cover (r != a_reg);
|
||||
cover (r == a_reg);
|
||||
end
|
||||
endmodule
|
3
tests/autotune/autotune_div.sh
Normal file
3
tests/autotune/autotune_div.sh
Normal file
|
@ -0,0 +1,3 @@
|
|||
#!/bin/bash
|
||||
set -e
|
||||
python3 $SBY_MAIN --autotune -f $SBY_FILE $TASK
|
50
tests/autotune/autotune_options.sby
Normal file
50
tests/autotune/autotune_options.sby
Normal file
|
@ -0,0 +1,50 @@
|
|||
[tasks]
|
||||
a
|
||||
b
|
||||
c
|
||||
d
|
||||
|
||||
[options]
|
||||
mode bmc
|
||||
expect fail
|
||||
|
||||
[engines]
|
||||
smtbmc boolector
|
||||
|
||||
[script]
|
||||
read -sv autotune_div.sv
|
||||
prep -top top
|
||||
|
||||
[autotune]
|
||||
a: timeout 60
|
||||
a: wait 10%+20
|
||||
a: parallel 1
|
||||
a: presat on
|
||||
a: incr on
|
||||
a: mem on
|
||||
a: forall on
|
||||
|
||||
b: timeout none
|
||||
b: parallel auto
|
||||
b: presat off
|
||||
b: incr off
|
||||
b: mem auto
|
||||
b: mem_threshold 20
|
||||
b: forall any
|
||||
|
||||
c: presat any
|
||||
c: incr any
|
||||
c: mem any
|
||||
c: forall auto
|
||||
|
||||
d: incr auto
|
||||
d: incr_threshold 10
|
||||
|
||||
[file autotune_div.sv]
|
||||
module top (input clk);
|
||||
reg [7:0] counter = 0;
|
||||
always @(posedge clk) begin
|
||||
counter <= counter + 1;
|
||||
assert (counter != 4);
|
||||
end
|
||||
endmodule
|
3
tests/autotune/autotune_options.sh
Normal file
3
tests/autotune/autotune_options.sh
Normal file
|
@ -0,0 +1,3 @@
|
|||
#!/bin/bash
|
||||
set -e
|
||||
python3 $SBY_MAIN --autotune -f $SBY_FILE $TASK
|
Loading…
Reference in a new issue