From ff802086b4b1b9d9ca0c74fd5fa521b5316bbe4c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 18:00:52 +0200 Subject: [PATCH] test uninited FFs with const clks and fix btor script for this --- sbysrc/sby_core.py | 2 +- tests/regression/const_clocks.sby | 43 +++++++++++++++++++++++++++++++ 2 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 tests/regression/const_clocks.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 4e57b21..5580d09 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -653,7 +653,7 @@ class SbyTask(SbyConfig): print("abc", file=f) print("opt_clean", file=f) else: - print("opt -fast", file=f) + print("opt -fast -keepdc", file=f) print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) diff --git a/tests/regression/const_clocks.sby b/tests/regression/const_clocks.sby new file mode 100644 index 0000000..245358b --- /dev/null +++ b/tests/regression/const_clocks.sby @@ -0,0 +1,43 @@ +[tasks] +btor +smt +btor_m btor multiclock +smt_m smt multiclock + +[options] +mode bmc + +multiclock: multiclock on + +[engines] +#smtbmc +btor: btor btormc +smt: smtbmc boolector + +[script] +read_verilog -formal const_clocks.sv +prep -flatten -top top + +[file const_clocks.sv] +module top( + input clk, + input [7:0] d +); + + (* keep *) + wire [7:0] some_const = $anyconst; + + wire [7:0] q; + + ff ff1(.clk(1'b0), .d(d), .q(q)); + + initial assume (some_const == q); + initial assume (q != 0); + + + always @(posedge clk) assert(some_const == q); +endmodule + +module ff(input clk, input [7:0] d, (* keep *) output reg [7:0] q); + always @(posedge clk) q <= d; +endmodule -- 2.30.2