vj_sim/sva/

future.rs

//! The global clocking FUTURE sampled value functions (LRM 1800-2023 16.9.4):
//! `$future_gclk`, `$rising_gclk`, `$falling_gclk`, `$steady_gclk`,
//! `$changing_gclk`, as a pure specification over sampled values.
//!
//! The past family (`$past_gclk` and friends) needs none of this: it is
//! literally `$past(v,,,@$global_clock)`, `$rose(v,@$global_clock)`, ... and
//! `sva::sampled` decodes it that way. The future family reads the sampled
//! value at the global clock tick that FOLLOWS the time step it is evaluated
//! in, so the value is not known until that tick; this module fixes what each
//! function returns once it is, and when the consumer may act on it:
//!
//! * the value of the expression "at the next tick" is its sampled
//!   (Preponed) value at the first global tick STRICTLY after the time step
//!   ([`first_tick_after`]), the mirror of `$past`'s "strictly before";
//! * `$rising_gclk`/`$falling_gclk` compare the LSB at that tick with the
//!   expression's own sampled value now, as `$rose`/`$fell` compare now with
//!   the previous tick; `$steady_gclk` is equality of the two, and
//!   `$changing_gclk` its complement;
//! * the evaluation attempt still ends at the last tick of the ASSERTION's
//!   clock, as though the future values were known in advance (so
//!   `disable iff` and `$assertcontrol` act only up to it), while its action
//!   block, and the default `$error`, run at the first global tick strictly
//!   after that ([`action_tick`]); a message that reports the attempt's end
//!   time reports the attempt's, not the action's. `sched::maturation::
//!   report_at_global_tick` is the scheduler half of the delay.
//!
//! Everything here is on a 4-state SCALAR (`b'0'`, `b'1'`, `b'x'`, `b'z'`),
//! the shape the LRM's tables and examples use; a wider expression is the
//! LSB for the edge functions and the whole value for equality, which the
//! caller reduces to `(lsb, equal)` before it gets here.

/// A simulation time, in the units of the global clock's tick list.
pub type Tick = u64;

/// The five future functions.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum FutureFn {
    Future,
    Rising,
    Falling,
    Steady,
    Changing,
}

/// The first element of `ticks` (ascending global clock tick times) strictly
/// greater than `t`, or `None` when the clock does not tick again.
pub fn first_tick_after(ticks: &[Tick], t: Tick) -> Option<Tick> {
    ticks.iter().copied().find(|&g| g > t)
}

/// When the action block (or default `$error`) of an attempt that ended at
/// assertion-clock tick `attempt_end` runs: the global clock tick that follows
/// it (16.9.4). A tick at `attempt_end` itself does not count, which is why
/// the LRM's `a3` fails at 80 -- itself a global tick -- and reports at 90.
pub fn action_tick(global_ticks: &[Tick], attempt_end: Tick) -> Option<Tick> {
    first_tick_after(global_ticks, attempt_end)
}

/// The function's value given the expression's sampled value now (`cur`) and
/// at the next global tick (`next`), as `b'0'`/`b'1'` -- or, for
/// [`FutureFn::Future`], the next value itself.
pub fn eval(f: FutureFn, cur: u8, next: u8) -> u8 {
    let truth = |b: bool| if b { b'1' } else { b'0' };
    match f {
        FutureFn::Future => next,
        FutureFn::Rising => truth(next == b'1' && cur != b'1'),
        FutureFn::Falling => truth(next == b'0' && cur != b'0'),
        FutureFn::Steady => truth(cur == next),
        FutureFn::Changing => truth(cur != next),
    }
}

