diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index d9eb51a9c..65af26132 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -403,6 +403,18 @@ struct AST_INTERNAL::ProcessGenerator
 				if (GetSize(syncrule->signal) != 1)
 					always->input_error("Found posedge/negedge event on a signal that is not 1 bit wide!\n");
 				addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true);
+				// Automatic (nosync) variables must not become flip-flops: remove
+				// them from clocked sync rules so that proc_dff does not infer
+				// an unnecessary register for a purely combinational temporary.
+				syncrule->actions.erase(
+					std::remove_if(syncrule->actions.begin(), syncrule->actions.end(),
+						[](const RTLIL::SigSig &ss) {
+							for (auto &chunk : ss.first.chunks())
+								if (chunk.wire && chunk.wire->get_bool_attribute(ID::nosync))
+									return true;
+							return false;
+						}),
+					syncrule->actions.end());
 				proc->syncs.push_back(syncrule);
 			}
 		if (proc->syncs.empty()) {
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 684727d5b..148a6cc63 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -84,7 +84,7 @@
 			int current_function_or_task_port_id;
 			std::vector<char> case_type_stack;
 			bool do_not_require_port_stubs;
-			bool current_wire_rand, current_wire_const;
+			bool current_wire_rand, current_wire_const, current_wire_automatic;
 			bool current_modport_input, current_modport_output;
 			bool default_nettype_wire = true;
 			std::istream* lexin;
@@ -958,14 +958,18 @@ delay:
 	non_opt_delay | %empty;
 
 io_wire_type:
-	{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; }
+	{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; }
 	wire_type_token_io wire_type_const_rand opt_wire_type_token wire_type_signedness
 	{ $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); };
 
 non_io_wire_type:
-	{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; }
-	wire_type_const_rand wire_type_token wire_type_signedness
-	{ $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); };
+	{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; }
+	opt_lifetime wire_type_const_rand wire_type_token wire_type_signedness
+	{
+		if (extra->current_wire_automatic)
+			extra->astbuf3->set_attribute(ID::nosync, AstNode::mkconst_int(extra->astbuf3->location, 1, false));
+		$$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$);
+	};
 
 wire_type:
 	io_wire_type { $$ = std::move($1); }  |
@@ -1253,6 +1257,10 @@ opt_automatic:
 	TOK_AUTOMATIC |
 	%empty;
 
+opt_lifetime:
+	TOK_AUTOMATIC { extra->current_wire_automatic = true; } |
+	%empty;
+
 task_func_args_opt:
 	TOK_LPAREN TOK_RPAREN | %empty | TOK_LPAREN {
 		extra->albuf = nullptr;
diff --git a/tests/verilog/automatic_lifetime.ys b/tests/verilog/automatic_lifetime.ys
new file mode 100644
index 000000000..84e21e088
--- /dev/null
+++ b/tests/verilog/automatic_lifetime.ys
@@ -0,0 +1,104 @@
+#   Automatic reg as intermediate value in always @(*)
+#   The result must be provably equivalent to the direct expression.
+#   No latch or DFF must be created for tmp.
+design -reset
+read_verilog -sv <<EOF
+module t1(input a, b, c, output reg y);
+    always @(*) begin : blk
+        automatic reg tmp;
+        tmp = a ^ b;
+        if (c) tmp = tmp & a;
+        y = tmp;
+    end
+    // equivalent to: y = c ? ((a^b)&a) : (a^b)
+    assert property (y === (c ? ((a ^ b) & a) : (a ^ b)));
+endmodule
+EOF
+proc
+async2sync
+# no state elements for tmp
+select -assert-none t:$dff t:$dlatch %%
+sat -verify -prove-asserts -show-all
+
+#   automatic logic in always_comb with chained computation
+#   Two automatic intermediates used in sequence; result must match
+#   the direct expression.  No latch/DFF.
+design -reset
+read_verilog -sv <<EOF
+module t2(input [3:0] a, b, input sel, output reg [3:0] y, output reg co);
+    always_comb begin : blk
+        automatic reg [4:0] sum;
+        automatic reg [3:0] pick;
+        sum  = {1'b0, a} + {1'b0, b};
+        pick = sel ? sum[3:0] : (a & b);
+        y  = pick;
+        co = sum[4];
+    end
+    assert property (y  === (sel ? ((a + b) & 4'hf) : (a & b)));
+    assert property (co === (((5'(a) + 5'(b)) >> 4) & 1'b1));
+endmodule
+EOF
+proc
+async2sync
+select -assert-none t:$dff t:$dlatch %%
+sat -verify -prove-asserts -show-all
+
+#   automatic in a clocked block — only the explicitly registered
+#   output (result) must get a DFF; the automatic temp must not.
+design -reset
+read_verilog -sv <<EOF
+module t3(input clk, rst, input [7:0] data, output reg [7:0] result);
+    always @(posedge clk) begin : compute
+        automatic reg [7:0] tmp;
+        tmp = data ^ 8'hA5;
+        if (rst)
+            result <= 8'h00;
+        else
+            result <= tmp;
+    end
+endmodule
+EOF
+proc
+# Exactly one DFF (for result), zero latches, no DFF for tmp
+select -assert-count 1 t:$dff %%
+select -assert-none t:$dlatch %%
+
+#   automatic integer in named block — ensure integer-width
+#   automatic variables work and produce no state elements.
+design -reset
+read_verilog -sv <<EOF
+module t4(input [7:0] a, b, input sub, output reg [7:0] y);
+    always @(*) begin : arith
+        automatic integer acc;
+        if (sub)
+            acc = $signed(a) - $signed(b);
+        else
+            acc = $signed(a) + $signed(b);
+        y = acc[7:0];
+    end
+    assert property (y === (sub ? (a - b) : (a + b)));
+endmodule
+EOF
+proc
+async2sync
+select -assert-none t:$dff t:$dlatch %%
+sat -verify -prove-asserts -show-all
+
+#   automatic variable not assigned on all paths (X semantics)
+#   With 'automatic', tmp holds no previous state; the undriven path
+#   produces X, not the old register value.  After proc, no latch may be
+#   inferred for tmp.
+design -reset
+read_verilog -sv <<EOF
+module t5(input en, d, output reg q);
+    always @(*) begin : blk
+        automatic reg tmp;
+        if (en) tmp = d;
+        // tmp is X when en==0: automatic means no state retention
+        q = tmp;
+    end
+endmodule
+EOF
+proc
+# No latch for tmp — X propagates instead of old value
+select -assert-none t:$dff t:$dlatch %%