[prim] Pulse Sync assertion to check input/output
Adding assertion to check the pulse is being generated
correctly.
Co-Authored-by: Timothy Chen <timothytim@google.com>
Signed-off-by: Eunchan Kim <eunchan@opentitan.org>
diff --git a/hw/ip/prim/rtl/prim_pulse_sync.sv b/hw/ip/prim/rtl/prim_pulse_sync.sv
index ad275fd..d6e51a2 100644
--- a/hw/ip/prim/rtl/prim_pulse_sync.sv
+++ b/hw/ip/prim/rtl/prim_pulse_sync.sv
@@ -32,6 +32,28 @@
end
end
+
+ // source active must come far enough such that the destination domain has time
+ // to create a valid pulse.
+`ifdef INC_ASSERT
+ logic src_active_flag;
+
+ // source active flag tracks whether there is an ongoing "toggle" event.
+ // Until this toggle event is accepted by the destination domain (negative edge of
+ // of the pulse output), the source side cannot toggle again.
+ always_ff @(posedge clk_src_i or negedge dst_pulse_o or negedge rst_src_ni) begin
+ if (!rst_src_ni) begin
+ src_active_flag <= '0;
+ end else if (!dst_pulse_o && src_active_flag) begin
+ src_active_flag <= '0;
+ end else if (src_pulse_i) begin
+ src_active_flag <= 1'b1;
+ end
+ end
+
+ `ASSERT(SrcPulseCheck_M, src_pulse_i |-> !src_active_flag, clk_src_i, !rst_src_ni)
+`endif
+
//////////////////////////////////////////////////////////
// synchronize level signal to destination clock domain //
//////////////////////////////////////////////////////////
@@ -63,4 +85,6 @@
// edge detection
assign dst_pulse_o = dst_level_q ^ dst_level;
+ `ASSERT(DstPulseCheck_A, dst_pulse_o |=> !dst_pulse_o, clk_dst_i, !rst_dst_ni)
+
endmodule
