vj 0.2.0

//! The SDF `TIMINGCHECK` -> SystemVerilog timing check mapping (IEEE 1800-2023 Table 32-2,
//! LRM 32.4.2), as data: which SystemVerilog checks one SDF check annotates, and which of the
//! SDF check's values lands in which of their limits. Matching a check against the design is
//! [`crate::sdf_apply`]'s job; this module is the table, so it can be pinned row by row.
//!
//! Table 32-2 (`v1` is the SDF check's first value, `v2` its second, `x` a limit the SDF check
//! does not annotate and therefore leaves alone):
//!
//! | SDF check          | SystemVerilog checks annotated                          |
//! |--------------------|---------------------------------------------------------|
//! | `SETUP v1`         | `$setup(v1)`, `$setuphold(v1, x)`                       |
//! | `HOLD v1`          | `$hold(v1)`, `$setuphold(x, v1)`                        |
//! | `SETUPHOLD v1 v2`  | `$setup(v1)`, `$hold(v2)`, `$setuphold(v1, v2)`         |
//! | `RECOVERY v1`      | `$recovery(v1)`, `$recrem(v1, x)`                       |
//! | `REMOVAL v1`       | `$removal(v1)`, `$recrem(x, v1)`                        |
//! | `RECREM v1 v2`     | `$recovery(v1)`, `$removal(v2)`, `$recrem(v1, v2)`      |
//! | `SKEW v1`          | `$skew(v1)`, `$timeskew(v1)`                            |
//! | `BIDIRECTSKEW v1 v2` | `$fullskew(v1, v2)`                                   |
//! | `WIDTH v1`         | `$width(v1, x)`                                         |
//! | `PERIOD v1`        | `$period(v1)`                                           |
//! | `NOCHANGE v1 v2`   | `$nochange(v1, v2)`                                     |
//!
//! **Implementation-defined: which SDF port is the reference.** IEEE 1497 (SDF 3.0), not the
//! LRM, defines the order of a check's two ports. This build reads the first port as the DATA
//! event and the second as the REFERENCE event for `SETUP`, `HOLD`, `SETUPHOLD`, `RECOVERY`,
//! `REMOVAL`, `RECREM` and `NOCHANGE` (the LRM's own 32.4.2 examples write
//! `(SETUPHOLD data (posedge clk) ...)`), and the first as the REFERENCE and the second as the
//! DATA event for `SKEW` and `BIDIRECTSKEW` (SDF's `(SKEW (posedge clk1) (posedge clk2) v)`,
//! the SystemVerilog `$skew(reference, data, limit)` order). `WIDTH` and `PERIOD` have one port,
//! the reference.

use vj_sdf::ast::CheckKind;
use vj_sim::netlist::specify::CheckArgs;

/// A SystemVerilog timing check kind an SDF check can annotate.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) enum SvCheck {
    Setup,
    Hold,
    SetupHold,
    Recovery,
    Removal,
    RecRem,
    Skew,
    TimeSkew,
    FullSkew,
    Width,
    Period,
    NoChange,
}

impl SvCheck {
    /// The kind of a decoded check.
    pub(crate) fn of(args: &CheckArgs) -> SvCheck {
        match args {
            CheckArgs::Setup(_) => SvCheck::Setup,
            CheckArgs::Hold(_) => SvCheck::Hold,
            CheckArgs::SetupHold(_) => SvCheck::SetupHold,
            CheckArgs::Recovery(_) => SvCheck::Recovery,
            CheckArgs::Removal(_) => SvCheck::Removal,
            CheckArgs::RecRem(_) => SvCheck::RecRem,
            CheckArgs::Skew(_) => SvCheck::Skew,
            CheckArgs::TimeSkew(_) => SvCheck::TimeSkew,
            CheckArgs::FullSkew(_) => SvCheck::FullSkew,
            CheckArgs::Width(_) => SvCheck::Width,
            CheckArgs::Period(_) => SvCheck::Period,
            CheckArgs::NoChange(_) => SvCheck::NoChange,
        }
    }

