[RTL] Synthesis optimization barriers for DCLS

design/el2_veer_lockstep.sv

@@ -401,8 +401,26 @@ module el2_veer_lockstep
   veer_outputs_t delayed_main_core_outputs;
   veer_outputs_t shadow_core_outputs;
 
-  assign shadow_core_inputs = delay_input_d[LockstepDelayPipeStages];
-  assign delayed_main_core_outputs = delay_output_d[LockstepDelayPipeStages];
+  // Insert optimization barriers (el2_prim_buf) at the shadow-core IOs so that
+  // synthesis tools cannot prove the shadow core / comparison redundant and
+  // optimize them away.
+  veer_inputs_t  shadow_core_inputs_pre;
+  veer_outputs_t delayed_main_core_outputs_pre;
+  assign shadow_core_inputs_pre        = delay_input_d[LockstepDelayPipeStages];
+  assign delayed_main_core_outputs_pre = delay_output_d[LockstepDelayPipeStages];
+
+  el2_prim_buf #(
+    .Width($bits(veer_inputs_t))
+  ) u_shadow_inputs_buf (
+      .in_i (shadow_core_inputs_pre),
+      .out_o(shadow_core_inputs)
+  );
+  el2_prim_buf #(
+    .Width($bits(veer_outputs_t))
+  ) u_main_outputs_buf (
+      .in_i (delayed_main_core_outputs_pre),
+      .out_o(delayed_main_core_outputs)
+  );
 
   // Capture input
   assign main_core_inputs.rst_vec = rst_vec;

design/flist

@@ -44,6 +44,8 @@ $RV_ROOT/design/dmi/dmi_jtag_to_core_sync.v
 $RV_ROOT/design/dmi/rvjtag_tap.v
 $RV_ROOT/design/lib/el2_lib.sv
 $RV_ROOT/design/lib/el2_mem_if.sv
+$RV_ROOT/design/lib/el2_prim_generic_buf.sv
+$RV_ROOT/design/lib/el2_prim_buf.sv
 -v $RV_ROOT/design/lib/beh_lib.sv
 -v $RV_ROOT/design/lib/mem_lib.sv
 $RV_ROOT/design/lib/ahb_to_axi4.sv

design/flist.formal

@@ -64,6 +64,8 @@ $RV_ROOT/design/dmi/dmi_jtag_to_core_sync.v
 $RV_ROOT/design/dmi/rvjtag_tap.v
 $RV_ROOT/design/lib/el2_lib.sv
 $RV_ROOT/design/lib/el2_mem_if.sv
+$RV_ROOT/design/lib/el2_prim_generic_buf.sv
+$RV_ROOT/design/lib/el2_prim_buf.sv
 $RV_ROOT/design/lib/beh_lib.sv
 $RV_ROOT/design/lib/mem_lib.sv
 $RV_ROOT/design/lib/ahb_to_axi4.sv

design/flist.lint

@@ -10,6 +10,8 @@ $RV_ROOT/design/lib/el2_assert.sv
 $RV_ROOT/design/el2_mubi_pkg.sv
 $RV_ROOT/design/el2_veer_wrapper.sv
 $RV_ROOT/design/lib/el2_mem_if.sv
+$RV_ROOT/design/lib/el2_prim_generic_buf.sv
+$RV_ROOT/design/lib/el2_prim_buf.sv
 $RV_ROOT/design/el2_mem.sv
 $RV_ROOT/design/el2_pic_ctrl.sv
 $RV_ROOT/design/el2_veer.sv

design/flist.questa

@@ -62,6 +62,8 @@ $RV_ROOT/design/dmi/dmi_jtag_to_core_sync.v
 $RV_ROOT/design/dmi/rvjtag_tap.v
 $RV_ROOT/design/lib/el2_lib.sv
 $RV_ROOT/design/lib/el2_mem_if.sv
+$RV_ROOT/design/lib/el2_prim_generic_buf.sv
+$RV_ROOT/design/lib/el2_prim_buf.sv
 $RV_ROOT/design/lib/beh_lib.sv
 $RV_ROOT/design/lib/mem_lib.sv
 $RV_ROOT/design/lib/ahb_to_axi4.sv

design/lib/el2_prim_buf.sv

@@ -0,0 +1,18 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+// Standalone default. Integrators (e.g. Caliptra) redirect this to their own
+// barrier primitive by defining RV_PRIM_BUF_IMPL (same Width/in_i/out_o interface).
+`ifndef RV_PRIM_BUF_IMPL
+  `define RV_PRIM_BUF_IMPL el2_prim_generic_buf
+`endif
+
+module el2_prim_buf #(
+  parameter int Width = 1
+) (
+  input        [Width-1:0] in_i,
+  output logic [Width-1:0] out_o
+);
+  `RV_PRIM_BUF_IMPL #(.Width(Width)) u_impl (.in_i(in_i), .out_o(out_o));
+endmodule

