Refactor cdc_2phase_clearable clock domains

formal/cc_cdc_reset_ctrlr_half_properties.sv

@@ -89,13 +89,17 @@ module cc_cdc_reset_ctrlr_half_properties #(
 
   logic init_q = 1'b0;
 
+  // Reset modeling: force the first sampled cycle into reset so the proof starts
+  // from a reachable reset-controller half state.
   always_ff @(posedge clk_i) begin
     init_q <= 1'b1;
     if (!init_q) begin
       assume (!rst_ni);
     end
   end
 
+  // Combinational contract: These checks tie the public clear/isolate
+  // outputs to the initiator/receiver halves and validate receiver phase decode.
   always_comb begin
     if (!rst_ni) begin
       if (CLEAR_ON_ASYNC_RESET) begin
@@ -180,6 +184,8 @@ module cc_cdc_reset_ctrlr_half_properties #(
     end
   end
 
+  // Sequential local-state checks. These assert the output contract of each
+  // initiator state and require stalled receiver phases to stay stable.
   always_ff @(posedge clk_i) begin
     if (rst_ni && init_q) begin
       if (receiver_phase_req && !receiver_phase_ack) begin
@@ -241,6 +247,8 @@ module cc_cdc_reset_ctrlr_half_properties #(
       end
     end
 
+    // Initiator transition relation: the next state must match the previous
+    // clear request, phase-CDC acknowledgement, and local isolate/clear ack.
     if (rst_ni && $past(rst_ni) && init_q) begin
       case ($past(initiator_state_q))
         InitIdle: begin
@@ -300,6 +308,8 @@ module cc_cdc_reset_ctrlr_half_properties #(
       endcase
     end
 
+    // Cover the main local and remote clear phases
+    // so bounded runs exercise both sides of the bidirectional half.
     cover (rst_ni && initiator_state_q == InitClear);
     cover (rst_ni && initiator_state_q == InitPostClear);
     cover (rst_ni && receiver_phase_q == PhaseClear);

formal/cc_cdc_reset_ctrlr_properties.sv

@@ -69,6 +69,8 @@ module cc_cdc_reset_ctrlr_composed_harness (
     .b_isolate_ack_i ( b_isolate_ack_q )
   );
 
+  // Each clock domain is independently initialized in reset, then held out of
+  // reset so the proof focuses on the synchronous clear sequence.
   always_ff @(posedge a_clk_i) begin
     a_init_q <= 1'b1;
     if (!a_init_q) begin
@@ -97,6 +99,8 @@ module cc_cdc_reset_ctrlr_composed_harness (
     end
   end
 
+  // Local acknowledgement for side A: the connected CDC side reports
+  // isolate and clear completion one A-clock cycle after the request.
   always_ff @(posedge a_clk_i, negedge a_rst_ni) begin
     if (!a_rst_ni) begin
       a_isolate_ack_q <= 1'b0;
@@ -107,6 +111,8 @@ module cc_cdc_reset_ctrlr_composed_harness (
     end
   end
 
+  // Local acknowledgement for side B mirrors side A, but is sampled on the
+  // independent B clock to preserve the two-domain composition.
   always_ff @(posedge b_clk_i, negedge b_rst_ni) begin
     if (!b_rst_ni) begin
       b_isolate_ack_q <= 1'b0;
@@ -117,6 +123,8 @@ module cc_cdc_reset_ctrlr_composed_harness (
     end
   end
 
+  // Cross-domain contract: clear implies isolate locally, and any active
+  // clear on either side requires both sides to be isolated.
   always_comb begin
     if (a_rst_ni) begin
       assert (!a_clear_o || a_isolate_o);