vj 0.2.0

//! Negative timing checks (LRM 1800-2023 31.9), the parts that are not a check's own state
//! machine: the delay solver and the delayed copies of signals.
//!
//! # What 31.9.1 asks for
//!
//! A `$setuphold` / `$recrem` limit may be negative. The violation window then does not
//! straddle the reference edge, so the checks "generate delayed copies of the data and
//! reference signals ... The setup and hold times used internally are adjusted to shift the
//! violation window and make it overlap the reference signal." Every check on a delayed
//! signal (all of `$setup`, `$hold`, `$setuphold`, `$recovery`, `$removal`, `$recrem`,
//! `$width`, `$period`, `$nochange`; never `$skew` / `$fullskew` / `$timeskew`) then reads the
//! delayed copy with limits adjusted accordingly, so that its notifier toggles at the proper
//! moment (31.9.3).
//!
//! # The solver ([`solve`])
//!
//! For a check with data-first limit `f` (the setup limit, or `$recrem`'s removal limit) and
//! data-second limit `s` (the hold / recovery limit) on reference signal `R` and data signal
//! `D`, delayed by `dR` and `dD`, the window in delayed time is
//!
//! ```text
//! f' = f - (dD - dR)        s' = s + (dD - dR)        (f' + s' = f + s)
//! ```
//!
//! "Make it overlap the reference signal" means both stay at least [`MARGIN`] (one tick of
//! simulation precision, the `u` of the LRM's own table: 31.9.2's `dCP = 10.01` for a `-10`
//! setup limit is `10 + 0.01`). A window is "exclusive of the end points" and "windows smaller
//! than two units of simulation precision cannot yield timing violations", which is exactly
//! `f' >= u` and `s' >= u`. Each is a difference constraint:
//!
//! ```text
//! dD >= dR + (u - s)        dR >= dD + (u - f)        dR, dD >= 0
//! ```
//!
//! and the delays are the LEAST solution (the smallest delays that satisfy everything), found
//! by relaxing from zero. A positive cycle is the LRM's "mutually inconsistent" set: the
//! smallest-magnitude negative limit becomes 0 (ties: the first in check order, a check's
//! first limit before its second), a warning is issued, and the delays are recomputed, "until a
//! solution is reached". Only a check with a NEGATIVE limit constrains anything -- the delay is
//! for those; a check whose limits are all non-negative is left to the delayed signals the
//! others created -- so the worst case, every negative limit zeroed, constrains nothing and
//! needs no delay.
//!
//! # What T23b reads ([`DelayTable`])
//!
//! The table is the hand-off to the condition / notifier / option work of 31.9.2-31.9.4: per
//! signal its solved delay and where its delayed copies live, per negative check its
//! declared and effective limits and which of its two delayed signals transitions first
//! ([`DelayTable::first_of`], which decides where the timestamp / timecheck condition goes),
//! and whether the option of 31.9.4 is on ([`DelayTable::enabled`]; off, every delay is 0).

use std::collections::HashMap;

use vj_codegen::process_lower::SignalSlot;
use vj_sim::netlist::InstanceId;
use vj_sim::symid::SymbolId;

pub(crate) use vj_exec::timing::negtiming::Explicit;

use crate::primitives::Loc;

/// The one-tick margin `u` (see the module doc): the smallest window overlap a solved delay
/// leaves, "two units of simulation precision" for a whole window.
pub(crate) const MARGIN: i64 = 1;

/// Which of a check's two limits.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) enum Limit {
    /// The window for data BEFORE the reference edge (`$setuphold`'s setup, `$recrem`'s
    /// removal).
    DataFirst,
    /// The window for data AFTER the reference edge (`$setuphold`'s hold, `$recrem`'s
    /// recovery).
    DataSecond,
}

/// One `$setuphold` / `$recrem` as the solver sees it: two signals (indices into one node
/// numbering the caller owns) and the two limits, in ticks.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) struct Constraint {
    pub(crate) reference: usize,
    pub(crate) data: usize,
    pub(crate) data_first: i64,
    pub(crate) data_second: i64,
}

/// A limit [`solve`] had to set to 0 to reach a solution.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) struct Zeroed {
    /// Index into the constraints passed to [`solve`].
    pub(crate) check: usize,
    pub(crate) limit: Limit,
    /// The (negative) value it had.
    pub(crate) was: i64,
}

