blob: 1940a9176599c902913356277875484bf4e858f0 [file] [log] [blame]
// Copyright lowRISC contributors.
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
// This contains SVA assertions for clock dividers.
// - For div2 (DIV == 2) the reference clk is io clock, which is never stepped.
// So when step_down check that the divided clock tracks the reference. This
// means we check at negedge, or we would see nothing interesting.
// - For div4 (DIV == 4) the reference clk is io_div2 clock, which is also stepped.
// So check it is always twice as slow, except during transitions.
//
// All checks at negedges for simplicity.
interface clkmgr_div_sva_if #(
parameter int DIV = 2
) (
input logic clk,
input logic rst_n,
input logic maybe_divided_clk,
input logic div_step_down_req_i,
input logic scanmode
);
localparam int WAIT_CYCLES = 20;
logic step_down;
always_comb step_down = div_step_down_req_i && !scanmode;
logic step_up;
always_comb step_up = !step_down;
sequence WholeLeadHigh_S;
step_down || maybe_divided_clk ##1 step_down || !maybe_divided_clk;
endsequence
sequence WholeLeadLow_S;
step_down || !maybe_divided_clk ##1 step_down || maybe_divided_clk;
endsequence
if (DIV == 2) begin : g_div2
sequence TracksClk_S; step_up || maybe_divided_clk ##1 step_up || maybe_divided_clk; endsequence
// Notice this fires at negedges, since maybe_divided_clk's value will be on when
// tracking.
`ASSERT(Div2Stepped_A, $rose(step_down) ##1 step_down [* WAIT_CYCLES] |-> TracksClk_S, !clk,
!rst_n)
`ASSERT(Div2Whole_A,
$fell(step_down) ##1 !step_down [* WAIT_CYCLES] |-> WholeLeadLow_S or WholeLeadHigh_S,
!clk, !rst_n)
end else begin : g_div4
sequence StepLeadHigh_S;
step_up || maybe_divided_clk ##1 step_up || !maybe_divided_clk;
endsequence
sequence StepLeadLow_S;
step_up || !maybe_divided_clk ##1 step_up || maybe_divided_clk;
endsequence
`ASSERT(Div4Stepped_A,
$rose(step_down) ##1 step_down [* WAIT_CYCLES] |-> StepLeadLow_S or StepLeadHigh_S,
!clk, !rst_n)
`ASSERT(Div4Whole_A,
$fell(step_down) ##1 !step_down [* WAIT_CYCLES] |-> WholeLeadLow_S or WholeLeadHigh_S,
!clk, !rst_n)
end
endinterface