/// `samples[i]` is the sampled value at global tick `i`; the function at tick
/// `i`, or `None` for the last tick, whose successor does not exist (the
/// attempt cannot be evaluated: the simulation ends first).
pub fn eval_at(f: FutureFn, samples: &[u8], i: usize) -> Option<u8> {
    let next = *samples.get(i + 1)?;
    Some(eval(f, samples[i], next))
}

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

    /// The waveform of `sig` at the global ticks 0, 10, ..., 110 that Table
    /// 16-2 and Figure 16-4 describe. The figure is a drawing, so it is
    /// reconstructed from the table (its sampled values at 10, 30, 40, 50 and
    /// 80 and the futures they imply, i.e. the value at 20, 60 and 90) and
    /// from the text of Examples 1 and 3 (changes only on a falling clock, but
    /// at 80). The remaining samples are chosen to keep to that.
    const SIG: &[u8] = b"110000111000";
    /// `clk` (a period of 40) at the same ticks: high at 0..=10, low 20..=30,
    /// high 40..=50, ... falling between the ticks 10-20, 50-60 and 90-100.
    const CLK: &[u8] = b"110011001100";
    const TICKS: [Tick; 12] = [0, 10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110];

    fn at(time: Tick) -> usize {
        TICKS
            .iter()
            .position(|&t| t == time)
            .expect("a global tick")
    }

    fn row(time: Tick) -> [u8; 6] {
        let i = at(time);
        [
            SIG[i],
            eval_at(FutureFn::Future, SIG, i).unwrap(),
            eval_at(FutureFn::Rising, SIG, i).unwrap(),
            eval_at(FutureFn::Falling, SIG, i).unwrap(),
            eval_at(FutureFn::Changing, SIG, i).unwrap(),
            eval_at(FutureFn::Steady, SIG, i).unwrap(),
        ]
    }

    /// Table 16-2, all five rows, columns `$sampled`, `$future_gclk`,
    /// `$rising_gclk`, `$falling_gclk`, `$changing_gclk`, `$steady_gclk`.
    #[test]
    fn table_16_2_rows() {
        assert_eq!(&row(10), b"100110");
        assert_eq!(&row(30), b"000001");
        assert_eq!(&row(40), b"000001");
        assert_eq!(&row(50), b"011010");
        assert_eq!(&row(80), b"100110");
    }

    /// The last tick has no successor: nothing is evaluated there.
    #[test]
    fn the_last_tick_has_no_future() {
        assert_eq!(eval_at(FutureFn::Future, SIG, SIG.len() - 1), None);
        assert_eq!(eval_at(FutureFn::Steady, SIG, SIG.len() - 1), None);
        assert!(eval_at(FutureFn::Steady, SIG, SIG.len() - 2).is_some());
    }

    /// 4-state: an unknown on either side is neither a rise nor a fall, is
    /// `steady` only when both are the same unknown (case equality), and
    /// `changing` is always `steady`'s complement.
    #[test]
    fn four_state_edges_and_equality() {
        for (cur, next, rising, falling, steady) in [
            (b'0', b'1', b'1', b'0', b'0'),
            (b'1', b'0', b'0', b'1', b'0'),
            (b'x', b'1', b'1', b'0', b'0'),
            (b'1', b'x', b'0', b'0', b'0'),
            (b'x', b'0', b'0', b'1', b'0'),
            (b'x', b'x', b'0', b'0', b'1'),
            (b'z', b'x', b'0', b'0', b'0'),
            (b'1', b'1', b'0', b'0', b'1'),
        ] {
            let case = format!("{} -> {}", cur as char, next as char);
            assert_eq!(eval(FutureFn::Rising, cur, next), rising, "{case}");
            assert_eq!(eval(FutureFn::Falling, cur, next), falling, "{case}");
            assert_eq!(eval(FutureFn::Steady, cur, next), steady, "{case}");
            assert_eq!(eval(FutureFn::Changing, cur, next), steady ^ 1, "{case}");
            assert_eq!(eval(FutureFn::Future, cur, next), next, "{case}");
        }
    }

    /// The tick lookup is strictly-after, and absent past the last tick.
    #[test]
    fn first_tick_after_is_strict() {
        assert_eq!(first_tick_after(&TICKS, 80), Some(90));
        assert_eq!(first_tick_after(&TICKS, 85), Some(90));
        assert_eq!(first_tick_after(&TICKS, 79), Some(80));
        assert_eq!(first_tick_after(&TICKS, 110), None);
        assert_eq!(first_tick_after(&[], 0), None);
    }

    /// The ticks at which Example 1's
    /// `a1: assert property (@$global_clock $changing_gclk(sig) |->
    /// $falling_gclk(clk))` is violated, given `rst` sampled at each tick
    /// (`disable iff (rst)`, Example 3, when `Some`).
    fn violations(rst: Option<&[u8]>) -> Vec<Tick> {
        (0..SIG.len())
            .filter(|&i| rst.is_none_or(|r| r[i] != b'1'))
            .filter(|&i| {
                let (Some(ch), Some(fall)) = (
                    eval_at(FutureFn::Changing, SIG, i),
                    eval_at(FutureFn::Falling, CLK, i),
                ) else {
                    return false;
                };
                ch == b'1' && fall != b'1'
            })
            .map(|i| TICKS[i])
            .collect()
    }

    /// Example 1: "The assertion a1 is violated at time 80 because
    /// `$changing_gclk(sig)` is true and `$falling_gclk(clk)` is false" -- and
    /// at no other tick -- and its `$error` is executed at time 90, while a
    /// message that reports the attempt's failing time reports 80.
    #[test]
    fn example_1_fails_at_80_and_the_error_executes_at_90() {
        assert_eq!(violations(None), [80]);
        let end = violations(None)[0];
        assert_eq!(action_tick(&TICKS, end), Some(90));
        // The attempt interval is not stretched to the action's time.
        assert_eq!(end, 80);
    }

    /// Example 3: `rst` is high between 82 and 84 and low elsewhere. The
    /// sampled value at every global tick is low, so the attempt at 80 is not
    /// disabled, and the later activity of `rst` before the action block at 90
    /// does not cancel it.
    #[test]
    fn example_3_an_ended_attempt_is_not_disabled_by_a_later_rst() {
        let rst_at = |t: Tick| u8::from((82..=84).contains(&t)) + b'0';
        let sampled: Vec<u8> = TICKS.iter().map(|&t| rst_at(t)).collect();
        assert!(sampled.iter().all(|&b| b == b'0'));
        assert_eq!(violations(Some(&sampled)), [80]);
        // rst active at the tick of the attempt does disable it.
        let mut at_80 = sampled.clone();
        at_80[at(80)] = b'1';
        assert_eq!(violations(Some(&at_80)), Vec::<Tick>::new());
    }

    /// Example 4: `##1 $stable_gclk(sig)` and `$steady_gclk(sig)` are
    /// equivalent; the `##1` is there because the plain `$stable_gclk(sig)`
    /// at the first tick compares with the default sampled value. Each
    /// attempt `i` of a4 looks at the past function of tick `i + 1`.
    #[test]
    fn example_4_stable_one_tick_later_is_steady() {
        let stable = |i: usize| SIG[i] == if i > 0 { SIG[i - 1] } else { b'x' };
        for i in 0..SIG.len() - 1 {
            let a4 = stable(i + 1);
            let a5 = eval_at(FutureFn::Steady, SIG, i) == Some(b'1');
            assert_eq!(a4, a5, "attempt at tick {i}");
        }
        // Cycle 0: a plain `$stable_gclk(sig)` compares with the default
        // sampled value of a `logic`, x, so it is false although the signal
        // does not change at the first tick.
        assert!(!stable(0));
        assert_eq!(eval_at(FutureFn::Steady, SIG, 0), Some(b'1'));
    }
}