|
| 1 | +# Automatic reg as intermediate value in always @(*) |
| 2 | +# The result must be provably equivalent to the direct expression. |
| 3 | +# No latch or DFF must be created for tmp. |
| 4 | +design -reset |
| 5 | +read_verilog -sv <<EOF |
| 6 | +module t1(input a, b, c, output reg y); |
| 7 | + always @(*) begin : blk |
| 8 | + automatic reg tmp; |
| 9 | + tmp = a ^ b; |
| 10 | + if (c) tmp = tmp & a; |
| 11 | + y = tmp; |
| 12 | + end |
| 13 | + // equivalent to: y = c ? ((a^b)&a) : (a^b) |
| 14 | + assert property (y === (c ? ((a ^ b) & a) : (a ^ b))); |
| 15 | +endmodule |
| 16 | +EOF |
| 17 | +proc |
| 18 | +async2sync |
| 19 | +# no state elements for tmp |
| 20 | +select -assert-none t:$dff t:$dlatch %% |
| 21 | +sat -verify -prove-asserts -show-all |
| 22 | + |
| 23 | +# automatic logic in always_comb with chained computation |
| 24 | +# Two automatic intermediates used in sequence; result must match |
| 25 | +# the direct expression. No latch/DFF. |
| 26 | +design -reset |
| 27 | +read_verilog -sv <<EOF |
| 28 | +module t2(input [3:0] a, b, input sel, output reg [3:0] y, output reg co); |
| 29 | + always_comb begin : blk |
| 30 | + automatic reg [4:0] sum; |
| 31 | + automatic reg [3:0] pick; |
| 32 | + sum = {1'b0, a} + {1'b0, b}; |
| 33 | + pick = sel ? sum[3:0] : (a & b); |
| 34 | + y = pick; |
| 35 | + co = sum[4]; |
| 36 | + end |
| 37 | + assert property (y === (sel ? ((a + b) & 4'hf) : (a & b))); |
| 38 | + assert property (co === (((5'(a) + 5'(b)) >> 4) & 1'b1)); |
| 39 | +endmodule |
| 40 | +EOF |
| 41 | +proc |
| 42 | +async2sync |
| 43 | +select -assert-none t:$dff t:$dlatch %% |
| 44 | +sat -verify -prove-asserts -show-all |
| 45 | + |
| 46 | +# automatic in a clocked block — only the explicitly registered |
| 47 | +# output (result) must get a DFF; the automatic temp must not. |
| 48 | +design -reset |
| 49 | +read_verilog -sv <<EOF |
| 50 | +module t3(input clk, rst, input [7:0] data, output reg [7:0] result); |
| 51 | + always @(posedge clk) begin : compute |
| 52 | + automatic reg [7:0] tmp; |
| 53 | + tmp = data ^ 8'hA5; |
| 54 | + if (rst) |
| 55 | + result <= 8'h00; |
| 56 | + else |
| 57 | + result <= tmp; |
| 58 | + end |
| 59 | +endmodule |
| 60 | +EOF |
| 61 | +proc |
| 62 | +# Exactly one DFF (for result), zero latches, no DFF for tmp |
| 63 | +select -assert-count 1 t:$dff %% |
| 64 | +select -assert-none t:$dlatch %% |
| 65 | + |
| 66 | +# automatic integer in named block — ensure integer-width |
| 67 | +# automatic variables work and produce no state elements. |
| 68 | +design -reset |
| 69 | +read_verilog -sv <<EOF |
| 70 | +module t4(input [7:0] a, b, input sub, output reg [7:0] y); |
| 71 | + always @(*) begin : arith |
| 72 | + automatic integer acc; |
| 73 | + if (sub) |
| 74 | + acc = $signed(a) - $signed(b); |
| 75 | + else |
| 76 | + acc = $signed(a) + $signed(b); |
| 77 | + y = acc[7:0]; |
| 78 | + end |
| 79 | + assert property (y === (sub ? (a - b) : (a + b))); |
| 80 | +endmodule |
| 81 | +EOF |
| 82 | +proc |
| 83 | +async2sync |
| 84 | +select -assert-none t:$dff t:$dlatch %% |
| 85 | +sat -verify -prove-asserts -show-all |
| 86 | + |
| 87 | +# automatic variable not assigned on all paths (X semantics) |
| 88 | +# With 'automatic', tmp holds no previous state; the undriven path |
| 89 | +# produces X, not the old register value. After proc, no latch may be |
| 90 | +# inferred for tmp. |
| 91 | +design -reset |
| 92 | +read_verilog -sv <<EOF |
| 93 | +module t5(input en, d, output reg q); |
| 94 | + always @(*) begin : blk |
| 95 | + automatic reg tmp; |
| 96 | + if (en) tmp = d; |
| 97 | + // tmp is X when en==0: automatic means no state retention |
| 98 | + q = tmp; |
| 99 | + end |
| 100 | +endmodule |
| 101 | +EOF |
| 102 | +proc |
| 103 | +# No latch for tmp — X propagates instead of old value |
| 104 | +select -assert-none t:$dff t:$dlatch %% |
0 commit comments