    /// The check as the LRM names it, for the annotation log.
    pub(crate) fn name(self) -> &'static str {
        match self {
            SvCheck::Setup => "$setup",
            SvCheck::Hold => "$hold",
            SvCheck::SetupHold => "$setuphold",
            SvCheck::Recovery => "$recovery",
            SvCheck::Removal => "$removal",
            SvCheck::RecRem => "$recrem",
            SvCheck::Skew => "$skew",
            SvCheck::TimeSkew => "$timeskew",
            SvCheck::FullSkew => "$fullskew",
            SvCheck::Width => "$width",
            SvCheck::Period => "$period",
            SvCheck::NoChange => "$nochange",
        }
    }
}

/// One row cell of Table 32-2: an SV check and, for each limit the SDF check annotates in it,
/// `(index into the SDF check's values, the SV check's limit slot)`. A slot is numbered in the
/// order of the SystemVerilog check's own limits (`CheckArgs::limits_mut`): `$setuphold`
/// (setup, hold), `$recrem` (recovery, removal), `$fullskew` (reference first, data first),
/// `$nochange` (start, end), and slot 0 of every other check.
pub(crate) struct Target {
    pub(crate) check: SvCheck,
    pub(crate) slots: &'static [(usize, usize)],
}

fn t(check: SvCheck, slots: &'static [(usize, usize)]) -> Target {
    Target { check, slots }
}

/// Table 32-2's row for the SDF check `kind`.
pub(crate) fn fan_out(kind: CheckKind) -> Vec<Target> {
    use SvCheck as S;
    match kind {
        CheckKind::Setup => vec![t(S::Setup, &[(0, 0)]), t(S::SetupHold, &[(0, 0)])],
        CheckKind::Hold => vec![t(S::Hold, &[(0, 0)]), t(S::SetupHold, &[(0, 1)])],
        CheckKind::SetupHold => vec![
            t(S::Setup, &[(0, 0)]),
            t(S::Hold, &[(1, 0)]),
            t(S::SetupHold, &[(0, 0), (1, 1)]),
        ],
        CheckKind::Recovery => vec![t(S::Recovery, &[(0, 0)]), t(S::RecRem, &[(0, 0)])],
        CheckKind::Removal => vec![t(S::Removal, &[(0, 0)]), t(S::RecRem, &[(0, 1)])],
        CheckKind::Recrem => vec![
            t(S::Recovery, &[(0, 0)]),
            t(S::Removal, &[(1, 0)]),
            t(S::RecRem, &[(0, 0), (1, 1)]),
        ],
        CheckKind::Skew => vec![t(S::Skew, &[(0, 0)]), t(S::TimeSkew, &[(0, 0)])],
        CheckKind::BidirectSkew => vec![t(S::FullSkew, &[(0, 0), (1, 1)])],
        CheckKind::Width => vec![t(S::Width, &[(0, 0)])],
        CheckKind::Period => vec![t(S::Period, &[(0, 0)])],
        CheckKind::NoChange => vec![t(S::NoChange, &[(0, 0), (1, 1)])],
    }
}

/// How many values the SDF check carries (what [`Target::slots`]' indices need).
pub(crate) fn value_count(kind: CheckKind) -> usize {
    match kind {
        CheckKind::SetupHold
        | CheckKind::Recrem
        | CheckKind::BidirectSkew
        | CheckKind::NoChange => 2,
        CheckKind::Setup
        | CheckKind::Hold
        | CheckKind::Recovery
        | CheckKind::Removal
        | CheckKind::Skew
        | CheckKind::Width
        | CheckKind::Period => 1,
    }
}

