diff --git a/.gitignore b/.gitignore index dd68acfa..90435c3e 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,8 @@ build formal/fifo formal/counter formal/fall_through_register +formal/cdc_reset_ctrlr_half +formal/cdc_reset_ctrlr_composed *.check *.vcd obj_dir/ diff --git a/formal/Makefile b/formal/Makefile index d27b5c66..b209937d 100644 --- a/formal/Makefile +++ b/formal/Makefile @@ -1,21 +1,28 @@ -# Copyright (c) 2019 ETH Zurich, University of Bologna +# Copyright 2019 ETH Zurich and University of Bologna. # # Copyright and related rights are licensed under the Solderpad Hardware # License, Version 0.51 (the "License"); you may not use this file except in -# compliance with the License. You may obtain a copy of the License at +# compliance with the License. You may obtain a copy of the License at # http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law # or agreed to in writing, software, hardware and materials distributed under # this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR # CONDITIONS OF ANY KIND, either express or implied. See the License for the # specific language governing permissions and limitations under the License. -# Author: Robert Balas +# Authors: +# - Robert Balas +# - Philippe Sauter +# +# Description: Formal Verification Targets +# Dispatch SymbiYosys proof runs for common_cells formal properties, including +# reset-controller half and composed CDC clear-sequencing checks. YOSYS ?= yosys SBY ?= sby RM ?= rm -all: fifo.check counter.check fall_through_register.check +all: fifo.check counter.check fall_through_register.check cdc_reset_ctrlr_half.check \ + cdc_reset_ctrlr_composed.check fifo.check: fifo.sby ../src/cc_fifo.sv cc_fifo_properties.sv $(SBY) -f $< @@ -34,9 +41,24 @@ fall_through_register.check: fall_through_register.sby ../src/cc_fall_through_re $(SBY) -f $< touch $@ +cdc_reset_ctrlr_half.check: cdc_reset_ctrlr_half.sby cc_cdc_reset_ctrlr_half_properties.sv \ + ../src/cc_cdc_reset_ctrlr.sv ../src/cc_cdc_4phase.sv \ + ../src/cc_sync.sv ../src/cc_pkg.sv + ./run_cdc_reset_ctrlr_half.sh + touch $@ + +cdc_reset_ctrlr_composed.check: cdc_reset_ctrlr_composed.sby cc_cdc_reset_ctrlr_properties.sv \ + cc_cdc_reset_ctrlr_half_properties.sv \ + ../src/cc_cdc_reset_ctrlr.sv ../src/cc_cdc_4phase.sv \ + ../src/cc_sync.sv ../src/cc_pkg.sv + ./run_cdc_reset_ctrlr_composed.sh + touch $@ + .PHONY: clean clean: $(RM) -r fifo.check fifo/ # $(RM) -r delta_counter.check delta_counter/ $(RM) -r counter.check counter/ $(RM) -r fall_through_register.check fall_through_register/ + $(RM) -r cdc_reset_ctrlr_half.check cdc_reset_ctrlr_half/ + $(RM) -r cdc_reset_ctrlr_composed.check cdc_reset_ctrlr_composed/ diff --git a/formal/cc_cdc_reset_ctrlr_half_properties.sv b/formal/cc_cdc_reset_ctrlr_half_properties.sv new file mode 100644 index 00000000..ee184bcf --- /dev/null +++ b/formal/cc_cdc_reset_ctrlr_half_properties.sv @@ -0,0 +1,335 @@ +// Copyright 2026 ETH Zurich and University of Bologna. +// +// Copyright and related rights are licensed under the Solderpad Hardware +// License, Version 0.51 (the "License"); you may not use this file except in +// compliance with the License. You may obtain a copy of the License at +// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +// or agreed to in writing, software, hardware and materials distributed under +// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +// CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// Authors: +// - Philippe Sauter +// +// Description: Reset-Controller Half Properties +// Prove the local clear/isolate FSM contract of one reset-controller half, +// including phase decode, output consistency, and initiator state transitions. + +module cc_cdc_reset_ctrlr_half_properties #( + parameter logic CLEAR_ON_ASYNC_RESET = 1'b1 +)( + input wire clk_i, + input wire rst_ni, + input wire clear_i, + input wire isolate_o, + input wire isolate_ack_i, + input wire clear_o, + input wire clear_ack_i, + input wire [1:0] async_next_phase_o, + input wire async_req_o, + input wire [1:0] async_next_phase_i, + input wire async_req_i, + input wire async_ack_o, + input wire [3:0] initiator_state_q, + input wire initiator_phase_transition_ack, + input wire [1:0] initiator_clear_seq_phase, + input wire initiator_phase_transition_req, + input wire initiator_isolate_out, + input wire initiator_clear_out, + input wire [1:0] receiver_phase_q, + input wire [1:0] receiver_next_phase, + input wire receiver_phase_req, + input wire receiver_phase_ack, + input wire receiver_isolate_out, + input wire receiver_clear_out +); + + localparam logic [1:0] PhaseIdle = 2'd0; + localparam logic [1:0] PhaseIsolate = 2'd1; + localparam logic [1:0] PhaseClear = 2'd2; + localparam logic [1:0] PhasePostClear = 2'd3; + + localparam logic [3:0] InitIdle = 4'd0; + localparam logic [3:0] InitIsolate = 4'd1; + localparam logic [3:0] InitWaitIsolatePhaseAck = 4'd2; + localparam logic [3:0] InitWaitIsolateAck = 4'd3; + localparam logic [3:0] InitClear = 4'd4; + localparam logic [3:0] InitWaitClearPhaseAck = 4'd5; + localparam logic [3:0] InitWaitClearAck = 4'd6; + localparam logic [3:0] InitPostClear = 4'd7; + localparam logic [3:0] InitFinished = 4'd8; + + function automatic logic valid_phase(input logic [1:0] phase); + case (phase) + PhaseIdle, PhaseIsolate, PhaseClear, PhasePostClear: valid_phase = 1'b1; + default: valid_phase = 1'b0; + endcase + endfunction + + function automatic logic valid_initiator_state(input logic [3:0] state); + case (state) + InitIdle, + InitIsolate, + InitWaitIsolatePhaseAck, + InitWaitIsolateAck, + InitClear, + InitWaitClearPhaseAck, + InitWaitClearAck, + InitPostClear, + InitFinished: valid_initiator_state = 1'b1; + default: valid_initiator_state = 1'b0; + endcase + endfunction + + 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 + assert (initiator_state_q == InitIsolate); + end else begin + assert (initiator_state_q == InitIdle); + end + assert (receiver_phase_q == PhaseIdle); + end + + if (rst_ni) begin + assert (clear_o == (initiator_clear_out || receiver_clear_out)); + assert (isolate_o == (initiator_isolate_out || receiver_isolate_out)); + assert (!clear_o || isolate_o); + assert (!initiator_clear_out || initiator_isolate_out); + assert (!receiver_clear_out || receiver_isolate_out); + + assert (valid_initiator_state(initiator_state_q)); + assert (valid_phase(receiver_phase_q)); + + if (async_req_o) begin + assert (valid_phase(async_next_phase_o)); + end + + if (initiator_phase_transition_req) begin + assert (valid_phase(initiator_clear_seq_phase)); + end + + if (receiver_phase_req) begin + assume (valid_phase(receiver_next_phase)); + + case (receiver_next_phase) + PhaseIdle: begin + assert (!receiver_clear_out); + assert (!receiver_isolate_out); + assert (receiver_phase_ack); + end + PhaseIsolate: begin + assert (!receiver_clear_out); + assert (receiver_isolate_out); + assert (receiver_phase_ack == isolate_ack_i); + end + PhaseClear: begin + assert (receiver_clear_out); + assert (receiver_isolate_out); + assert (receiver_phase_ack == clear_ack_i); + end + PhasePostClear: begin + assert (!receiver_clear_out); + assert (receiver_isolate_out); + assert (receiver_phase_ack); + end + default: begin + end + endcase + end else begin + case (receiver_phase_q) + PhaseIdle: begin + assert (!receiver_clear_out); + assert (!receiver_isolate_out); + end + PhaseIsolate: begin + assert (!receiver_clear_out); + assert (receiver_isolate_out); + end + PhaseClear: begin + assert (receiver_clear_out); + assert (receiver_isolate_out); + end + PhasePostClear: begin + assert (!receiver_clear_out); + assert (receiver_isolate_out); + end + default: begin + end + endcase + end + 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 + assume (receiver_next_phase == $past(receiver_next_phase)); + end + + if (initiator_state_q == InitIdle) begin + assert (!initiator_isolate_out); + assert (!initiator_clear_out); + assert (!initiator_phase_transition_req); + end + + if (initiator_state_q == InitIsolate || + initiator_state_q == InitWaitIsolatePhaseAck) begin + assert (initiator_isolate_out); + assert (!initiator_clear_out); + assert (initiator_phase_transition_req); + assert (initiator_clear_seq_phase == PhaseIsolate); + end + + if (initiator_state_q == InitWaitIsolateAck) begin + assert (initiator_isolate_out); + assert (!initiator_clear_out); + assert (!initiator_phase_transition_req); + assert (initiator_clear_seq_phase == PhaseIsolate); + end + + if (initiator_state_q == InitClear || + initiator_state_q == InitWaitClearPhaseAck) begin + assert (initiator_isolate_out); + assert (initiator_clear_out); + assert (initiator_phase_transition_req); + assert (initiator_clear_seq_phase == PhaseClear); + end + + if (initiator_state_q == InitWaitClearAck) begin + assert (initiator_isolate_out); + assert (initiator_clear_out); + assert (!initiator_phase_transition_req); + assert (initiator_clear_seq_phase == PhaseClear); + end + + if (initiator_state_q == InitPostClear) begin + assert (initiator_isolate_out); + assert (!initiator_clear_out); + assert (initiator_phase_transition_req); + assert (initiator_clear_seq_phase == PhasePostClear); + end + + if (initiator_state_q == InitFinished) begin + assert (initiator_isolate_out); + assert (!initiator_clear_out); + assert (initiator_phase_transition_req); + assert (initiator_clear_seq_phase == PhaseIdle); + 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 + assert (initiator_state_q == ($past(clear_i) ? InitIsolate : InitIdle)); + end + InitIsolate: begin + if ($past(initiator_phase_transition_ack && isolate_ack_i)) begin + assert (initiator_state_q == InitClear); + end else if ($past(initiator_phase_transition_ack)) begin + assert (initiator_state_q == InitWaitIsolateAck); + end else if ($past(isolate_ack_i)) begin + assert (initiator_state_q == InitWaitIsolatePhaseAck); + end else begin + assert (initiator_state_q == InitIsolate); + end + end + InitWaitIsolateAck: begin + assert (initiator_state_q == + ($past(isolate_ack_i) ? InitClear : InitWaitIsolateAck)); + end + InitWaitIsolatePhaseAck: begin + assert (initiator_state_q == + ($past(initiator_phase_transition_ack) ? InitClear : + InitWaitIsolatePhaseAck)); + end + InitClear: begin + if ($past(initiator_phase_transition_ack && clear_ack_i)) begin + assert (initiator_state_q == InitPostClear); + end else if ($past(initiator_phase_transition_ack)) begin + assert (initiator_state_q == InitWaitClearAck); + end else if ($past(clear_ack_i)) begin + assert (initiator_state_q == InitWaitClearPhaseAck); + end else begin + assert (initiator_state_q == InitClear); + end + end + InitWaitClearAck: begin + assert (initiator_state_q == + ($past(clear_ack_i) ? InitPostClear : InitWaitClearAck)); + end + InitWaitClearPhaseAck: begin + assert (initiator_state_q == + ($past(initiator_phase_transition_ack) ? InitPostClear : + InitWaitClearPhaseAck)); + end + InitPostClear: begin + assert (initiator_state_q == + ($past(initiator_phase_transition_ack) ? InitFinished : InitPostClear)); + end + InitFinished: begin + assert (initiator_state_q == + ($past(initiator_phase_transition_ack) ? InitIdle : InitFinished)); + end + default: begin + assert (initiator_state_q == InitIsolate); + end + 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); + end + +endmodule + + +bind cc_cdc_reset_ctrlr_half cc_cdc_reset_ctrlr_half_properties #( + .CLEAR_ON_ASYNC_RESET(CLEAR_ON_ASYNC_RESET) +) i_cc_cdc_reset_ctrlr_half_properties ( + .clk_i, + .rst_ni, + .clear_i, + .isolate_o, + .isolate_ack_i, + .clear_o, + .clear_ack_i, + .async_next_phase_o, + .async_req_o, + .async_next_phase_i, + .async_req_i, + .async_ack_o, + .initiator_state_q, + .initiator_phase_transition_ack, + .initiator_clear_seq_phase, + .initiator_phase_transition_req, + .initiator_isolate_out, + .initiator_clear_out, + .receiver_phase_q, + .receiver_next_phase, + .receiver_phase_req, + .receiver_phase_ack, + .receiver_isolate_out, + .receiver_clear_out +); diff --git a/formal/cc_cdc_reset_ctrlr_properties.sv b/formal/cc_cdc_reset_ctrlr_properties.sv new file mode 100644 index 00000000..3517d296 --- /dev/null +++ b/formal/cc_cdc_reset_ctrlr_properties.sv @@ -0,0 +1,154 @@ +// Copyright 2026 ETH Zurich and University of Bologna. +// +// Copyright and related rights are licensed under the Solderpad Hardware +// License, Version 0.51 (the "License"); you may not use this file except in +// compliance with the License. You may obtain a copy of the License at +// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +// or agreed to in writing, software, hardware and materials distributed under +// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +// CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// Authors: +// - Philippe Sauter +// +// Description: Composed Reset-Controller Properties +// Instantiate the bidirectional reset controller with a one-cycle local +// acknowledgement model and prove cross-domain clear/isolate sequencing. + +module cc_cdc_reset_ctrlr_composed_harness ( + input wire a_clk_i, + input wire a_rst_ni, + input wire a_clear_i, + input wire b_clk_i, + input wire b_rst_ni, + input wire b_clear_i +); + + logic a_clear_o; + logic a_clear_ack_q; + logic a_isolate_o; + logic a_isolate_ack_q; + logic b_clear_o; + logic b_clear_ack_q; + logic b_isolate_o; + logic b_isolate_ack_q; + + logic a_init_q = 1'b0; + logic b_init_q = 1'b0; + + // Composed harness: instantiate both halves through the public controller and + // model a CDC user that acknowledges isolate/clear one local cycle later. + cc_cdc_reset_ctrlr #( + .SYNC_STAGES ( 2 ), + .CLEAR_ON_ASYNC_RESET ( 1'b1 ) + ) i_dut ( + .a_clk_i, + .a_rst_ni, + .a_clear_i, + .a_clear_o, + .a_clear_ack_i ( a_clear_ack_q ), + .a_isolate_o, + .a_isolate_ack_i ( a_isolate_ack_q ), + .b_clk_i, + .b_rst_ni, + .b_clear_i, + .b_clear_o, + .b_clear_ack_i ( b_clear_ack_q ), + .b_isolate_o, + .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 + assume (!a_rst_ni); + end + end + + always_ff @(posedge b_clk_i) begin + b_init_q <= 1'b1; + if (!b_init_q) begin + assume (!b_rst_ni); + end + end + + always_comb begin + if (a_init_q) begin + assume (a_rst_ni); + end else begin + assume (!a_clear_i); + end + + if (b_init_q) begin + assume (b_rst_ni); + end else begin + assume (!b_clear_i); + 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; + a_clear_ack_q <= 1'b0; + end else begin + a_isolate_ack_q <= a_isolate_o; + a_clear_ack_q <= a_clear_o; + 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; + b_clear_ack_q <= 1'b0; + end else begin + b_isolate_ack_q <= b_isolate_o; + b_clear_ack_q <= b_clear_o; + 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); + end + + if (b_rst_ni) begin + assert (!b_clear_o || b_isolate_o); + end + + if (a_rst_ni && b_rst_ni) begin + assert (!(a_clear_o || b_clear_o) || (a_isolate_o && b_isolate_o)); + end + end + + // Side-A sequential checks validate the one-cycle acknowledgement model and + // cover a sequence initiated from A that propagates isolation to B. + always_ff @(posedge a_clk_i) begin + if (a_rst_ni && $past(a_rst_ni) && a_init_q) begin + assert (a_isolate_ack_q == $past(a_isolate_o)); + assert (a_clear_ack_q == $past(a_clear_o)); + end + + cover (a_rst_ni && b_rst_ni && a_clear_o && b_isolate_o); + end + + // Side-B sequential checks mirror the side-A properties and cover a sequence + // initiated from B that propagates isolation to A. + always_ff @(posedge b_clk_i) begin + if (b_rst_ni && $past(b_rst_ni) && b_init_q) begin + assert (b_isolate_ack_q == $past(b_isolate_o)); + assert (b_clear_ack_q == $past(b_clear_o)); + end + + cover (a_rst_ni && b_rst_ni && b_clear_o && a_isolate_o); + end + +endmodule diff --git a/formal/cdc_reset_ctrlr_composed.sby b/formal/cdc_reset_ctrlr_composed.sby new file mode 100644 index 00000000..07053281 --- /dev/null +++ b/formal/cdc_reset_ctrlr_composed.sby @@ -0,0 +1,38 @@ +# Copyright 2026 ETH Zurich and University of Bologna. +# +# Copyright and related rights are licensed under the Solderpad Hardware +# License, Version 0.51 (the "License"); you may not use this file except in +# compliance with the License. You may obtain a copy of the License at +# http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +# or agreed to in writing, software, hardware and materials distributed under +# this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +# CONDITIONS OF ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the License. +# +# Authors: +# - Philippe Sauter +# +# Description: Composed Reset-Controller Proof Configuration +# Configure the SymbiYosys proof for the two-half reset-controller harness. + +[options] +mode prove +depth 48 + +[engines] +abc pdr + +[script] +plugin -i slang.so +read_slang --std 1800-2017 -Wno-implicit-port-type-mismatch -I../../../include --top cc_cdc_reset_ctrlr_composed_harness cc_pkg.sv cc_sync.sv cc_cdc_4phase.sv cc_cdc_reset_ctrlr.sv cc_cdc_reset_ctrlr_half_properties.sv cc_cdc_reset_ctrlr_properties.sv +prep -top cc_cdc_reset_ctrlr_composed_harness +async2sync +dffunmap + +[files] +../src/cc_pkg.sv +../src/cc_sync.sv +../src/cc_cdc_4phase.sv +../src/cc_cdc_reset_ctrlr.sv +cc_cdc_reset_ctrlr_half_properties.sv +cc_cdc_reset_ctrlr_properties.sv diff --git a/formal/cdc_reset_ctrlr_half.sby b/formal/cdc_reset_ctrlr_half.sby new file mode 100644 index 00000000..5f7b7dc8 --- /dev/null +++ b/formal/cdc_reset_ctrlr_half.sby @@ -0,0 +1,38 @@ +# Copyright 2026 ETH Zurich and University of Bologna. +# +# Copyright and related rights are licensed under the Solderpad Hardware +# License, Version 0.51 (the "License"); you may not use this file except in +# compliance with the License. You may obtain a copy of the License at +# http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +# or agreed to in writing, software, hardware and materials distributed under +# this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +# CONDITIONS OF ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the License. +# +# Authors: +# - Philippe Sauter +# +# Description: Reset-Controller Half Proof Configuration +# Configure the SymbiYosys proof for one reset-controller half and its bound +# local-state property module. + +[options] +mode prove +depth 40 + +[engines] +abc pdr + +[script] +plugin -i slang.so +read_slang --std 1800-2017 -Wno-implicit-port-type-mismatch -I../../../include --top cc_cdc_reset_ctrlr_half cc_pkg.sv cc_sync.sv cc_cdc_4phase.sv cc_cdc_reset_ctrlr.sv cc_cdc_reset_ctrlr_half_properties.sv +prep -top cc_cdc_reset_ctrlr_half +async2sync +dffunmap + +[files] +../src/cc_pkg.sv +../src/cc_sync.sv +../src/cc_cdc_4phase.sv +../src/cc_cdc_reset_ctrlr.sv +cc_cdc_reset_ctrlr_half_properties.sv diff --git a/formal/run_cdc_reset_ctrlr_composed.sh b/formal/run_cdc_reset_ctrlr_composed.sh new file mode 100755 index 00000000..d29919fa --- /dev/null +++ b/formal/run_cdc_reset_ctrlr_composed.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright 2026 ETH Zurich and University of Bologna. +# +# Copyright and related rights are licensed under the Solderpad Hardware +# License, Version 0.51 (the "License"); you may not use this file except in +# compliance with the License. You may obtain a copy of the License at +# http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +# or agreed to in writing, software, hardware and materials distributed under +# this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +# CONDITIONS OF ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the License. +# +# Authors: +# - Philippe Sauter +# +# Description: Composed Reset-Controller Proof Runner +# Run the composed reset-controller SymbiYosys proof from the formal directory. + +set -euo pipefail + +cd "$(dirname "$0")" +"${SBY:=sby}" -f cdc_reset_ctrlr_composed.sby diff --git a/formal/run_cdc_reset_ctrlr_half.sh b/formal/run_cdc_reset_ctrlr_half.sh new file mode 100755 index 00000000..96a2352c --- /dev/null +++ b/formal/run_cdc_reset_ctrlr_half.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash +# Copyright 2026 ETH Zurich and University of Bologna. +# +# Copyright and related rights are licensed under the Solderpad Hardware +# License, Version 0.51 (the "License"); you may not use this file except in +# compliance with the License. You may obtain a copy of the License at +# http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +# or agreed to in writing, software, hardware and materials distributed under +# this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +# CONDITIONS OF ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the License. +# +# Authors: +# - Philippe Sauter +# +# Description: Reset-Controller Half Proof Runner +# Run the reset-controller half SymbiYosys proof from the formal directory. + +set -euo pipefail + +script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" + +: "${SBY:=sby}" + +cd "${script_dir}" +"${SBY}" -f cdc_reset_ctrlr_half.sby diff --git a/src/cc_cdc_2phase_clearable.sv b/src/cc_cdc_2phase_clearable.sv index 3dc27379..739a7e14 100644 --- a/src/cc_cdc_2phase_clearable.sv +++ b/src/cc_cdc_2phase_clearable.sv @@ -9,8 +9,14 @@ // CONDITIONS OF ANY KIND, either express or implied. See the License for the // specific language governing permissions and limitations under the License. // -// Fabian Schuiki (original CDC) -// Manuel Eggimann (clearability feature) +// Authors: +// - Fabian Schuiki (original CDC) +// - Manuel Eggimann (clearability feature) +// - Philippe Sauter (source/destination split) +// +// Description: Clearable Two-Phase CDC +// Transfer payloads with a two-phase handshake while coordinating synchronous +// and optional asynchronous one-sided clears across source and destination. /// A two-phase clock domain crossing. /// @@ -72,21 +78,27 @@ module cc_cdc_2phase_clearable #( output logic dst_valid_o, input logic dst_ready_i ); - logic s_src_clear_req; - logic s_src_clear_ack_q; - logic s_src_ready; - logic s_src_isolate_req; - logic s_src_isolate_ack_q; - logic s_dst_clear_req; - logic s_dst_clear_ack_q; - logic s_dst_valid; - logic s_dst_isolate_req; - logic s_dst_isolate_ack_q; - - // Asynchronous handshake signals between the CDCs - (* dont_touch = "true" *) logic async_req; - (* dont_touch = "true" *) logic async_ack; - (* dont_touch = "true" *) T async_data; + // Asynchronous payload handshake signals between the source and destination. + (* dont_touch = "true" *) logic async_payload_req; + (* dont_touch = "true" *) logic async_payload_ack; + (* dont_touch = "true" *) T async_payload_data; + + // Asynchronous clear-controller phase handshakes between the domains. + (* dont_touch = "true" *) logic async_reset_src2dst_req; + (* dont_touch = "true" *) logic async_reset_dst2src_ack; + (* dont_touch = "true" *) cc_pkg::cdc_clear_seq_phase_e async_reset_src2dst_next_phase; + (* dont_touch = "true" *) logic async_reset_dst2src_req; + (* dont_touch = "true" *) logic async_reset_src2dst_ack; + (* dont_touch = "true" *) cc_pkg::cdc_clear_seq_phase_e async_reset_dst2src_next_phase; + + // Clear/isolate contract: + // - src/dst_clear_pending_o are the local isolate requests. + // - local isolate and clear acknowledgements are one-cycle delayed copies of + // the corresponding local requests. + // - isolate gates the external valid/ready interface on both sides. + // - transactions accepted before or during a clear sequence may complete or + // be dropped, but fresh post-clear traffic must not be duplicated, + // reordered, or corrupted. if (CLEAR_ON_ASYNC_RESET) begin : gen_elaboration_assertion if (SYNC_STAGES < 3) @@ -99,98 +111,237 @@ module cc_cdc_2phase_clearable #( end - // The sender in the source domain. - cc_cdc_2phase_src_clearable #( - .T ( T ), - .SYNC_STAGES ( SYNC_STAGES ) - ) i_src ( - .rst_ni ( src_rst_ni ), - .clk_i ( src_clk_i ), - .clear_i ( s_src_clear_req ), - .data_i ( src_data_i ), - .valid_i ( src_valid_i & !s_src_isolate_req ), - .ready_o ( s_src_ready ), - .async_req_o ( async_req ), - .async_ack_i ( async_ack ), - .async_data_o ( async_data ) + // The source-domain wrapper owns the payload CDC half, local clear/isolate + // acknowledgements, and the local reset-controller half. + cc_cdc_2phase_src_domain_clearable #( + .T ( T ), + .SYNC_STAGES ( SYNC_STAGES ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_src_domain ( + .src_rst_ni ( src_rst_ni ), + .src_clk_i ( src_clk_i ), + .src_clear_i ( src_clear_i ), + .src_clear_pending_o ( src_clear_pending_o ), + .src_data_i ( src_data_i ), + .src_valid_i ( src_valid_i ), + .src_ready_o ( src_ready_o ), + (* async *) .async_payload_req_o ( async_payload_req ), + (* async *) .async_payload_ack_i ( async_payload_ack ), + (* async *) .async_payload_data_o ( async_payload_data ), + (* async *) .async_reset_next_phase_o ( async_reset_src2dst_next_phase ), + (* async *) .async_reset_req_o ( async_reset_src2dst_req ), + (* async *) .async_reset_ack_i ( async_reset_dst2src_ack ), + (* async *) .async_reset_next_phase_i ( async_reset_dst2src_next_phase ), + (* async *) .async_reset_req_i ( async_reset_dst2src_req ), + (* async *) .async_reset_ack_o ( async_reset_src2dst_ack ) + ); + + + // The destination-domain wrapper owns the payload CDC half, local + // clear/isolate acknowledgements, and the local reset-controller half. + cc_cdc_2phase_dst_domain_clearable #( + .T ( T ), + .SYNC_STAGES ( SYNC_STAGES ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_dst_domain ( + .dst_rst_ni ( dst_rst_ni ), + .dst_clk_i ( dst_clk_i ), + .dst_clear_i ( dst_clear_i ), + .dst_clear_pending_o ( dst_clear_pending_o ), + .dst_data_o ( dst_data_o ), + .dst_valid_o ( dst_valid_o ), + .dst_ready_i ( dst_ready_i ), + (* async *) .async_payload_req_i ( async_payload_req ), + (* async *) .async_payload_ack_o ( async_payload_ack ), + (* async *) .async_payload_data_i ( async_payload_data ), + (* async *) .async_reset_next_phase_o ( async_reset_dst2src_next_phase ), + (* async *) .async_reset_req_o ( async_reset_dst2src_req ), + (* async *) .async_reset_ack_i ( async_reset_src2dst_ack ), + (* async *) .async_reset_next_phase_i ( async_reset_src2dst_next_phase ), + (* async *) .async_reset_req_i ( async_reset_src2dst_req ), + (* async *) .async_reset_ack_o ( async_reset_dst2src_ack ) ); - assign src_ready_o = s_src_ready & !s_src_isolate_req; +`ifndef COMMON_CELLS_ASSERTS_OFF + + `ASSERT(no_valid_i_during_clear_i, src_clear_i |-> !src_valid_i, src_clk_i, !src_rst_ni) + +`endif + +endmodule + + +/// Destination-domain wrapper for the clearable two-phase CDC. +module cc_cdc_2phase_dst_domain_clearable #( + parameter type T = logic, + parameter int unsigned SYNC_STAGES = 2, + parameter logic CLEAR_ON_ASYNC_RESET = 1'b1 +) ( + input logic dst_rst_ni, + input logic dst_clk_i, + input logic dst_clear_i, + output logic dst_clear_pending_o, + output T dst_data_o, + output logic dst_valid_o, + input logic dst_ready_i, + input logic async_payload_req_i, + output logic async_payload_ack_o, + input T async_payload_data_i, + output cc_pkg::cdc_clear_seq_phase_e async_reset_next_phase_o, + output logic async_reset_req_o, + input logic async_reset_ack_i, + input cc_pkg::cdc_clear_seq_phase_e async_reset_next_phase_i, + input logic async_reset_req_i, + output logic async_reset_ack_o +); + + logic dst_clear_req; + logic dst_clear_ack_q; + logic dst_isolate_req; + logic dst_isolate_ack_q; + logic dst_valid; + + // Keep the clear-control path one synchronizer stage ahead of the payload CDC + // when async reset propagation is enabled, but never below two stages. + localparam int unsigned ResetSyncStages = (SYNC_STAGES > 2) ? SYNC_STAGES - 1 : 2; + + cc_cdc_reset_ctrlr_half #( + .SYNC_STAGES ( ResetSyncStages ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_cdc_reset_ctrlr_half ( + .clk_i ( dst_clk_i ), + .rst_ni ( dst_rst_ni ), + .clear_i ( dst_clear_i ), + .clear_o ( dst_clear_req ), + .clear_ack_i ( dst_clear_ack_q ), + .isolate_o ( dst_isolate_req ), + .isolate_ack_i ( dst_isolate_ack_q ), + (* async *) .async_next_phase_o ( async_reset_next_phase_o ), + (* async *) .async_req_o ( async_reset_req_o ), + (* async *) .async_ack_i ( async_reset_ack_i ), + (* async *) .async_next_phase_i ( async_reset_next_phase_i ), + (* async *) .async_req_i ( async_reset_req_i ), + (* async *) .async_ack_o ( async_reset_ack_o ) + ); - // The receiver in the destination domain. cc_cdc_2phase_dst_clearable #( .T ( T ), .SYNC_STAGES ( SYNC_STAGES ) ) i_dst ( - .rst_ni ( dst_rst_ni ), - .clk_i ( dst_clk_i ), - .clear_i ( s_dst_clear_req ), - .data_o ( dst_data_o ), - .valid_o ( s_dst_valid ), - .ready_i ( dst_ready_i & !s_dst_isolate_req ), - .async_req_i ( async_req ), - .async_ack_o ( async_ack ), - .async_data_i ( async_data ) + .rst_ni ( dst_rst_ni ), + .clk_i ( dst_clk_i ), + .clear_i ( dst_clear_req ), + .data_o ( dst_data_o ), + .valid_o ( dst_valid ), + .ready_i ( dst_ready_i & !dst_isolate_req ), + (* async *) .async_req_i ( async_payload_req_i ), + (* async *) .async_ack_o ( async_payload_ack_o ), + (* async *) .async_data_i ( async_payload_data_i ) ); - assign dst_valid_o = s_dst_valid & !s_dst_isolate_req; - - // Synchronize the clear and reset signaling in both directions (see header of - // the cc_cdc_reset_ctrlr module for more details.) - cc_cdc_reset_ctrlr #( - .SYNC_STAGES(SYNC_STAGES-1) - ) i_cdc_reset_ctrlr ( - .a_clk_i ( src_clk_i ), - .a_rst_ni ( src_rst_ni ), - .a_clear_i ( src_clear_i ), - .a_clear_o ( s_src_clear_req ), - .a_clear_ack_i ( s_src_clear_ack_q ), - .a_isolate_o ( s_src_isolate_req ), - .a_isolate_ack_i ( s_src_isolate_ack_q ), - .b_clk_i ( dst_clk_i ), - .b_rst_ni ( dst_rst_ni ), - .b_clear_i ( dst_clear_i ), - .b_clear_o ( s_dst_clear_req ), - .b_clear_ack_i ( s_dst_clear_ack_q ), - .b_isolate_o ( s_dst_isolate_req ), - .b_isolate_ack_i ( s_dst_isolate_ack_q ) - ); - - // Just delay the isolate request by one cycle. We can ensure isolation within - // one cycle by just deasserting valid and ready signals on both sides of the CDC. - always_ff @(posedge src_clk_i, negedge src_rst_ni) begin - if (!src_rst_ni) begin - s_src_isolate_ack_q <= 1'b0; - s_src_clear_ack_q <= 1'b0; - end else begin - s_src_isolate_ack_q <= s_src_isolate_req; - s_src_clear_ack_q <= s_src_clear_req; - end - end + assign dst_valid_o = dst_valid & !dst_isolate_req; + // Isolation and clear are acknowledged one cycle after the local request. always_ff @(posedge dst_clk_i, negedge dst_rst_ni) begin if (!dst_rst_ni) begin - s_dst_isolate_ack_q <= 1'b0; - s_dst_clear_ack_q <= 1'b0; + dst_isolate_ack_q <= 1'b0; + dst_clear_ack_q <= 1'b0; end else begin - s_dst_isolate_ack_q <= s_dst_isolate_req; - s_dst_clear_ack_q <= s_dst_clear_req; + dst_isolate_ack_q <= dst_isolate_req; + dst_clear_ack_q <= dst_clear_req; end end + assign dst_clear_pending_o = dst_isolate_req; - assign src_clear_pending_o = s_src_isolate_req; // The isolate signal stays - // asserted during the whole - // clear sequence. - assign dst_clear_pending_o = s_dst_isolate_req; +endmodule -`ifndef COMMON_CELLS_ASSERTS_OFF +/// Source-domain wrapper for the clearable two-phase CDC. +module cc_cdc_2phase_src_domain_clearable #( + parameter type T = logic, + parameter int unsigned SYNC_STAGES = 2, + parameter logic CLEAR_ON_ASYNC_RESET = 1'b1 +) ( + input logic src_rst_ni, + input logic src_clk_i, + input logic src_clear_i, + output logic src_clear_pending_o, + input T src_data_i, + input logic src_valid_i, + output logic src_ready_o, + output logic async_payload_req_o, + input logic async_payload_ack_i, + output T async_payload_data_o, + output cc_pkg::cdc_clear_seq_phase_e async_reset_next_phase_o, + output logic async_reset_req_o, + input logic async_reset_ack_i, + input cc_pkg::cdc_clear_seq_phase_e async_reset_next_phase_i, + input logic async_reset_req_i, + output logic async_reset_ack_o +); - `ASSERT(no_valid_i_during_clear_i, src_clear_i |-> !src_valid_i, src_clk_i, !src_rst_ni) + logic src_clear_req; + logic src_clear_ack_q; + logic src_ready; + logic src_isolate_req; + logic src_isolate_ack_q; + + // Keep the clear-control path one synchronizer stage ahead of the payload CDC + // when async reset propagation is enabled, but never below two stages. + localparam int unsigned ResetSyncStages = (SYNC_STAGES > 2) ? SYNC_STAGES - 1 : 2; + + cc_cdc_reset_ctrlr_half #( + .SYNC_STAGES ( ResetSyncStages ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_cdc_reset_ctrlr_half ( + .clk_i ( src_clk_i ), + .rst_ni ( src_rst_ni ), + .clear_i ( src_clear_i ), + .clear_o ( src_clear_req ), + .clear_ack_i ( src_clear_ack_q ), + .isolate_o ( src_isolate_req ), + .isolate_ack_i ( src_isolate_ack_q ), + (* async *) .async_next_phase_o ( async_reset_next_phase_o ), + (* async *) .async_req_o ( async_reset_req_o ), + (* async *) .async_ack_i ( async_reset_ack_i ), + (* async *) .async_next_phase_i ( async_reset_next_phase_i ), + (* async *) .async_req_i ( async_reset_req_i ), + (* async *) .async_ack_o ( async_reset_ack_o ) + ); -`endif + cc_cdc_2phase_src_clearable #( + .T ( T ), + .SYNC_STAGES ( SYNC_STAGES ) + ) i_src ( + .rst_ni ( src_rst_ni ), + .clk_i ( src_clk_i ), + .clear_i ( src_clear_req ), + .data_i ( src_data_i ), + .valid_i ( src_valid_i & !src_isolate_req ), + .ready_o ( src_ready ), + (* async *) .async_req_o ( async_payload_req_o ), + (* async *) .async_ack_i ( async_payload_ack_i ), + (* async *) .async_data_o ( async_payload_data_o ) + ); + + assign src_ready_o = src_ready & !src_isolate_req; + + // Isolation and clear are acknowledged one cycle after the local request. + always_ff @(posedge src_clk_i, negedge src_rst_ni) begin + if (!src_rst_ni) begin + src_isolate_ack_q <= 1'b0; + src_clear_ack_q <= 1'b0; + end else begin + src_isolate_ack_q <= src_isolate_req; + src_clear_ack_q <= src_clear_req; + end + end + + assign src_clear_pending_o = src_isolate_req; // The isolate signal stays + // asserted during the whole + // clear sequence. endmodule diff --git a/src/cc_cdc_reset_ctrlr.sv b/src/cc_cdc_reset_ctrlr.sv index 13587bf9..d90ae2bf 100644 --- a/src/cc_cdc_reset_ctrlr.sv +++ b/src/cc_cdc_reset_ctrlr.sv @@ -1,11 +1,23 @@ -//----------------------------------------------------------------------------- -// Title : CDC Clear Signaling Synchronization -// ----------------------------------------------------------------------------- -// File : cdc_clear_propagator.sv Author : Manuel Eggimann -// Created : 22.12.2021 -// ----------------------------------------------------------------------------- -// Description : +// Copyright 2021 ETH Zurich and University of Bologna. // +// Copyright and related rights are licensed under the Solderpad Hardware +// License, Version 0.51 (the "License"); you may not use this file except in +// compliance with the License. You may obtain a copy of the License at +// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +// or agreed to in writing, software, hardware and materials distributed under +// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +// CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. +// +// Authors: +// - Manuel Eggimann +// - Philippe Sauter (formalization and stage cleanup) +// +// Description: CDC Clear Signaling Synchronization +// Coordinate clear and isolate sequencing between two CDC clock domains so +// one-sided reset or clear requests do not break the protected CDC protocol. +// +// Detailed Description: // This module is mainly used internally to synchronize the clear requests // between both sides of a CDC module. It aims to solve the problem of // initiating a CDC clear, reset one-sidedly without running into @@ -93,19 +105,6 @@ // side is isolated (depending on protocol this might take several cycles), // assert the a/b_isolate_ack_i signal. // -// ----------------------------------------------------------------------------- -// Copyright (C) 2021 ETH Zurich, University of Bologna Copyright and related -// rights are licensed under the Solderpad Hardware License, Version 0.51 (the -// "License"); you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law or -// agreed to in writing, software, hardware and materials distributed under this -// License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS -// OF ANY KIND, either express or implied. See the License for the specific -// language governing permissions and limitations under the License. -// SPDX-License-Identifier: SHL-0.51 -// ----------------------------------------------------------------------------- - module cc_cdc_reset_ctrlr import cc_pkg::*; #( @@ -262,6 +261,10 @@ module cc_cdc_reset_ctrlr_half logic initiator_isolate_out; logic initiator_clear_out; + // The phase CDC is a real CDC even when callers pass a reduced latency for + // synchronous-clear-only configurations. + localparam int unsigned ResetSyncStages = (SYNC_STAGES > 2) ? SYNC_STAGES : 2; + always_comb begin initiator_state_d = initiator_state_q; initiator_phase_transition_req = 1'b0; @@ -388,7 +391,7 @@ module cc_cdc_reset_ctrlr_half cc_cdc_4phase_src #( .T(cdc_clear_seq_phase_e), - .SYNC_STAGES(2), + .SYNC_STAGES(ResetSyncStages), .DECOUPLED(0), // Important! The CDC must not be in decoupled mode. // Otherwise we will proceed to the next state without // waiting for the new state to arrive on the other side. @@ -420,7 +423,7 @@ module cc_cdc_reset_ctrlr_half cc_cdc_4phase_dst #( .T(cdc_clear_seq_phase_e), - .SYNC_STAGES(2), + .SYNC_STAGES(ResetSyncStages), .DECOUPLED(0) // Important! The CDC must not be in decoupled mode. Otherwise // we will proceed to the next state without waiting for the // new state to arrive on the other side. diff --git a/test/cc_cdc_2phase_clearable_tb.sv b/test/cc_cdc_2phase_clearable_tb.sv index 715726a9..ad9e3d96 100644 --- a/test/cc_cdc_2phase_clearable_tb.sv +++ b/test/cc_cdc_2phase_clearable_tb.sv @@ -9,283 +9,823 @@ // CONDITIONS OF ANY KIND, either express or implied. See the License for the // specific language governing permissions and limitations under the License. // -// Fabian Schuiki +// Authors: +// - Fabian Schuiki +// - Philippe Sauter +// +// Description: Clearable Two-Phase CDC Testbench +// Exercise payload ordering, clear/isolate sequencing, async-reset behavior, +// and timed async-channel delay sweeps for cc_cdc_2phase_clearable. module cc_cdc_2phase_clearable_tb; - parameter int UNTIL = 100000; - parameter bit INJECT_DELAYS = 1; - parameter int CLEAR_PPM = 2000; - parameter int SYNC_STAGES = 3; + timeunit 1ns; + timeprecision 1ps; + + parameter int unsigned NUM_RANDOM_TRANSFERS = 200; + parameter int unsigned NUM_ACTIVE_STRESS_TRANSFERS = 160; + parameter int unsigned NUM_ACTIVE_STRESS_EVENTS = 8; + parameter int unsigned SYNC_STAGES = 3; + parameter int unsigned TCK_SRC_PS = 10000; + parameter int unsigned TCK_DST_PS = 17000; + parameter int unsigned TIMEOUT_CYCLES = 20000; + parameter int unsigned SEED = 32'hcdc2_c1ea; + parameter bit CLEAR_ON_ASYNC_RESET = 1'b1; + parameter bit INJECT_DELAYS = 1'b0; + parameter int unsigned MAX_DELAY_PS = 0; + parameter int unsigned SRC_START_DELAY_PS = 0; + parameter int unsigned DST_START_DELAY_PS = 0; + typedef enum logic [1:0] { + DstReadyLow, + DstReadyHigh, + DstReadyRandom + } dst_ready_mode_e; - time tck_src = 10ns; - time tck_dst = 10ns; - bit src_done = 0; - bit dst_done = 0; - bit done; - assign done = src_done & dst_done; + typedef enum logic [2:0] { + EventSrcClear, + EventDstClear, + EventBothClear, + EventSrcReset, + EventDstReset + } control_event_e; - // Signals of the design under test. - logic src_rst_ni = 1; - logic src_clk_i = 0; - logic [31:0] src_data_i = 0; - logic src_clear_i = 0; + time tck_src = TCK_SRC_PS * 1ps; + time tck_dst = TCK_DST_PS * 1ps; + + logic src_rst_ni = 1'b1; + logic src_clk_i = 1'b0; + logic src_clear_i = 1'b0; logic src_clear_pending_o; - logic src_valid_i = 0; + logic [31:0] src_data_i = '0; + logic src_valid_i = 1'b0; logic src_ready_o; - logic dst_rst_ni = 1; - logic dst_clk_i = 0; - logic dst_clear_i = 0; + logic dst_rst_ni = 1'b1; + logic dst_clk_i = 1'b0; + logic dst_clear_i = 1'b0; logic dst_clear_pending_o; logic [31:0] dst_data_o; logic dst_valid_o; - logic dst_ready_i = 0; + logic dst_ready_i = 1'b0; + + logic [31:0] expected_q[$]; + // Transactions accepted before/during a clear window may either be dropped or + // complete later. They are still checked against this queue to catch truly + // spurious or duplicated destination handshakes. + logic [31:0] stale_q[$]; + int unsigned num_src_handshakes = 0; + int unsigned num_dst_handshakes = 0; + int unsigned num_stale_ignored = 0; + int unsigned num_active_stress_events = 0; + int unsigned num_errors = 0; + bit drop_window = 1'b0; + bit active_src_pause = 1'b0; + bit active_src_done = 1'b1; - // Instantiate the design under test. - if (INJECT_DELAYS) begin : g_dut - cc_cdc_2phase_clearable_tb_delay_injector #(0.8ns) i_dut (.*); - end else begin : g_dut - cc_cdc_2phase_clearable #(logic [31:0]) i_dut (.*); + dst_ready_mode_e dst_ready_mode = DstReadyLow; + + // Instantiate either the plain DUT or the timed delay-injection harness used + // by sweeps to perturb every explicit asynchronous channel. + if (INJECT_DELAYS) begin : gen_delayed_dut + cc_cdc_2phase_clearable_tb_delay_injector #( + .SYNC_STAGES ( SYNC_STAGES ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ), + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_dut ( + .src_rst_ni, + .src_clk_i, + .src_clear_i, + .src_clear_pending_o, + .src_data_i, + .src_valid_i, + .src_ready_o, + .dst_rst_ni, + .dst_clk_i, + .dst_clear_i, + .dst_clear_pending_o, + .dst_data_o, + .dst_valid_o, + .dst_ready_i + ); + end else begin : gen_dut + cc_cdc_2phase_clearable #( + .T ( logic [31:0] ), + .SYNC_STAGES ( SYNC_STAGES ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_dut ( + .src_rst_ni, + .src_clk_i, + .src_clear_i, + .src_clear_pending_o, + .src_data_i, + .src_valid_i, + .src_ready_o, + .dst_rst_ni, + .dst_clk_i, + .dst_clear_i, + .dst_clear_pending_o, + .dst_data_o, + .dst_valid_o, + .dst_ready_i + ); end - typedef struct { - int data; - bit is_stale; - } item_t; + initial begin : gen_src_clk + #(SRC_START_DELAY_PS * 1ps); + forever #(tck_src / 2) src_clk_i = ~src_clk_i; + end + initial begin : gen_dst_clk + #(DST_START_DELAY_PS * 1ps); + forever #(tck_dst / 2) dst_clk_i = ~dst_clk_i; + end - // Mailbox with expected items on destination side. - item_t dst_mbox[$]; - int num_sent = 0; - int num_received = 0; - int num_failed = 0; + always @(negedge dst_clk_i) begin + case (dst_ready_mode) + DstReadyLow: dst_ready_i <= 1'b0; + DstReadyHigh: dst_ready_i <= 1'b1; + DstReadyRandom: dst_ready_i <= ($urandom_range(0, 99) < 70); + default: dst_ready_i <= 1'b0; + endcase + end - // Clock generators. - initial begin - static int num_items, num_clks; - num_items = 10; - num_clks = 0; - #10ns; - src_rst_ni = 0; - #10ns; - src_rst_ni = 1; - #10ns; - while (!done) begin - src_clk_i = 1; - #(tck_src/2); - src_clk_i = 0; - #(tck_src/2); - - // Modulate the clock frequency. - num_clks++; - if (num_sent >= num_items && num_clks > 10) begin - num_items = num_sent + 10; - num_clks = 0; - tck_src = $urandom_range(1000, 10000) * 1ps; - assert(tck_src > 0); + // Scoreboard source and destination handshakes. During clear/reset windows, + // accepted source items are stale: they may later complete or be dropped. + always @(posedge src_clk_i) begin + if (!src_rst_ni) begin + // Reset is handled by the DUT. The scoreboard is controlled by the test + // sequence because one-sided reset intentionally drops in-flight items. + end else begin + if (src_clear_pending_o && src_ready_o) begin + report_error("src_ready_o asserted while src_clear_pending_o is asserted"); + end + if (src_valid_i && src_ready_o) begin + num_src_handshakes++; + if (drop_window) begin + stale_q.push_back(src_data_i); + end else begin + expected_q.push_back(src_data_i); + end end end end - initial begin - static int num_items, num_clks; - num_items = 10; - num_clks = 0; - #10ns; - dst_rst_ni = 0; - #10ns; - dst_rst_ni = 1; - #10ns; - while (!done) begin - dst_clk_i = 1; - #(tck_dst/2); - dst_clk_i = 0; - #(tck_dst/2); - - // Modulate the clock frequency. - num_clks++; - if (num_received >= num_items && num_clks > 10) begin - num_items = num_received + 10; - num_clks = 0; - tck_dst = $urandom_range(1000, 10000) * 1ps; - assert(tck_dst > 0); + always @(posedge dst_clk_i) begin + logic [31:0] expected; + + if (!dst_rst_ni) begin + // See source-side reset comment above. + end else begin + if (dst_clear_pending_o && dst_valid_o) begin + report_error("dst_valid_o asserted while dst_clear_pending_o is asserted"); + end + if (dst_valid_o && dst_ready_i) begin + num_dst_handshakes++; + if (consume_stale(dst_data_o)) begin + num_stale_ignored++; + end else if (drop_window) begin + report_error($sformatf("unexpected destination transaction during drop window: data=0x%08h stale_pending=%0d", + dst_data_o, stale_q.size())); + end else if (expected_q.size() == 0) begin + report_error($sformatf("unexpected destination transaction: data=0x%08h", dst_data_o)); + end else begin + expected = expected_q.pop_front(); + if (dst_data_o !== expected) begin + report_error($sformatf("transaction mismatch: expected=0x%08h actual=0x%08h", + expected, dst_data_o)); + end + end end end end - // Source side sender. - task src_cycle_start; - #(tck_src*0.8); + // Small shared helpers for reporting, cycle waits, and the stale-item window + // used whenever a clear/reset may intentionally discard in-flight traffic. + task automatic report_error(input string msg); + num_errors++; + $error("%s", msg); endtask - task src_cycle_end; - @(posedge src_clk_i); + function automatic bit consume_stale(input logic [31:0] data); + int match_idx; + + match_idx = -1; + foreach (stale_q[i]) begin + if ((match_idx < 0) && (stale_q[i] === data)) begin + match_idx = int'(i); + end + end + + if (match_idx < 0) begin + return 1'b0; + end + + // Earlier stale items may have been dropped by the clear sequence. + repeat (match_idx + 1) begin + void'(stale_q.pop_front()); + end + return 1'b1; + endfunction + + task automatic wait_src_cycles(input int unsigned cycles); + repeat (cycles) begin + @(posedge src_clk_i); + end + #1ps; endtask - initial begin - @(negedge src_rst_ni); - @(posedge src_rst_ni); - repeat(3) @(posedge src_clk_i); - for (int i = 0; i < UNTIL; i++) begin - static item_t stimulus; - static bit clear_cdc; - stimulus.data = $random(); - stimulus.is_stale = 1'b0; - src_data_i <= #(tck_src*0.2) stimulus.data; - src_valid_i <= #(tck_src*0.2) 1; - dst_mbox.push_front(stimulus); - num_sent++; - src_cycle_start(); - while (!src_ready_o) begin - src_cycle_end(); - src_cycle_start(); - // Ramdomly clear the CDC. During pending transaction - clear_cdc = $urandom_range(0,1e6) < CLEAR_PPM; - if (clear_cdc && !src_clear_pending_o) begin - // The cdc shall be cleared. Mark all items in the mailbox as stale. - foreach(dst_mbox[i]) begin - if (!dst_mbox[i].is_stale) begin - dst_mbox[i].is_stale = 1'b1; - num_sent--; - end - end - // Clear the CDC using either asynchronous or synchronous reset - if ($urandom_range(0,1) == 1) begin - $info("Randomly clearing CDC source-side synchronously"); - // Now raise the clear signal for one clock cycle. - src_cycle_start(); + task automatic wait_dst_cycles(input int unsigned cycles); + repeat (cycles) begin + @(posedge dst_clk_i); + end + #1ps; + endtask + + task automatic begin_drop_window; + drop_window = 1'b1; + while (expected_q.size() != 0) begin + stale_q.push_back(expected_q.pop_front()); + end + endtask + + task automatic reset_both_domains; + drop_window = 1'b1; + expected_q.delete(); + stale_q.delete(); + src_valid_i = 1'b0; + src_clear_i = 1'b0; + dst_clear_i = 1'b0; + active_src_pause = 1'b0; + active_src_done = 1'b1; + dst_ready_mode = DstReadyLow; + src_rst_ni = 1'b0; + dst_rst_ni = 1'b0; + + fork + wait_src_cycles(4); + wait_dst_cycles(4); + join + + src_rst_ni = 1'b1; + dst_rst_ni = 1'b1; + + fork + wait_src_cycles(6); + wait_dst_cycles(6); + join + + drop_window = 1'b0; + endtask + + // Clear/reset completion helpers. They check that both domains see the + // pending sequence and then wait for the CDC to settle before fresh traffic. + task automatic wait_pending_seen(input bit expect_src, input bit expect_dst, input string test_name); + bit seen_src; + bit seen_dst; + + seen_src = !expect_src; + seen_dst = !expect_dst; + + for (int unsigned i = 0; i < TIMEOUT_CYCLES; i++) begin + if (src_clear_pending_o) begin + seen_src = 1'b1; + end + if (dst_clear_pending_o) begin + seen_dst = 1'b1; + end + if (seen_src && seen_dst) begin + return; + end + @(posedge src_clk_i or posedge dst_clk_i); + end + + report_error($sformatf("timeout waiting for clear pending assertion in %s", test_name)); + endtask + + task automatic wait_clear_done(input string test_name); + for (int unsigned i = 0; i < TIMEOUT_CYCLES; i++) begin + if (src_rst_ni && dst_rst_ni && + !src_clear_i && !dst_clear_i && + !src_clear_pending_o && !dst_clear_pending_o) begin + fork + wait_src_cycles(SYNC_STAGES + 4); + wait_dst_cycles(SYNC_STAGES + 4); + join + expected_q.delete(); + return; + end + @(posedge src_clk_i or posedge dst_clk_i); + end + + report_error($sformatf("timeout waiting for clear completion in %s", test_name)); + endtask + + task automatic send_word(input logic [31:0] data); + src_data_i = data; + src_valid_i = 1'b1; + + for (int unsigned i = 0; i < TIMEOUT_CYCLES; i++) begin + @(negedge src_clk_i); + if (src_ready_o) begin + @(posedge src_clk_i); + @(negedge src_clk_i); + src_valid_i = 1'b0; + src_data_i = '0; + return; + end + end + + report_error($sformatf("timeout sending data=0x%08h", data)); + src_valid_i = 1'b0; + endtask + + // Transfer helpers for normal traffic: send ordered words, wait for the + // scoreboard to drain, and verify the source has returned to ready. + task automatic wait_scoreboard_empty(input string test_name); + for (int unsigned i = 0; i < TIMEOUT_CYCLES; i++) begin + if (expected_q.size() == 0) begin + return; + end + @(posedge dst_clk_i or posedge src_clk_i); + end + + report_error($sformatf("timeout waiting for scoreboard to drain in %s, pending=%0d", + test_name, expected_q.size())); + endtask + + task automatic wait_src_ready(input string test_name); + for (int unsigned i = 0; i < TIMEOUT_CYCLES; i++) begin + if (src_ready_o) begin + return; + end + @(posedge src_clk_i or posedge dst_clk_i); + end + + report_error($sformatf("timeout waiting for source ready in %s", test_name)); + endtask + + task automatic wait_dst_valid(input string test_name); + for (int unsigned i = 0; i < TIMEOUT_CYCLES; i++) begin + if (dst_valid_o) begin + return; + end + @(posedge dst_clk_i or posedge src_clk_i); + end + + report_error($sformatf("timeout waiting for destination valid in %s", test_name)); + endtask + + task automatic send_sequence(input int unsigned num_words, input logic [31:0] base); + for (int unsigned i = 0; i < num_words; i++) begin + send_word(base + i); + if ($urandom_range(0, 3) == 0) begin + wait_src_cycles($urandom_range(1, 3)); + end + end + endtask + + function automatic string control_event_name(input control_event_e ctrl_event); + unique case (ctrl_event) + EventSrcClear: control_event_name = "source synchronous clear"; + EventDstClear: control_event_name = "destination synchronous clear"; + EventBothClear: control_event_name = "simultaneous synchronous clear"; + EventSrcReset: control_event_name = "source asynchronous reset"; + EventDstReset: control_event_name = "destination asynchronous reset"; + default: control_event_name = "unknown control event"; + endcase + endfunction + + function automatic bit event_touches_source(input control_event_e ctrl_event); + return ctrl_event inside {EventSrcClear, EventBothClear, EventSrcReset}; + endfunction + + task automatic pulse_control_event(input control_event_e ctrl_event); + unique case (ctrl_event) + EventSrcClear: begin + @(negedge src_clk_i); + src_clear_i = 1'b1; + @(negedge src_clk_i); + src_clear_i = 1'b0; + end + EventDstClear: begin + @(negedge dst_clk_i); + dst_clear_i = 1'b1; + @(negedge dst_clk_i); + dst_clear_i = 1'b0; + end + EventBothClear: begin + fork + begin + @(negedge src_clk_i); src_clear_i = 1'b1; - src_valid_i = 1'b0; - src_cycle_end(); - src_clear_i = #(tck_src*0.2) 1'b0; - end else begin - $info("Randomly resetting CDC source-side asynchronously"); - // Now assert the async reset signal for one clock cycle. - src_cycle_start(); - src_rst_ni = 1'b0; - src_valid_i = 1'b0; - src_cycle_end(); - src_rst_ni = #(tck_src*0.2) 1'b1; + @(negedge src_clk_i); + src_clear_i = 1'b0; end - break; - end + begin + @(negedge dst_clk_i); + dst_clear_i = 1'b1; + @(negedge dst_clk_i); + dst_clear_i = 1'b0; + end + join end - src_cycle_end(); - src_valid_i <= #(tck_src*0.2) 0; + EventSrcReset: begin + #(tck_src / 3); + src_rst_ni = 1'b0; + wait_src_cycles(2); + src_rst_ni = 1'b1; + end + EventDstReset: begin + #(tck_dst / 3); + dst_rst_ni = 1'b0; + wait_dst_cycles(2); + dst_rst_ni = 1'b1; + end + default: begin + end + endcase + endtask + + // Run a control event with the expected cross-domain clear sequence. The drop + // window covers accepted items that may be intentionally discarded. + task automatic run_control_event(input control_event_e ctrl_event, input string test_name, + input bit pause_source_driver = 1'b0); + if (pause_source_driver) begin + pause_active_source(test_name); end - src_done = 1; - end - // Destination side receiver. - task dst_cycle_start; - #(tck_dst*0.8); - endtask + begin_drop_window(); + if (event_touches_source(ctrl_event)) begin + src_valid_i = 1'b0; + end - task dst_cycle_end; - @(posedge dst_clk_i); + pulse_control_event(ctrl_event); + wait_pending_seen(1'b1, 1'b1, test_name); + wait_clear_done(test_name); + drop_window = 1'b0; + + if (pause_source_driver) begin + resume_active_source(); + end endtask - initial begin - @(negedge dst_rst_ni); - @(posedge dst_rst_ni); - repeat(3) @(posedge dst_clk_i); - while (!src_done || dst_mbox.size() > 0) begin - static item_t expected; - static integer actual; - static int cooldown; - static bit clear_cdc; - //randomly drop the transaction by clearing from the destination side - clear_cdc = $urandom_range(0,1e6) < CLEAR_PPM; - if (clear_cdc && !dst_clear_pending_o) begin - // Clear the CDC using either asynchronous or synchronous reset - if ($urandom_range(0,1) == 1) begin - $info("Randomly clearing CDC destination-side synchronously"); - // Now raise the clear signal for one clock cycle. - dst_cycle_start(); - dst_clear_i = 1'b1; - dst_ready_i = 1'b0; - dst_cycle_end(); - dst_clear_i = #(tck_dst*0.2) 1'b0; - end else begin - $info("Randomly resetting CDC destination-side asynchronously"); - // Now assert the async reset signal for one clock cycle. - dst_cycle_start(); - dst_rst_ni = 1'b0; - dst_ready_i = 1'b0; - dst_cycle_end(); - dst_rst_ni = #(tck_dst*0.2) 1'b1; + task automatic check_no_cross_clear_after_reset(input control_event_e ctrl_event, + input string test_name); + $display("%m: %s", test_name); + src_valid_i = 1'b0; + wait_scoreboard_empty(test_name); + wait_src_ready(test_name); + + pulse_control_event(ctrl_event); + + for (int unsigned i = 0; i < TIMEOUT_CYCLES / 20; i++) begin + unique case (ctrl_event) + EventSrcReset: begin + if (dst_clear_pending_o) begin + report_error($sformatf("unexpected destination clear pending in %s", test_name)); + wait_clear_done(test_name); + return; + end end - // Wait for 1 dst clock cycle + SYNC_STAGES source clock cycles for the clear to propagate to the - // other domain before clearing the mailbox (the pending item might be - // consumsed by destination before the clear request arrives). - @(posedge dst_clk_i); - repeat(SYNC_STAGES) @(posedge src_clk_i); - // and end the loop iteration at the rising edge of the dst clk - dst_cycle_end(); - // Delete all pending items in the mailbox except for the last one - while (dst_mbox.size() > 1) begin - expected = dst_mbox.pop_back(); + EventDstReset: begin + if (src_clear_pending_o) begin + report_error($sformatf("unexpected source clear pending in %s", test_name)); + wait_clear_done(test_name); + return; + end end - end else begin - dst_ready_i <= #(tck_dst*0.2) 1; - dst_cycle_start(); - while (!dst_valid_o) begin - dst_cycle_end(); - dst_cycle_start(); + default: begin + report_error($sformatf("unsupported no-cross-clear event in %s", test_name)); + return; end - actual = dst_data_o; - num_received++; - if (dst_mbox.size() == 0) begin - $error("unexpected transaction: data=%0h", actual); - num_failed++; + endcase + @(posedge src_clk_i or posedge dst_clk_i); + end + endtask + + task automatic run_transfer_check(input string test_name, input int unsigned num_words, + input logic [31:0] base, + input dst_ready_mode_e ready_mode); + $display("%m: %s", test_name); + dst_ready_mode = ready_mode; + send_sequence(num_words, base); + wait_scoreboard_empty(test_name); + wait_src_ready(test_name); + dst_ready_mode = DstReadyLow; + wait_dst_cycles(2); + endtask + + task automatic stage_backpressured_item(input logic [31:0] data, input string test_name); + dst_ready_mode = DstReadyHigh; + wait_src_ready(test_name); + send_word(data); + dst_ready_mode = DstReadyLow; + wait_dst_valid(test_name); + endtask + + // Backpressure tests stage one valid destination item, withhold ready, and + // then trigger clear/reset to exercise the exposed valid-withdrawal contract. + task automatic run_backpressured_control_check(input control_event_e ctrl_event, + input logic [31:0] staged_data, + input logic [31:0] post_base); + string event_name; + + event_name = control_event_name(ctrl_event); + $display("%m: %s while destination holds a valid item", event_name); + stage_backpressured_item(staged_data, + {event_name, " while valid is backpressured"}); + run_control_event(ctrl_event, {event_name, " while valid is backpressured"}); + run_transfer_check({"post-", event_name, "-backpressure transfer"}, 8, post_base, + DstReadyHigh); + endtask + + // Active-traffic stress keeps a source driver running while randomized + // clear/reset events interrupt the CDC from either side. + task automatic pause_active_source(input string test_name); + active_src_pause = 1'b1; + wait_src_cycles(2); + @(negedge src_clk_i); + #1ps; + src_valid_i = 1'b0; + src_data_i = '0; + $display("%m: active source paused for %s", test_name); + endtask + + task automatic resume_active_source; + @(negedge src_clk_i); + active_src_pause = 1'b0; + endtask + + task automatic drive_active_source(input int unsigned num_words, input logic [31:0] base); + int unsigned sent; + bit handshake_seen; + + sent = 0; + handshake_seen = 1'b0; + active_src_done = 1'b0; + src_valid_i = 1'b0; + src_data_i = '0; + + while (sent < num_words) begin + @(negedge src_clk_i); + #1ps; + + if (!src_rst_ni || active_src_pause) begin + src_valid_i = 1'b0; + src_data_i = '0; + handshake_seen = 1'b0; + end else if (handshake_seen) begin + handshake_seen = 1'b0; + if ((sent >= num_words) || ($urandom_range(0, 9) == 0)) begin + src_valid_i = 1'b0; + src_data_i = '0; end else begin - expected = dst_mbox.pop_back(); - if (actual != expected.data) begin - // Check if the expected item is a stale item. If so, pop all stale - // items until we receive a fresh one and check again. - while (dst_mbox.size() > 0 && expected.is_stale && expected.data != actual) begin - expected = dst_mbox.pop_back(); - end - if (actual != expected.data) begin - $error("transaction mismatch: exp=%0h, act=%0h", expected.data, actual); - num_failed++; - end else begin - if (!expected.is_stale) begin - num_received++; - end - end - end else if (expected.is_stale) begin - $info("Received stale item after clear. This is expected to happen for some cycles after the clear until the clear propagated to the other side."); - end else begin - num_received++; - end + src_valid_i = 1'b1; + src_data_i = base + sent; end - dst_cycle_end(); - dst_ready_i <= #(tck_dst*0.2) 0; + end else if (!src_valid_i && ($urandom_range(0, 3) != 0)) begin + src_valid_i = 1'b1; + src_data_i = base + sent; + end - // Insert a random cooldown period. - cooldown = $urandom_range(0, 40); - if (cooldown < 20) repeat(cooldown) @(posedge dst_clk_i); + @(posedge src_clk_i); + if (src_rst_ni && !active_src_pause && src_valid_i && src_ready_o) begin + sent++; + handshake_seen = 1'b1; end end - if (num_failed > 0) begin - $error("%0d/%0d items mismatched", num_failed, num_sent); + @(negedge src_clk_i); + src_valid_i = 1'b0; + src_data_i = '0; + active_src_done = 1'b1; + endtask + + task automatic wait_active_event_gap; + repeat ($urandom_range(4, 20)) begin + @(posedge src_clk_i or posedge dst_clk_i); + end + #1ps; + endtask + + task automatic run_active_control_events(input int unsigned num_events); + string event_name; + control_event_e ctrl_event; + + for (int unsigned i = 0; i < num_events; i++) begin + wait_active_event_gap(); + if (CLEAR_ON_ASYNC_RESET) begin + unique case (i) + 0: ctrl_event = EventDstClear; + 1: ctrl_event = EventDstReset; + 2: ctrl_event = EventSrcClear; + 3: ctrl_event = EventSrcReset; + 4: ctrl_event = EventBothClear; + default: ctrl_event = control_event_e'($urandom_range(0, 4)); + endcase + end else begin + unique case (i) + 0: ctrl_event = EventDstClear; + 1: ctrl_event = EventSrcClear; + 2: ctrl_event = EventBothClear; + default: ctrl_event = control_event_e'($urandom_range(0, 2)); + endcase + end + + event_name = $sformatf("active stress event %0d: %s", i, control_event_name(ctrl_event)); + run_control_event(ctrl_event, event_name, event_touches_source(ctrl_event)); + + num_active_stress_events++; + end + endtask + + task automatic run_active_traffic_stress; + if ((NUM_ACTIVE_STRESS_TRANSFERS == 0) || (NUM_ACTIVE_STRESS_EVENTS == 0)) begin + return; + end + + $display("%m: active traffic stress: transfers=%0d events=%0d", + NUM_ACTIVE_STRESS_TRANSFERS, NUM_ACTIVE_STRESS_EVENTS); + expected_q.delete(); + stale_q.delete(); + drop_window = 1'b0; + active_src_pause = 1'b0; + active_src_done = 1'b0; + dst_ready_mode = DstReadyRandom; + + fork + drive_active_source(NUM_ACTIVE_STRESS_TRANSFERS, 32'ha000_0000); + run_active_control_events(NUM_ACTIVE_STRESS_EVENTS); + join + + if (!active_src_done) begin + report_error("active source driver did not finish"); + end + + wait_scoreboard_empty("active traffic stress"); + wait_src_ready("active traffic stress"); + dst_ready_mode = DstReadyLow; + wait_dst_cycles(2); + endtask + + initial begin : run_tests + int unsigned seed; + + seed = SEED; + seed = $urandom(seed); + $display("%m: SEED=0x%08h derived=0x%08h", SEED, seed); + + reset_both_domains(); + + // Baseline ordered transfer with the destination always ready. + run_transfer_check("basic fixed-ready transfer", 32, 32'h1000_0000, DstReadyHigh); + + // Idle synchronous clears from source, destination, and both domains, + // followed by fresh transfers to check post-clear recovery. + run_control_event(EventSrcClear, "source synchronous idle clear"); + run_transfer_check("post-source-clear transfer", 16, 32'h2000_0000, DstReadyHigh); + + run_control_event(EventDstClear, "destination synchronous idle clear"); + run_transfer_check("post-destination-clear transfer", 16, 32'h3000_0000, DstReadyHigh); + + run_control_event(EventBothClear, "simultaneous synchronous idle clear"); + run_transfer_check("post-simultaneous-clear transfer", 16, 32'h4000_0000, DstReadyHigh); + + // One-sided asynchronous resets are only a cross-domain clear source when + // the feature is enabled. + if (CLEAR_ON_ASYNC_RESET) begin + run_control_event(EventSrcReset, "source asynchronous idle reset"); + run_transfer_check("post-source-async-reset transfer", 16, 32'h5000_0000, DstReadyHigh); + + run_control_event(EventDstReset, "destination asynchronous idle reset"); + run_transfer_check("post-destination-async-reset transfer", 16, 32'h6000_0000, DstReadyHigh); end else begin - $info("%0d items passed", num_sent); + check_no_cross_clear_after_reset(EventSrcReset, + "source asynchronous idle reset without cross-clear"); + reset_both_domains(); + + check_no_cross_clear_after_reset(EventDstReset, + "destination asynchronous idle reset without cross-clear"); + reset_both_domains(); + end + + // Backpressured destination-visible traffic is the critical case where + // clear/reset may withdraw valid and drop the staged item. + run_backpressured_control_check(EventDstClear, 32'hc1ea_0001, 32'hc1ea_1000); + run_backpressured_control_check(EventSrcClear, 32'hc1ea_2001, 32'hc1ea_3000); + run_backpressured_control_check(EventBothClear, 32'hc1ea_4001, 32'hc1ea_5000); + if (CLEAR_ON_ASYNC_RESET) begin + run_backpressured_control_check(EventSrcReset, 32'hc1ea_6001, 32'hc1ea_7000); + run_backpressured_control_check(EventDstReset, 32'hc1ea_8001, 32'hc1ea_9000); end - dst_done = 1; + // Long mixed stress run with random traffic, destination backpressure, and + // interleaved source/destination clear or reset events. + run_active_traffic_stress(); + + // Final randomized-ready transfer checks ordinary payload ordering after + // all disruptive control-event categories have completed. + run_transfer_check("randomized ready transfer", NUM_RANDOM_TRANSFERS, 32'h7000_0000, + DstReadyRandom); + + if (num_errors != 0) begin + $fatal(1, "%m: failed with %0d errors", num_errors); + end + + $display("%m: passed: src_handshakes=%0d dst_handshakes=%0d stale_ignored=%0d stale_dropped=%0d active_stress_events=%0d", + num_src_handshakes, num_dst_handshakes, num_stale_ignored, + stale_q.size(), num_active_stress_events); + $finish; + end + + // Bind a simulation-only monitor into each reset-controller half. It mirrors + // the formal invariants to catch invalid internal clear FSM behavior in Questa. + bind cc_cdc_reset_ctrlr_half cc_cdc_reset_ctrlr_half_monitor i_monitor ( + .clk_i, + .rst_ni, + .isolate_o, + .isolate_ack_i, + .clear_o, + .clear_ack_i, + .async_next_phase_o, + .async_req_o, + .async_next_phase_i, + .async_req_i, + .initiator_state_q, + .initiator_clear_seq_phase, + .initiator_phase_transition_req, + .initiator_isolate_out, + .initiator_clear_out, + .receiver_phase_q, + .receiver_next_phase, + .receiver_phase_req, + .receiver_phase_ack, + .receiver_isolate_out, + .receiver_clear_out + ); + +endmodule + + +// Per-bit inertial delay model used to sweep relative async channel timing in +// simulation without changing the production DUT hierarchy. +module cc_cdc_2phase_clearable_tb_bit_delay #( + parameter int unsigned MAX_DELAY_PS = 0 +)( + input logic in_i, + output logic out_o +); + + timeunit 1ns; + timeprecision 1ps; + + initial begin + out_o = 1'b0; + end + + always @(in_i) begin + automatic int unsigned delay_ps; + delay_ps = (MAX_DELAY_PS == 0) ? 0 : $urandom_range(0, MAX_DELAY_PS); + out_o <= #(delay_ps * 1ps) in_i; end endmodule -module cc_cdc_2phase_clearable_tb_delay_injector #( - parameter time MAX_DELAY = 0ns, - parameter int SYNC_STAGES = 3 +// Bus delay wrapper that applies independent random per-bit delay. This stresses +// bundled payload and phase buses under the same async timing assumptions. +module cc_cdc_2phase_clearable_tb_bus_delay #( + parameter int unsigned Width = 1, + parameter int unsigned MAX_DELAY_PS = 0 +)( + input logic [Width-1:0] in_i, + output logic [Width-1:0] out_o +); + + timeunit 1ns; + timeprecision 1ps; + + for (genvar i = 0; i < Width; i++) begin : gen_bit_delay + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_delay ( + .in_i ( in_i[i] ), + .out_o ( out_o[i] ) + ); + end + +endmodule + + +// Timed test harness equivalent to the clearable DUT, but with explicit delay +// elements inserted on all payload and reset-controller async wires. +module cc_cdc_2phase_clearable_tb_delay_injector + import cc_pkg::*; +#( + parameter int unsigned SYNC_STAGES = 3, + parameter bit CLEAR_ON_ASYNC_RESET = 1'b1, + parameter int unsigned MAX_DELAY_PS = 0 )( input logic src_rst_ni, input logic src_clk_i, @@ -304,83 +844,326 @@ module cc_cdc_2phase_clearable_tb_delay_injector #( input logic dst_ready_i ); - logic async_req_o, async_req_i; - logic async_ack_o, async_ack_i; - logic [31:0] async_data_o, async_data_i; + timeunit 1ns; + timeprecision 1ps; + localparam int unsigned ClearPhaseWidth = $bits(cdc_clear_seq_phase_e); - logic s_src_clear; - logic s_src_ready; - logic s_dst_clear; - logic s_dst_valid; + logic async_payload_req_from_src; + logic async_payload_req_to_dst; + logic async_payload_ack_from_dst; + logic async_payload_ack_to_src; + logic [31:0] async_payload_data_from_src; + logic [31:0] async_payload_data_to_dst; - always @(async_req_o) begin - automatic time d = $urandom_range(1ps, MAX_DELAY); - async_req_i <= #d async_req_o; - end + cdc_clear_seq_phase_e async_reset_src2dst_next_phase_from_src; + cdc_clear_seq_phase_e async_reset_src2dst_next_phase_to_dst; + cdc_clear_seq_phase_e async_reset_dst2src_next_phase_from_dst; + cdc_clear_seq_phase_e async_reset_dst2src_next_phase_to_src; + logic [ClearPhaseWidth-1:0] async_reset_src2dst_next_phase_from_src_bits; + logic [ClearPhaseWidth-1:0] async_reset_src2dst_next_phase_to_dst_bits; + logic [ClearPhaseWidth-1:0] async_reset_dst2src_next_phase_from_dst_bits; + logic [ClearPhaseWidth-1:0] async_reset_dst2src_next_phase_to_src_bits; + logic async_reset_src2dst_req_from_src; + logic async_reset_src2dst_req_to_dst; + logic async_reset_dst2src_ack_from_dst; + logic async_reset_dst2src_ack_to_src; + logic async_reset_dst2src_req_from_dst; + logic async_reset_dst2src_req_to_src; + logic async_reset_src2dst_ack_from_src; + logic async_reset_src2dst_ack_to_dst; - always @(async_ack_o) begin - automatic time d = $urandom_range(1ps, MAX_DELAY); - async_ack_i <= #d async_ack_o; - end + assign async_reset_src2dst_next_phase_from_src_bits = async_reset_src2dst_next_phase_from_src; + assign async_reset_src2dst_next_phase_to_dst = + cdc_clear_seq_phase_e'(async_reset_src2dst_next_phase_to_dst_bits); + assign async_reset_dst2src_next_phase_from_dst_bits = async_reset_dst2src_next_phase_from_dst; + assign async_reset_dst2src_next_phase_to_src = + cdc_clear_seq_phase_e'(async_reset_dst2src_next_phase_to_src_bits); - for (genvar i = 0; i < 32; i++) begin - always @(async_data_o[i]) begin - automatic time d = $urandom_range(1ps, MAX_DELAY); - async_data_i[i] <= #d async_data_o[i]; - end - end + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_payload_req_delay ( + .in_i ( async_payload_req_from_src ), + .out_o ( async_payload_req_to_dst ) + ); + + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_payload_ack_delay ( + .in_i ( async_payload_ack_from_dst ), + .out_o ( async_payload_ack_to_src ) + ); - cc_cdc_2phase_src_clearable #(logic [31:0], SYNC_STAGES) i_src ( - .rst_ni ( src_rst_ni ), - .clk_i ( src_clk_i ), - .clear_i ( s_src_clear ), - .data_i ( src_data_i ), - .valid_i ( src_valid_i & !s_src_clear ), - .ready_o ( s_src_ready ), - .async_req_o ( async_req_o ), - .async_ack_i ( async_ack_i ), - .async_data_o ( async_data_o ) + cc_cdc_2phase_clearable_tb_bus_delay #( + .Width ( 32 ), + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_payload_data_delay ( + .in_i ( async_payload_data_from_src ), + .out_o ( async_payload_data_to_dst ) ); - assign src_ready_o = s_src_ready & !s_src_clear; - - cc_cdc_2phase_dst_clearable #(logic [31:0], SYNC_STAGES) i_dst ( - .rst_ni ( dst_rst_ni ), - .clk_i ( dst_clk_i ), - .clear_i ( s_dst_clear ), - .data_o ( dst_data_o ), - .valid_o ( s_dst_valid ), - .ready_i ( dst_ready_i & !s_dst_clear ), - .async_req_i ( async_req_i ), - .async_ack_o ( async_ack_o ), - .async_data_i ( async_data_i ) + cc_cdc_2phase_clearable_tb_bus_delay #( + .Width ( ClearPhaseWidth ), + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_reset_src2dst_next_phase_delay ( + .in_i ( async_reset_src2dst_next_phase_from_src_bits ), + .out_o ( async_reset_src2dst_next_phase_to_dst_bits ) ); - assign dst_valid_o = s_dst_valid & !s_dst_clear; - - // Synchronize the clear and reset signaling in both directions (see header of - // the cc_cdc_reset_ctrlr module for more details.) - cc_cdc_reset_ctrlr #( - .SYNC_STAGES(SYNC_STAGES-1) - ) i_cdc_reset_ctrlr ( - .a_clk_i ( src_clk_i ), - .a_rst_ni ( src_rst_ni ), - .a_clear_i ( src_clear_i ), - .a_clear_o ( s_src_clear ), - .a_clear_ack_i ( '0 ), - .a_isolate_o ( ), - .a_isolate_ack_i( '0 ), - .b_clk_i ( dst_clk_i ), - .b_rst_ni ( dst_rst_ni ), - .b_clear_i ( dst_clear_i ), - .b_clear_o ( s_dst_clear ), - .b_clear_ack_i ( '0 ), - .b_isolate_o ( ), - .b_isolate_ack_i( '0 ) + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_reset_src2dst_req_delay ( + .in_i ( async_reset_src2dst_req_from_src ), + .out_o ( async_reset_src2dst_req_to_dst ) ); - assign src_clear_pending_o = s_src_clear; - assign dst_clear_pending_o = s_dst_clear; + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_reset_dst2src_ack_delay ( + .in_i ( async_reset_dst2src_ack_from_dst ), + .out_o ( async_reset_dst2src_ack_to_src ) + ); + + cc_cdc_2phase_clearable_tb_bus_delay #( + .Width ( ClearPhaseWidth ), + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_reset_dst2src_next_phase_delay ( + .in_i ( async_reset_dst2src_next_phase_from_dst_bits ), + .out_o ( async_reset_dst2src_next_phase_to_src_bits ) + ); + + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_reset_dst2src_req_delay ( + .in_i ( async_reset_dst2src_req_from_dst ), + .out_o ( async_reset_dst2src_req_to_src ) + ); + + cc_cdc_2phase_clearable_tb_bit_delay #( + .MAX_DELAY_PS ( MAX_DELAY_PS ) + ) i_async_reset_src2dst_ack_delay ( + .in_i ( async_reset_src2dst_ack_from_src ), + .out_o ( async_reset_src2dst_ack_to_dst ) + ); + + // Reuse the production source and destination domain wrappers. The harness + // only inserts timing delays on the explicit async wires between them. + cc_cdc_2phase_src_domain_clearable #( + .T ( logic [31:0] ), + .SYNC_STAGES ( SYNC_STAGES ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_src_domain ( + .src_rst_ni, + .src_clk_i, + .src_clear_i, + .src_clear_pending_o, + .src_data_i, + .src_valid_i, + .src_ready_o, + .async_payload_req_o ( async_payload_req_from_src ), + .async_payload_ack_i ( async_payload_ack_to_src ), + .async_payload_data_o ( async_payload_data_from_src ), + .async_reset_next_phase_o ( async_reset_src2dst_next_phase_from_src ), + .async_reset_req_o ( async_reset_src2dst_req_from_src ), + .async_reset_ack_i ( async_reset_dst2src_ack_to_src ), + .async_reset_next_phase_i ( async_reset_dst2src_next_phase_to_src ), + .async_reset_req_i ( async_reset_dst2src_req_to_src ), + .async_reset_ack_o ( async_reset_src2dst_ack_from_src ) + ); + + cc_cdc_2phase_dst_domain_clearable #( + .T ( logic [31:0] ), + .SYNC_STAGES ( SYNC_STAGES ), + .CLEAR_ON_ASYNC_RESET ( CLEAR_ON_ASYNC_RESET ) + ) i_dst_domain ( + .dst_rst_ni, + .dst_clk_i, + .dst_clear_i, + .dst_clear_pending_o, + .dst_data_o, + .dst_valid_o, + .dst_ready_i, + .async_payload_req_i ( async_payload_req_to_dst ), + .async_payload_ack_o ( async_payload_ack_from_dst ), + .async_payload_data_i ( async_payload_data_to_dst ), + .async_reset_next_phase_o ( async_reset_dst2src_next_phase_from_dst ), + .async_reset_req_o ( async_reset_dst2src_req_from_dst ), + .async_reset_ack_i ( async_reset_src2dst_ack_to_dst ), + .async_reset_next_phase_i ( async_reset_src2dst_next_phase_to_dst ), + .async_reset_req_i ( async_reset_src2dst_req_to_dst ), + .async_reset_ack_o ( async_reset_dst2src_ack_from_dst ) + ); + +endmodule + + +// Lightweight checker for reset-controller half internals. This is deliberately +// local-clock only and checks invariants that should hold after every edge. +module cc_cdc_reset_ctrlr_half_monitor + import cc_pkg::*; +( + input logic clk_i, + input logic rst_ni, + input logic isolate_o, + input logic isolate_ack_i, + input logic clear_o, + input logic clear_ack_i, + input cdc_clear_seq_phase_e async_next_phase_o, + input logic async_req_o, + input cdc_clear_seq_phase_e async_next_phase_i, + input logic async_req_i, + input logic [3:0] initiator_state_q, + input cdc_clear_seq_phase_e initiator_clear_seq_phase, + input logic initiator_phase_transition_req, + input logic initiator_isolate_out, + input logic initiator_clear_out, + input cdc_clear_seq_phase_e receiver_phase_q, + input cdc_clear_seq_phase_e receiver_next_phase, + input logic receiver_phase_req, + input logic receiver_phase_ack, + input logic receiver_isolate_out, + input logic receiver_clear_out +); + + timeunit 1ns; + timeprecision 1ps; + + localparam logic [3:0] InitIdle = 4'd0; + localparam logic [3:0] InitIsolate = 4'd1; + localparam logic [3:0] InitWaitIsolatePhaseAck = 4'd2; + localparam logic [3:0] InitWaitIsolateAck = 4'd3; + localparam logic [3:0] InitClear = 4'd4; + localparam logic [3:0] InitWaitClearPhaseAck = 4'd5; + localparam logic [3:0] InitWaitClearAck = 4'd6; + localparam logic [3:0] InitPostClear = 4'd7; + localparam logic [3:0] InitFinished = 4'd8; + + function automatic bit valid_phase(input cdc_clear_seq_phase_e phase); + return phase inside { + CDC_CLEAR_PHASE_IDLE, + CDC_CLEAR_PHASE_ISOLATE, + CDC_CLEAR_PHASE_CLEAR, + CDC_CLEAR_PHASE_POST_CLEAR + }; + endfunction + + function automatic bit valid_initiator_state(input logic [3:0] state); + return state inside { + InitIdle, + InitIsolate, + InitWaitIsolatePhaseAck, + InitWaitIsolateAck, + InitClear, + InitWaitClearPhaseAck, + InitWaitClearAck, + InitPostClear, + InitFinished + }; + endfunction + + task automatic check_stable_outputs; + if (clear_o && !isolate_o) begin + $error("%m: clear_o asserted without isolate_o"); + end + + if (initiator_clear_out && !initiator_isolate_out) begin + $error("%m: initiator clear asserted without initiator isolate"); + end + + if (receiver_clear_out && !receiver_isolate_out) begin + $error("%m: receiver clear asserted without receiver isolate"); + end + + if (clear_o !== (initiator_clear_out || receiver_clear_out)) begin + $error("%m: clear_o does not match initiator/receiver clear outputs"); + end + + if (isolate_o !== (initiator_isolate_out || receiver_isolate_out)) begin + $error("%m: isolate_o does not match initiator/receiver isolate outputs"); + end + + if (async_req_o && !valid_phase(async_next_phase_o)) begin + $error("%m: outgoing clear phase is illegal"); + end + + if (initiator_phase_transition_req && !valid_phase(initiator_clear_seq_phase)) begin + $error("%m: initiator requested an illegal clear phase"); + end + + if (receiver_phase_req) begin + unique case (receiver_next_phase) + CDC_CLEAR_PHASE_IDLE: begin + if (receiver_clear_out || receiver_isolate_out || !receiver_phase_ack) begin + $error("%m: receiver IDLE phase outputs are inconsistent"); + end + end + CDC_CLEAR_PHASE_ISOLATE: begin + if (receiver_clear_out || !receiver_isolate_out || + (receiver_phase_ack !== isolate_ack_i)) begin + $error("%m: receiver ISOLATE phase outputs are inconsistent"); + end + end + CDC_CLEAR_PHASE_CLEAR: begin + if (!receiver_clear_out || !receiver_isolate_out || + (receiver_phase_ack !== clear_ack_i)) begin + $error("%m: receiver CLEAR phase outputs are inconsistent"); + end + end + CDC_CLEAR_PHASE_POST_CLEAR: begin + if (receiver_clear_out || !receiver_isolate_out || !receiver_phase_ack) begin + $error("%m: receiver POST_CLEAR phase outputs are inconsistent"); + end + end + default: begin + if (receiver_clear_out || receiver_isolate_out || receiver_phase_ack) begin + $error("%m: receiver illegal phase was acknowledged or exposed"); + end + end + endcase + end + endtask + + always @(posedge clk_i) begin + if (rst_ni) begin + #1ps; + check_stable_outputs(); + + if (!valid_initiator_state(initiator_state_q)) begin + $error("%m: illegal initiator FSM state 0x%0h", initiator_state_q); + end + + if (!valid_phase(receiver_phase_q)) begin + $error("%m: illegal stored receiver phase 0x%0h", receiver_phase_q); + end + + if (initiator_state_q inside { + InitClear, + InitWaitClearPhaseAck, + InitWaitClearAck + }) begin + if (!initiator_clear_out || !initiator_isolate_out) begin + $error("%m: initiator clear state without clear/isolate outputs"); + end + end + + if (initiator_state_q inside { + InitIsolate, + InitWaitIsolatePhaseAck, + InitWaitIsolateAck, + InitPostClear, + InitFinished + }) begin + if (!initiator_isolate_out || initiator_clear_out) begin + $error("%m: initiator isolate-only state has inconsistent outputs"); + end + end + + if (initiator_state_q == InitIdle) begin + if (initiator_isolate_out || initiator_clear_out || initiator_phase_transition_req) begin + $error("%m: initiator IDLE state has active clear outputs or phase request"); + end + end + end + end endmodule diff --git a/test/simulate_cdc_clearable.sh b/test/simulate_cdc_clearable.sh new file mode 100755 index 00000000..1230bfc2 --- /dev/null +++ b/test/simulate_cdc_clearable.sh @@ -0,0 +1,154 @@ +#!/usr/bin/env bash +# Copyright 2026 ETH Zurich and University of Bologna. +# +# Copyright and related rights are licensed under the Solderpad Hardware +# License, Version 0.51 (the "License"); you may not use this file except in +# compliance with the License. You may obtain a copy of the License at +# http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +# or agreed to in writing, software, hardware and materials distributed under +# this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +# CONDITIONS OF ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the License. +# +# Authors: +# - Philippe Sauter +# +# Description: Clearable Two-Phase CDC Simulation Sweep +# Compile the test target and run plain plus timed-delay Questa regressions for +# cc_cdc_2phase_clearable. + +set -euo pipefail + +: "${VSIM:=vsim}" + +bender script vsim -t test > compile.cdc_clearable.tcl +"${VSIM}" -c -quiet -do 'source compile.cdc_clearable.tcl; quit' + +call_vsim() { + local name="$1" + shift + echo "== ${name} ==" + # Questa 10.7 reports the enum-typed RESET_MSG parameter default in + # cc_cdc_4phase_src as a suppressible elaboration error, even though the + # reset controller overrides it with an enum value. + "${VSIM}" -c -quiet cc_cdc_2phase_clearable_tb -suppress 8386 "$@" -do 'run -all; quit -f' | + tee "vsim.${name}.log" + grep "Errors: 0," "vsim.${name}.log" +} + +call_vsim smoke_default \ + -gSEED=1 \ + -gNUM_RANDOM_TRANSFERS=100 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=120 \ + -gNUM_ACTIVE_STRESS_EVENTS=8 + +call_vsim src_fast \ + -gSEED=2 \ + -gNUM_RANDOM_TRANSFERS=100 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=120 \ + -gNUM_ACTIVE_STRESS_EVENTS=8 \ + -gTCK_SRC_PS=5000 \ + -gTCK_DST_PS=17000 + +call_vsim dst_fast \ + -gSEED=3 \ + -gNUM_RANDOM_TRANSFERS=100 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=120 \ + -gNUM_ACTIVE_STRESS_EVENTS=8 \ + -gTCK_SRC_PS=17000 \ + -gTCK_DST_PS=5000 + +call_vsim no_async_reset_sync_only \ + -gSEED=4 \ + -gCLEAR_ON_ASYNC_RESET=0 \ + -gSYNC_STAGES=2 \ + -gNUM_RANDOM_TRANSFERS=100 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=120 \ + -gNUM_ACTIVE_STRESS_EVENTS=8 + +call_vsim timed_balanced_250ps \ + -gSEED=11 \ + -gNUM_RANDOM_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_EVENTS=4 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=250 \ + -gTCK_SRC_PS=10000 \ + -gTCK_DST_PS=10000 + +call_vsim timed_src_fast_800ps \ + -gSEED=12 \ + -gNUM_RANDOM_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_EVENTS=4 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=800 \ + -gTCK_SRC_PS=5000 \ + -gTCK_DST_PS=17000 + +call_vsim timed_dst_fast_800ps \ + -gSEED=13 \ + -gNUM_RANDOM_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_EVENTS=4 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=800 \ + -gTCK_SRC_PS=17000 \ + -gTCK_DST_PS=5000 + +call_vsim timed_no_async_reset_sync_only \ + -gSEED=10 \ + -gCLEAR_ON_ASYNC_RESET=0 \ + -gSYNC_STAGES=2 \ + -gNUM_RANDOM_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=60 \ + -gNUM_ACTIVE_STRESS_EVENTS=4 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=800 + +call_vsim timed_balanced_offset_1800ps \ + -gSEED=14 \ + -gNUM_RANDOM_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_EVENTS=5 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=1800 \ + -gTCK_SRC_PS=10000 \ + -gTCK_DST_PS=10000 \ + -gDST_START_DELAY_PS=2500 + +call_vsim timed_relprime_offset_2200ps \ + -gSEED=15 \ + -gNUM_RANDOM_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_EVENTS=5 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=2200 \ + -gTCK_SRC_PS=7000 \ + -gTCK_DST_PS=11000 \ + -gSRC_START_DELAY_PS=1500 \ + -gDST_START_DELAY_PS=3300 + +call_vsim timed_src_fast_near_bound \ + -gSEED=16 \ + -gNUM_RANDOM_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_EVENTS=5 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=4500 \ + -gTCK_SRC_PS=5000 \ + -gTCK_DST_PS=17000 \ + -gSRC_START_DELAY_PS=1000 \ + -gDST_START_DELAY_PS=2500 + +call_vsim timed_dst_fast_near_bound \ + -gSEED=17 \ + -gNUM_RANDOM_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_TRANSFERS=80 \ + -gNUM_ACTIVE_STRESS_EVENTS=5 \ + -gINJECT_DELAYS=1 \ + -gMAX_DELAY_PS=4500 \ + -gTCK_SRC_PS=17000 \ + -gTCK_DST_PS=5000 \ + -gSRC_START_DELAY_PS=2500 \ + -gDST_START_DELAY_PS=1000