diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/sat/initval.v | 4 | ||||
-rw-r--r-- | tests/sat/initval.ys | 2 | ||||
-rw-r--r-- | tests/various/shregmap.ys | 33 |
3 files changed, 5 insertions, 34 deletions
diff --git a/tests/sat/initval.v b/tests/sat/initval.v index 5b661f8d6..d46ccae48 100644 --- a/tests/sat/initval.v +++ b/tests/sat/initval.v @@ -1,6 +1,7 @@ module test(input clk, input [3:0] bar, output [3:0] foo); reg [3:0] foo = 0; reg [3:0] last_bar = 0; + reg [3:0] asdf = 4'b1xxx; always @* foo[1:0] <= bar[1:0]; @@ -11,5 +12,8 @@ module test(input clk, input [3:0] bar, output [3:0] foo); always @(posedge clk) last_bar <= bar; + always @* + asdf[2:0] <= 3'b111; + assert property (foo == {last_bar[3:2], bar[1:0]}); endmodule diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..3d88aa971 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -1,4 +1,4 @@ read_verilog -sv initval.v -proc;; +proc; sat -seq 10 -prove-asserts diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys index 0e5fe882b..16e5f40e1 100644 --- a/tests/various/shregmap.ys +++ b/tests/various/shregmap.ys @@ -31,36 +31,3 @@ sat -verify -prove-asserts -show-ports -seq 5 miter #design -load gate #stat - -########## - -design -load read -design -copy-to model $__XILINX_SHREG_ -hierarchy -top shregmap_variable_test -prep -design -save gold - -simplemap t:$dff t:$dffe -shregmap -tech xilinx - -#stat -# show -width -# write_verilog -noexpr -norename -select -assert-count 1 t:$_DFF_P_ -select -assert-count 2 t:$__XILINX_SHREG_ - -design -stash gate - -design -import gold -as gold -design -import gate -as gate -design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ -prep - -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -verify -prove-asserts -show-ports -seq 5 miter - -# design -load gold -# stat - -# design -load gate -# stat |