/// [`solve`]'s result.
#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct Solution {
    /// The delay of every node, in ticks (0 for a node no negative check mentions).
    pub(crate) delays: Vec<i64>,
    /// Each constraint's limits after any zeroing, `(data_first, data_second)`.
    pub(crate) effective: Vec<(i64, i64)>,
    /// The limits that were zeroed, in the order it was done.
    pub(crate) zeroed: Vec<Zeroed>,
}

/// The least delays satisfying every constraint that has a negative limit in `limits`, or
/// `None` when they are inconsistent (a positive cycle: the relaxation never settles).
fn least_delays(nodes: usize, checks: &[Constraint], limits: &[(i64, i64)]) -> Option<Vec<i64>> {
    let mut d = vec![0i64; nodes];
    for _ in 0..=nodes {
        let mut changed = false;
        for (c, &(first, second)) in checks.iter().zip(limits) {
            if first >= 0 && second >= 0 {
                continue;
            }
            // dD >= dR + (u - second);  dR >= dD + (u - first).
            for (from, to, w) in [
                (c.reference, c.data, MARGIN - second),
                (c.data, c.reference, MARGIN - first),
            ] {
                if d[to] < d[from] + w {
                    d[to] = d[from] + w;
                    changed = true;
                }
            }
        }
        if !changed {
            return Some(d);
        }
    }
    None
}

/// Solves the delays of `nodes` delayed signals for `checks` (see the module doc).
pub(crate) fn solve(nodes: usize, checks: &[Constraint]) -> Solution {
    let mut effective: Vec<(i64, i64)> = checks
        .iter()
        .map(|c| (c.data_first, c.data_second))
        .collect();
    let mut zeroed = Vec::new();
    loop {
        if let Some(delays) = least_delays(nodes, checks, &effective) {
            return Solution {
                delays,
                effective,
                zeroed,
            };
        }
        // Inconsistent: zero the smallest-magnitude negative limit (first on a tie).
        let mut best: Option<(i64, usize, Limit)> = None;
        for (i, &(first, second)) in effective.iter().enumerate() {
            for (v, limit) in [(first, Limit::DataFirst), (second, Limit::DataSecond)] {
                if v < 0 && best.is_none_or(|(magnitude, ..)| -v < magnitude) {
                    best = Some((-v, i, limit));
                }
            }
        }
        let (magnitude, check, limit) =
            best.expect("an inconsistent system has a negative limit: only those add constraints");
        zeroed.push(Zeroed {
            check,
            limit,
            was: -magnitude,
        });
        match limit {
            Limit::DataFirst => effective[check].0 = 0,
            Limit::DataSecond => effective[check].1 = 0,
        }
    }
}

/// Which of a check's two signals.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) enum Role {
    Reference,
    Data,
}

/// One signal that has delayed copies (31.9.1): the original, its solved delay and where the
/// copies are.
#[derive(Clone, Debug)]
pub(crate) struct DelayedSignal {
    pub(crate) instance: InstanceId,
    pub(crate) slot: SignalSlot,
    /// The solved delay in ticks; 0 when no negative limit asked for one.
    pub(crate) delay: i64,
    /// The nets the model declared for it. A signal with delayed copies uses the explicit one
    /// in every check that reads it (31.9.1 Example 3), never a second implicit one.
    pub(crate) explicit: Vec<Explicit>,
    /// The implicit, whole-signal copy, allocated only when a check needs one (a delayed
    /// signal no explicit net covers). Not nameable by the model.
    pub(crate) implicit: Option<Loc>,
}

/// What the solver decided about one `$setuphold` / `$recrem`.
#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct NegativeCheck {
    /// The check's position in `TimingModel::timing_checks`.
    pub(crate) entry: usize,
    pub(crate) check: SymbolId,
    pub(crate) reference: usize,
    pub(crate) data: usize,
    /// `(data_first, data_second)` as written.
    pub(crate) declared: (i64, i64),
    /// After zeroing an inconsistent negative limit.
    pub(crate) effective: (i64, i64),
}