/// The SDF check's name as SDF spells it, for warnings.
pub(crate) fn sdf_name(kind: CheckKind) -> &'static str {
    match kind {
        CheckKind::Setup => "SETUP",
        CheckKind::Hold => "HOLD",
        CheckKind::SetupHold => "SETUPHOLD",
        CheckKind::Recovery => "RECOVERY",
        CheckKind::Removal => "REMOVAL",
        CheckKind::Recrem => "RECREM",
        CheckKind::Skew => "SKEW",
        CheckKind::BidirectSkew => "BIDIRECTSKEW",
        CheckKind::Width => "WIDTH",
        CheckKind::Period => "PERIOD",
        CheckKind::NoChange => "NOCHANGE",
    }
}

/// Whether the SDF check's FIRST port is the data event (see the module doc); the second is then
/// the reference. `WIDTH` and `PERIOD` have a single port, the reference.
pub(crate) fn first_port_is_data(kind: CheckKind) -> bool {
    !matches!(
        kind,
        CheckKind::Skew | CheckKind::BidirectSkew | CheckKind::Width | CheckKind::Period
    )
}

#[cfg(test)]
mod tests {
    use super::*;

    fn row(kind: CheckKind) -> Vec<(&'static str, Vec<(usize, usize)>)> {
        fan_out(kind)
            .iter()
            .map(|t| (t.check.name(), t.slots.to_vec()))
            .collect()
    }

    /// Table 32-2, row by row: a value lands in exactly the limits the table gives, and a limit
    /// the SDF check names no value for (`x`) has no slot entry at all.
    #[test]
    fn table_32_2_rows() {
        assert_eq!(
            row(CheckKind::Setup),
            [("$setup", vec![(0, 0)]), ("$setuphold", vec![(0, 0)])]
        );
        assert_eq!(
            row(CheckKind::Hold),
            [("$hold", vec![(0, 0)]), ("$setuphold", vec![(0, 1)])]
        );
        assert_eq!(
            row(CheckKind::SetupHold),
            [
                ("$setup", vec![(0, 0)]),
                ("$hold", vec![(1, 0)]),
                ("$setuphold", vec![(0, 0), (1, 1)])
            ]
        );
        assert_eq!(
            row(CheckKind::Recovery),
            [("$recovery", vec![(0, 0)]), ("$recrem", vec![(0, 0)])]
        );
        assert_eq!(
            row(CheckKind::Removal),
            [("$removal", vec![(0, 0)]), ("$recrem", vec![(0, 1)])]
        );
        assert_eq!(
            row(CheckKind::Recrem),
            [
                ("$recovery", vec![(0, 0)]),
                ("$removal", vec![(1, 0)]),
                ("$recrem", vec![(0, 0), (1, 1)])
            ]
        );
        assert_eq!(
            row(CheckKind::Skew),
            [("$skew", vec![(0, 0)]), ("$timeskew", vec![(0, 0)])]
        );
        assert_eq!(
            row(CheckKind::BidirectSkew),
            [("$fullskew", vec![(0, 0), (1, 1)])]
        );
        assert_eq!(row(CheckKind::Width), [("$width", vec![(0, 0)])]);
        assert_eq!(row(CheckKind::Period), [("$period", vec![(0, 0)])]);
        assert_eq!(
            row(CheckKind::NoChange),
            [("$nochange", vec![(0, 0), (1, 1)])]
        );
    }

    /// Every value index the table uses exists in the SDF check.
    #[test]
    fn table_32_2_value_indices_are_in_range() {
        for kind in [
            CheckKind::Setup,
            CheckKind::Hold,
            CheckKind::SetupHold,
            CheckKind::Recovery,
            CheckKind::Removal,
            CheckKind::Recrem,
            CheckKind::Skew,
            CheckKind::BidirectSkew,
            CheckKind::Width,
            CheckKind::Period,
            CheckKind::NoChange,
        ] {
            for target in fan_out(kind) {
                for &(v, _) in target.slots {
                    assert!(v < value_count(kind), "{kind:?} -> {}", target.check.name());
                }
            }
        }
    }
}