diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/proc/proc_rom.ys | 43 | ||||
| -rw-r--r-- | tests/sva/sva_value_change_changed_wide.sv | 22 | ||||
| -rw-r--r-- | tests/sva/sva_value_change_sim.sv | 23 |
3 files changed, 86 insertions, 2 deletions
diff --git a/tests/proc/proc_rom.ys b/tests/proc/proc_rom.ys new file mode 100644 index 000000000..c854e732f --- /dev/null +++ b/tests/proc/proc_rom.ys @@ -0,0 +1,43 @@ +read_verilog << EOT + +module top(input [3:0] a, input en, output [7:0] d); + +always @* + if (en) + case(a) + 4'h0: d <= 8'h12; + 4'h1: d <= 8'h34; + 4'h2: d <= 8'h56; + 4'h3: d <= 8'h78; + 4'h4: d <= 8'h9a; + 4'h5: d <= 8'hbc; + 4'h6: d <= 8'hde; + 4'h7: d <= 8'hff; + 4'h8: d <= 8'h61; + 4'h9: d <= 8'h49; + 4'ha: d <= 8'h36; + 4'hb: d <= 8'h81; + 4'hc: d <= 8'h8c; + 4'hd: d <= 8'ha9; + 4'he: d <= 8'h99; + 4'hf: d <= 8'h51; + endcase + else + d <= 0; + +endmodule + +EOT + +hierarchy -auto-top + +design -save orig +proc +memory +opt_dff +design -stash postopt +design -load orig +proc -norom +design -stash preopt + +equiv_opt -assert -run prepare: dummy diff --git a/tests/sva/sva_value_change_changed_wide.sv b/tests/sva/sva_value_change_changed_wide.sv new file mode 100644 index 000000000..c9147c4f3 --- /dev/null +++ b/tests/sva/sva_value_change_changed_wide.sv @@ -0,0 +1,22 @@ +module top ( + input clk, + input [2:0] a, + input [2:0] b +); + default clocking @(posedge clk); endclocking + + assert property ( + $changed(a) + ); + + assert property ( + $changed(b) == ($changed(b[0]) || $changed(b[1]) || $changed(b[2])) + ); + +`ifndef FAIL + assume property ( + a !== 'x ##1 $changed(a) + ); +`endif + +endmodule diff --git a/tests/sva/sva_value_change_sim.sv b/tests/sva/sva_value_change_sim.sv index 80ff309cd..92fe30b23 100644 --- a/tests/sva/sva_value_change_sim.sv +++ b/tests/sva/sva_value_change_sim.sv @@ -7,6 +7,8 @@ reg [7:0] counter = 0; reg a = 0; reg b = 1; reg c; +reg [2:0] wide_a = 3'b10x; +reg [2:0] wide_b = 'x; wire a_fell; assign a_fell = $fell(a, @(posedge clk)); wire a_rose; assign a_rose = $rose(a, @(posedge clk)); @@ -20,6 +22,9 @@ wire c_fell; assign c_fell = $fell(c, @(posedge clk)); wire c_rose; assign c_rose = $rose(c, @(posedge clk)); wire c_stable; assign c_stable = $stable(c, @(posedge clk)); +wire wide_a_stable; assign wide_a_stable = $stable(wide_a, @(posedge clk)); +wire wide_b_stable; assign wide_b_stable = $stable(wide_b, @(posedge clk)); + always @(posedge clk) begin counter <= counter + 1; @@ -28,13 +33,20 @@ always @(posedge clk) begin assert property ( $fell(a) && !$rose(a) && !$stable(a)); assert property (!$fell(b) && $rose(b) && !$stable(b)); assert property (!$fell(c) && !$rose(c) && $stable(c)); + assert property (!$stable(wide_a)); + assert property ($stable(wide_b)); a <= 1; b <= 1; c <= 1; end - 1: begin a <= 0; b <= 1; c <= 'x; end + 1: begin + a <= 0; b <= 1; c <= 'x; + wide_a <= 3'b101; wide_b <= 3'bxx0; + end 2: begin assert property ( $fell(a) && !$rose(a) && !$stable(a)); assert property (!$fell(b) && !$rose(b) && $stable(b)); assert property (!$fell(c) && !$rose(c) && !$stable(c)); + assert property (!$stable(wide_a)); + assert property (!$stable(wide_b)); a <= 0; b <= 0; c <= 0; end 3: begin a <= 0; b <= 1; c <= 'x; end @@ -42,9 +54,16 @@ always @(posedge clk) begin assert property (!$fell(a) && !$rose(a) && $stable(a)); assert property (!$fell(b) && $rose(b) && !$stable(b)); assert property (!$fell(c) && !$rose(c) && !$stable(c)); + assert property ($stable(wide_a)); + assert property ($stable(wide_b)); a <= 'x; b <= 'x; c <= 'x; + wide_a <= 'x; wide_b <= 'x; + end + 5: begin + a <= 0; b <= 1; c <= 'x; + wide_a <= 3'b10x; wide_b <= 'x; + counter <= 0; end - 5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end endcase; end |