/// The delayed signals of a design and the checks that use them: what 31.9.2's condition
/// association and 31.9.3's notifier timing read.
///
/// T23b reads, by signal (indices are the position in [`Self::signals`]):
///
/// * [`Self::delay_of`] / [`DelayedSignal::delay`]: the delay each signal was given -- the
///   `dCP / dD / dTI / dTE` of 31.9.2's table;
/// * [`Self::shadow_of`]: where a signal's delayed copy is, which is what a condition written
///   over the delayed signals sees and what the notifier timing is measured on;
/// * [`Self::first_of`]: which of a negative check's two delayed signals transitions first, so
///   which one carries its `timestamp_condition` (the other carries `timecheck_condition`).
///   A negative DATA-FIRST limit puts the data window after the reference, so the reference
///   transitions first; a negative data-second limit puts it before. `None` for a check with
///   no negative limit left: its order is whichever event arrives first, as for positive
///   limits.
#[derive(Clone, Debug, Default)]
pub(crate) struct DelayTable {
    pub(crate) signals: Vec<DelayedSignal>,
    index: HashMap<(InstanceId, SymbolId), usize>,
    pub(crate) checks: Vec<NegativeCheck>,
    /// The warnings the solve produced (inconsistent limits zeroed), to print once.
    pub(crate) warnings: Vec<String>,
    /// Whether the negative-timing-check option (LRM 31.9.4) is on. Off, every delay is 0 and
    /// [`crate::timingcheck`] clamps the negative limits of the checks it plans.
    pub(crate) enabled: bool,
}

impl DelayTable {
    /// An empty table for a run with the negative-timing-check option `enabled` or not.
    pub(crate) fn new(enabled: bool) -> DelayTable {
        DelayTable {
            enabled,
            ..DelayTable::default()
        }
    }

    /// The node of `signal` in `instance`, adding it when new.
    /// `owner` is the instance holding the signal's cell: `instance` itself, or the interface
    /// instance for a signal of an interface port (LRM 25.6).
    pub(crate) fn node(
        &mut self,
        instance: InstanceId,
        owner: InstanceId,
        signal: &SymbolId,
        slot: SignalSlot,
    ) -> usize {
        *self
            .index
            .entry((instance, signal.clone()))
            .or_insert_with(|| {
                self.signals.push(DelayedSignal {
                    instance: owner,
                    slot,
                    delay: 0,
                    explicit: Vec::new(),
                    implicit: None,
                });
                self.signals.len() - 1
            })
    }

    /// Records the declared delayed net `e` as a copy of node `node`'s signal (once: the same
    /// net named by several checks is one copy).
    pub(crate) fn add_explicit(&mut self, node: usize, e: Explicit) {
        let list = &mut self.signals[node].explicit;
        let known = list.iter().any(|x| {
            x.loc.inst == e.loc.inst
                && x.loc.slot.slot == e.loc.slot.slot
                && x.dst_lo == e.dst_lo
                && x.source_lo == e.source_lo
                && x.width == e.width
        });
        if !known {
            list.push(e);
        }
    }

    /// The node of `signal` if it has delayed copies.
    pub(crate) fn find(&self, instance: InstanceId, signal: &SymbolId) -> Option<usize> {
        self.index.get(&(instance, signal.clone())).copied()
    }

    /// The solved delay of `signal`, in ticks (0 for a signal with no delayed copy).
    pub(crate) fn delay_of(&self, instance: InstanceId, signal: &SymbolId) -> i64 {
        self.find(instance, signal)
            .map_or(0, |n| self.signals[n].delay)
    }

    /// Where the delayed copy covering bits `lo..lo + width` of `signal` is, with the bit of
    /// the copy that `lo` is; `None` when the signal has no delay (its checks read the
    /// original) or no copy has been made yet.
    pub(crate) fn shadow_of(
        &self,
        instance: InstanceId,
        signal: &SymbolId,
        lo: u32,
        width: u32,
    ) -> Option<(Loc, u32)> {
        let s = &self.signals[self.find(instance, signal)?];
        if s.delay == 0 {
            return None;
        }
        s.explicit
            .iter()
            .find(|e| e.source_lo <= lo && lo + width <= e.source_lo + e.width)
            .map(|e| (e.loc, lo - e.source_lo + e.dst_lo))
            .or_else(|| s.implicit.map(|loc| (loc, lo)))
    }