design/lib/el2_prim_generic_buf.sv

@@ -0,0 +1,28 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+// Generic optimization-barrier buffer that is the default implementation
+// behind el2_prim_buf.
+//
+// WARNING: This is a plain functional buffer. It is NOT constrained for
+// synthesis - it carries no keep / size_only / dont_touch attribute. As
+// shipped, a synthesis tool MAY optimize this buffer away.
+//
+// Integrators targeting silicon (or FI/safety hardening) MUST either:
+//   * constrain this module in their synthesis flow or
+//   * override RV_PRIM_BUF_IMPL with an already-constrained primitive
+//     (e.g. caliptra_prim_buf).
+
+module el2_prim_generic_buf #(
+  parameter int Width = 1
+) (
+  input        [Width-1:0] in_i,
+  output logic [Width-1:0] out_o
+);
+
+  logic [Width-1:0] inv;
+  assign inv = ~in_i;
+  assign out_o = ~inv;
+
+endmodule

docs/source/dual-core-lock-step.md

@@ -1183,6 +1183,33 @@ There are two configuration options:
 
 The configuration options are ignored and their macros are not generated if the Dual Core Lockstep feature is disabled.
 
+## Synthesis: optimization barriers (`el2_prim_buf`)
+
+For the DCLS to be effective, the Shadow Core and the Main/Shadow comparison logic must *not* be merged or removed by synthesis.
+Logic-equivalence-aware tools can otherwise recognize the Shadow Core as redundant duplicate logic and optimize it away.
+
+To prevent this, `el2_veer_lockstep` inserts optimization barriers (`el2_prim_buf`) on the IOs of the Shadow Core:
+
+* the Shadow Core input bus (`shadow_core_inputs`),
+* the delayed Main Core outputs used in the comparison (`delayed_main_core_outputs`).
+
+The register-file comparison (when `lockstep_regfile_enable=1`) is covered by the `shadow_core_inputs` barrier: the Shadow Core's internal register file is driven from the buffered inputs, so the comparison cannot be proven constant and optimized away.
+
+`el2_prim_buf` is an abstract wrapper that selects its implementation through the `RV_PRIM_BUF_IMPL` macro.
+By default, it resolves to `el2_prim_generic_buf`, which is a plain buffer provided such that the core builds and simulates standalone.
+
+**Warning**
+The default `el2_prim_generic_buf` shipped in this repository is **functionally** a buffer but is **not constrained for synthesis**, i.e., it carries no `keep` / `size_only` / `dont_touch` attribute.
+With the generic buffer alone, a synthesis tool is free to optimize the barrier - and therefore the redundant Shadow Core and comparison logic it protects - away.
+
+An integrator targeting silicon (or fault-injection / safety hardening) **must** do one of the following:
+
+* Apply the appropriate synthesis constraints to `el2_prim_generic_buf` in their flow (e.g. `size_only` or `KEEP` / `DONT_TOUCH` in) so the buffer survives optimization; **or**
+* Override `RV_PRIM_BUF_IMPL` to point at a primitive that already carries those constraints. For example, Caliptra builds pass `+define+RV_PRIM_BUF_IMPL=caliptra_prim_buf`, whose generic/Xilinx implementations are constrained `size_only` / `keep` by the Caliptra synthesis flow.
+
+Failing to do either leaves the DCLS protection unverified against logic-optimization removal.
+```
+
 ## Validation Plan
 
 The DCLS feature will be tested within:

verification/block/config.vlt

@@ -82,7 +82,7 @@ lint_off -rule BLKSEQ -file "*/beh_lib.sv" -lines 783
 lint_off -rule SYNCASYNCNET -file "*/el2_veer.sv" -lines 41
 
 // Unused clocks from shadow core
-lint_off -rule PINCONNECTEMPTY -file "*/el2_veer_lockstep.sv" -lines 797-798
+lint_off -rule PINCONNECTEMPTY -file "*/el2_veer_lockstep.sv" -lines 815-816
 
 // Logic that might be not optimal for event based model used by Verilator
 lint_off -rule UNOPTFLAT -file "*/axi4_to_ahb.sv"

verification/block/dcls/Makefile

@@ -67,6 +67,8 @@ VERILOG_SOURCES  = \
 	${SRCDIR}/lib/el2_lib.sv \
 	${SRCDIR}/lib/axi4_to_ahb.sv \
 	${SRCDIR}/lib/ahb_to_axi4.sv \
+	${SRCDIR}/lib/el2_prim_generic_buf.sv \
+	${SRCDIR}/lib/el2_prim_buf.sv \
 	$(SRCDIR)/el2_lockstep_pkg.sv \
 	$(SRCDIR)/el2_veer_lockstep.sv \
 	$(TEST_DIR)/el2_veer_lockstep_cov_if.sv \