    /// Which signal of the negative check `check` transitions first (see the type doc).
    pub(crate) fn first_of(&self, check: &SymbolId) -> Option<Role> {
        let c = self.checks.iter().find(|c| &c.check == check)?;
        match c.effective {
            (first, _) if first < 0 => Some(Role::Reference),
            (_, second) if second < 0 => Some(Role::Data),
            _ => None,
        }
    }
}

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

    /// 31.9.2's example, in units of 0.01 (the precision its table is written in, so
    /// `MARGIN` is the table's `.01`): the four delays the LRM prints.
    #[test]
    fn the_lrm_31_9_2_delay_table_is_reproduced() {
        const CP: usize = 0;
        const D: usize = 1;
        const TI: usize = 2;
        const TE: usize = 3;
        let checks = [
            // $setuphold(posedge CP, D, -10, 20, ...)
            Constraint {
                reference: CP,
                data: D,
                data_first: -1000,
                data_second: 2000,
            },
            // $setuphold(posedge CP, TI, 20, -10, ...)
            Constraint {
                reference: CP,
                data: TI,
                data_first: 2000,
                data_second: -1000,
            },
            // $setuphold(posedge CP, TE, -4, 8, ...)
            Constraint {
                reference: CP,
                data: TE,
                data_first: -400,
                data_second: 800,
            },
        ];
        let s = solve(4, &checks);
        assert_eq!(s.zeroed, vec![], "the set is consistent");
        // dCP 10.01, dD 0.00, dTI 20.02, dTE 2.02.
        assert_eq!(s.delays, vec![1001, 0, 2002, 202]);
    }

    /// 31.9.1's first example: `$setuphold(posedge CLK, DATA, -10, 20)` delays CLK by the
    /// 10 the data window is late, plus the margin, and leaves DATA alone.
    #[test]
    fn example_1_delays_the_reference_by_the_negative_setup() {
        let s = solve(
            2,
            &[Constraint {
                reference: 0,
                data: 1,
                data_first: -10,
                data_second: 20,
            }],
        );
        assert_eq!(s.delays, vec![10 + MARGIN, 0]);
        assert_eq!(s.effective, vec![(-10, 20)]);
    }

    /// Example 2: two checks on one CLK, one delayed CLK for both; the larger magnitude
    /// decides it, and each data signal keeps its own delay (0).
    #[test]
    fn example_2_gives_one_delay_to_the_shared_reference() {
        let s = solve(
            3,
            &[
                Constraint {
                    reference: 0,
                    data: 1,
                    data_first: -10,
                    data_second: 20,
                },
                Constraint {
                    reference: 0,
                    data: 2,
                    data_first: -15,
                    data_second: 18,
                },
            ],
        );
        assert_eq!(s.delays, vec![15 + MARGIN, 0, 0]);
    }

    /// A negative hold limit delays the DATA instead (the window is before the reference).
    #[test]
    fn a_negative_hold_delays_the_data() {
        let s = solve(
            2,
            &[Constraint {
                reference: 0,
                data: 1,
                data_first: 20,
                data_second: -10,
            }],
        );
        assert_eq!(s.delays, vec![0, 10 + MARGIN]);
    }

    /// 31.9.1's `(CLK = Q) = 6` example: the larger magnitude of -3 and -7 is the delay, so
    /// the output is held to 7 (plus the margin) rather than 6.
    #[test]
    fn the_larger_negative_setup_of_two_checks_on_one_pair_wins() {
        let s = solve(
            2,
            &[
                Constraint {
                    reference: 0,
                    data: 1,
                    data_first: -3,
                    data_second: 8,
                },
                Constraint {
                    reference: 0,
                    data: 1,
                    data_first: -7,
                    data_second: 13,
                },
            ],
        );
        assert_eq!(s.delays, vec![7 + MARGIN, 0]);
    }

    /// A window that is empty (setup + hold < 2 ticks) is inconsistent on its own: the
    /// negative limit is zeroed and no delay is needed.
    #[test]
    fn an_empty_window_zeroes_its_negative_limit() {
        let s = solve(
            2,
            &[Constraint {
                reference: 0,
                data: 1,
                data_first: -10,
                data_second: 5,
            }],
        );
        assert_eq!(s.delays, vec![0, 0]);
        assert_eq!(s.effective, vec![(0, 5)]);
        assert_eq!(
            s.zeroed,
            vec![Zeroed {
                check: 0,
                limit: Limit::DataFirst,
                was: -10
            }]
        );
    }

    /// Mutually inconsistent checks: the SMALLEST-magnitude negative limit goes first, and
    /// once that leaves a solution the rest are kept. Two checks on the same pair with
    /// reversed roles each want the other signal later; the cycle through both is positive,
    /// so the -1 (smaller than -9) is zeroed and the -9 survives.
    #[test]
    fn the_smallest_magnitude_negative_limit_is_zeroed_first() {
        // check 0, reference 0 / data 1, (-9, 12): d0 >= d1 + 10, d1 >= d0 - 11.
        // check 1, reference 1 / data 0, (-1, 0):  d0 >= d1 + 1,  d1 >= d0 + 2.
        let s = solve(
            2,
            &[
                Constraint {
                    reference: 0,
                    data: 1,
                    data_first: -9,
                    data_second: 12,
                },
                Constraint {
                    reference: 1,
                    data: 0,
                    data_first: -1,
                    data_second: 0,
                },
            ],
        );
        assert_eq!(
            s.zeroed,
            vec![Zeroed {
                check: 1,
                limit: Limit::DataFirst,
                was: -1
            }]
        );
        assert_eq!(s.effective, vec![(-9, 12), (0, 0)]);
        assert_eq!(s.delays, vec![9 + MARGIN, 0]);
    }

    /// A tie goes to the first limit in check order, the first limit of a check before its
    /// second.
    #[test]
    fn a_tie_zeroes_the_first_limit_in_order() {
        let s = solve(
            2,
            &[Constraint {
                reference: 0,
                data: 1,
                data_first: -3,
                data_second: -3,
            }],
        );
        assert_eq!(s.zeroed[0].limit, Limit::DataFirst);
        // Zeroed to (0, -3): still empty, so the second goes too, and nothing is left.
        assert_eq!(s.effective, vec![(0, 0)]);
        assert_eq!(s.zeroed.len(), 2);
        assert_eq!(s.delays, vec![0, 0]);
    }

    /// A check with no negative limit adds no constraint, however small its window.
    #[test]
    fn non_negative_checks_do_not_constrain() {
        let s = solve(
            2,
            &[Constraint {
                reference: 0,
                data: 1,
                data_first: 0,
                data_second: 1,
            }],
        );
        assert_eq!(s.delays, vec![0, 0]);
        assert_eq!(s.zeroed, vec![]);
    }

    /// The same signal as both reference and data cannot be delayed relative to itself.
    #[test]
    fn a_check_of_a_signal_against_itself_is_zeroed() {
        let s = solve(
            1,
            &[Constraint {
                reference: 0,
                data: 0,
                data_first: -3,
                data_second: 8,
            }],
        );
        assert_eq!(s.delays, vec![0]);
        assert_eq!(s.effective, vec![(0, 8)]);
    }

    /// The solution satisfies every constraint with both adjusted limits at least the margin,
    /// and is the least one (lowering any positive delay by a tick breaks something).
    #[test]
    fn solutions_are_feasible_and_minimal() {
        let checks = [
            Constraint {
                reference: 0,
                data: 1,
                data_first: -6,
                data_second: 20,
            },
            Constraint {
                reference: 0,
                data: 2,
                data_first: -4,
                data_second: 20,
            },
            // A negative hold: the data (node 1) is delayed past the reference (node 3).
            Constraint {
                reference: 3,
                data: 1,
                data_first: 5,
                data_second: -2,
            },
        ];
        let s = solve(4, &checks);
        assert!(s.zeroed.is_empty());
        for (c, &(f, h)) in checks.iter().zip(&s.effective) {
            let delta = s.delays[c.data] - s.delays[c.reference];
            assert!(f - delta >= MARGIN, "{c:?}: setup' {}", f - delta);
            assert!(h + delta >= MARGIN, "{c:?}: hold' {}", h + delta);
        }
        for node in 0..4 {
            if s.delays[node] == 0 {
                continue;
            }
            let mut lower = s.delays.clone();
            lower[node] -= 1;
            let ok = checks.iter().zip(&s.effective).all(|(c, &(f, h))| {
                let delta = lower[c.data] - lower[c.reference];
                f - delta >= MARGIN && h + delta >= MARGIN
            });
            assert!(!ok, "node {node} could have been delayed less");
        }
    }
}