merge queue: checking #2408 on master (a037246), stacked on #2413

conformance/sv-tests/expected.tsv

@@ -315,8 +315,8 @@ chapter-16/16.11--sequence-subroutine-uvm.sv	2state	fail
 chapter-16/16.11--sequence-subroutine-uvm.sv	4state	fail
 chapter-16/16.12--property-disable-iff.sv	2state	fail
 chapter-16/16.12--property-disable-iff.sv	4state	fail
-chapter-16/16.12--property-disj.sv	2state	fail
-chapter-16/16.12--property-disj.sv	4state	fail
+chapter-16/16.12--property-disj.sv	2state	pass
+chapter-16/16.12--property-disj.sv	4state	pass
 chapter-16/16.12--property-iff.sv	2state	fail
 chapter-16/16.12--property-iff.sv	4state	fail
 chapter-16/16.12--property-interface-prec-uvm.sv	2state	fail
@@ -329,14 +329,14 @@ chapter-16/16.12--property-prec.sv	2state	fail
 chapter-16/16.12--property-prec.sv	4state	fail
 chapter-16/16.12--property-uvm.sv	2state	fail
 chapter-16/16.12--property-uvm.sv	4state	fail
-chapter-16/16.12--property.sv	2state	fail
-chapter-16/16.12--property.sv	4state	fail
+chapter-16/16.12--property.sv	2state	pass
+chapter-16/16.12--property.sv	4state	pass
 chapter-16/16.13--sequence-multiclock-uvm.sv	2state	fail
 chapter-16/16.13--sequence-multiclock-uvm.sv	4state	fail
 chapter-16/16.14--assume-property-uvm.sv	2state	fail
 chapter-16/16.14--assume-property-uvm.sv	4state	fail
-chapter-16/16.14--assume-property.sv	2state	fail
-chapter-16/16.14--assume-property.sv	4state	fail
+chapter-16/16.14--assume-property.sv	2state	pass
+chapter-16/16.14--assume-property.sv	4state	pass
 chapter-16/16.15--property-disable-iff-fail.sv	2state	pass
 chapter-16/16.15--property-disable-iff-fail.sv	4state	pass
 chapter-16/16.15--property-disable-iff.sv	2state	fail
@@ -2637,8 +2637,8 @@ generated/sampled_functions/20.13--rose.sv	2state	fail
 generated/sampled_functions/20.13--rose.sv	4state	fail
 generated/sampled_functions/20.13--rose_gclk.sv	2state	fail
 generated/sampled_functions/20.13--rose_gclk.sv	4state	fail
-generated/sampled_functions/20.13--sampled.sv	2state	fail
-generated/sampled_functions/20.13--sampled.sv	4state	fail
+generated/sampled_functions/20.13--sampled.sv	2state	pass
+generated/sampled_functions/20.13--sampled.sv	4state	pass
 generated/sampled_functions/20.13--stable.sv	2state	fail
 generated/sampled_functions/20.13--stable.sv	4state	fail
 generated/sampled_functions/20.13--stable_gclk.sv	2state	fail

crates/celox-design/src/lib.rs

@@ -475,6 +475,10 @@ pub enum ProcessStatus {
     DisableFork,
     /// A side-effect-free event-expression probe completed; no HDL continuation ran.
     EventProbe,
+    /// Resume an assertion predicate in Observed after Active/NBA quiescence.
+    AssertionObserved,
+    /// Resume an assertion action in Reactive after every Observed predicate.
+    AssertionReactive,
 }
 
 impl ProcessStatus {
@@ -498,6 +502,8 @@ impl ProcessStatus {
             Self::WaitFork => 14,
             Self::DisableFork => 15,
             Self::EventProbe => 16,
+            Self::AssertionObserved => 17,
+            Self::AssertionReactive => 18,
         }
     }
 
@@ -519,6 +525,8 @@ impl ProcessStatus {
             14 => Some(Self::WaitFork),
             15 => Some(Self::DisableFork),
             16 => Some(Self::EventProbe),
+            17 => Some(Self::AssertionObserved),
+            18 => Some(Self::AssertionReactive),
             _ => None,
         }
     }

crates/celox-frontend-core/src/process.rs

@@ -208,6 +208,16 @@ impl ProcessKernelBuilder {
         self.suspend(ProcessStatus::InactiveDelay)
     }
 
+    /// A concurrent assertion's Observed predicate / Reactive action boundary.
+    pub fn assertion_region(&mut self, reactive: bool) -> Result<(), ProcessKernelError> {
+        self.slots.const_delays = false;
+        self.suspend(if reactive {
+            ProcessStatus::AssertionReactive
+        } else {
+            ProcessStatus::AssertionObserved
+        })
+    }
+
     fn note_delay(&mut self, constant: Option<u64>) {
         self.slots.const_delays &= constant.is_some_and(|amount| amount > 0);
     }

crates/celox-frontend-sv/src/lowering/comb.rs

@@ -2041,7 +2041,9 @@ impl<'p, 'a> Comb<'p, 'a> {
     ) -> Result<Store, sv::AnalyzerError> {
         match stmt {
             sv::ir::Stmt::DisableFork => Ok(store),
-            sv::ir::Stmt::Fork { .. } | sv::ir::Stmt::WaitFork => {
+            sv::ir::Stmt::Fork { .. }
+            | sv::ir::Stmt::WaitFork
+            | sv::ir::Stmt::AssertionRegion { .. } => {
                 Err(unsupported("fork control outside a timed process"))
             }
             sv::ir::Stmt::Assign {

crates/celox-frontend-sv/src/lowering/ff.rs

@@ -3599,6 +3599,11 @@ impl<'p, 'a> Ff<'p, 'a> {
                 self.wait_level(condition)?;
                 Ok(true)
             }
+            sv::ir::Stmt::AssertionRegion { reactive } => {
+                self.with_kernel(|kernel| kernel.assertion_region(*reactive))
+                    .map_err(kernel_error)?;
+                Ok(true)
+            }
             sv::ir::Stmt::WaitFork | sv::ir::Stmt::DisableFork => {
                 if self.kernel.is_none() {
                     return if matches!(stmt, sv::ir::Stmt::DisableFork) {

crates/celox-runtime/src/simulation/activation.rs

@@ -247,6 +247,7 @@ impl<B: SimBackend> SimulationState<B> {
                 state.waiters.remove(id);
                 state.ready.remove(&id);
                 state.reactive.remove(&id);
+                state.observed.remove(&id);
                 state.inactive.remove(&id);
                 state.re_inactive.remove(&id);
             }

crates/celox-runtime/src/simulation/compiled.rs

@@ -72,6 +72,7 @@ impl<B: SimBackend> SimulationState<B> {
             || self.suspended.is_some()
             || self.declarations_pending
             || self.host_pending
+            || !pending.observed.is_empty()
             || !pending.ready.is_empty()
             || !pending.inactive.is_empty()
             || !pending.nba_queue.is_empty()

crates/celox-runtime/src/simulation/persist.rs

@@ -297,6 +297,7 @@ impl<B: SimBackend> SimulationState<B> {
             inactive: state.inactive.iter().copied().collect(),
             nba_queue: state.nba_queue.clone(),
             reactive: state.reactive.iter().copied().collect(),
+            observed: state.observed.iter().copied().collect(),
             re_inactive: state.re_inactive.iter().copied().collect(),
             re_nba_queue: state.re_nba_queue.clone(),
             domain_counters: state.domain_counters.clone(),
@@ -329,6 +330,7 @@ pub struct ScheduleKey {
     pub inactive: Vec<usize>,
     pub nba_queue: Vec<super::NbaUpdate>,
     pub reactive: Vec<usize>,
+    pub observed: Vec<usize>,
     pub re_inactive: Vec<usize>,
     pub re_nba_queue: Vec<super::NbaUpdate>,
     pub domain_counters: Vec<[u32; 3]>,

crates/celox-runtime/src/simulation/process.rs

@@ -225,6 +225,12 @@ impl<B: SimBackend> SimulationState<B> {
                     self.charge(*returns, Some(process))?;
                     return Ok(true);
                 }
+                Some(ProcessStatus::AssertionObserved) => {
+                    self.process_state.observed.insert(process);
+                }
+                Some(ProcessStatus::AssertionReactive) => {
+                    self.process_state.reactive.insert(process);
+                }
                 Some(ProcessStatus::HostRequest) => {
                     let (kind, index) = HostRequestKind::decode(delay())
                         .ok_or(SimulatorErrorCode::InternalError)?;
@@ -316,6 +322,34 @@ impl<B: SimBackend> SimulationState<B> {
         Ok(true)
     }
 
+    pub(super) fn run_observed_assertions<E>(
+        &mut self,
+        executor: &mut E,
+        time: u64,
+    ) -> Result<(), Halt>
+    where
+        E: SimulationExecutor<Backend = B>,
+    {
+        let mut returns = 0;
+        while let Some(&process) = self.process_state.observed.first() {
+            self.charge_pass()?;
+            self.process_state.observed.remove(&process);
+            loop {
+                match self.run_process(executor, time, process, &mut returns) {
+                    Ok(true) => continue,
+                    Ok(false) => break,
+                    Err(halt) => {
+                        if matches!(halt, Halt::Stop) {
+                            self.process_state.observed.insert(process);
+                        }
+                        return Err(halt);
+                    }
+                }
+            }
+        }
+        Ok(())
+    }
+
     /// The processes ready in the Reactive region if `reactive`, otherwise in
     /// the Active region.
     #[inline]

crates/celox-runtime/src/simulation/time.rs

@@ -196,6 +196,7 @@ impl<B: SimBackend> SimulationState<B> {
             let ready = self.take_ready_processes(current_time);
             if ready.is_empty() && self.process_state.ready.is_empty() {
                 executor.try_observed_deferred_assertions(current_time)?;
+                self.run_observed_assertions(executor, current_time)?;
                 // The active region set is empty: the reactive region set
                 // runs, and the design activity it creates runs in the active
                 // region set again (IEEE 1800-2023 4.5).
@@ -321,6 +322,7 @@ impl<B: SimBackend> SimulationState<B> {
             return None;
         }
         if self.finalizing.is_some()
+            || !self.process_state.observed.is_empty()
             || !self.process_state.ready.is_empty()
             || !self.process_state.reactive.is_empty()
         {

crates/celox-runtime/src/state_file.rs

@@ -51,12 +51,13 @@
 //! Version 1 files, which have no process section, still load. A file whose
 //! processes have nothing to record is written as version 1, which older
 //! builds read too. Static-only process schedules retain version 2; graphs
-//! and reactive queues require version 3. Versions 1 and 2 remain readable.
+//! and reactive queues require version 3. Pending Observed assertion evaluations
+//! require version 4. Versions 1 through 3 remain readable.
 
 use std::io::{self, Read, Write};
 
 const MAGIC: &[u8; 8] = b"CXSTATE\0";
-const VERSION: u16 = 3;
+const VERSION: u16 = 4;
 
 mod activations;
 use activations::*;
@@ -133,6 +134,7 @@ pub struct ProcessRecord {
     /// Values shared by automatic locals across activations.
     pub cells: Vec<FrameValueRecord>,
     pub reactive: Vec<ProcessRef>,
+    pub observed: Vec<ProcessRef>,
     pub re_inactive: Vec<ProcessRef>,
     pub re_nba_queue: Vec<NbaRecord>,
     /// Suspended processes and the time each resumes at.
@@ -248,7 +250,15 @@ impl StateFile {
             .as_ref()
             .map(|schedule| &schedule.processes)
             .filter(|processes| **processes != ProcessRecord::default());
-        let version = processes.map_or(1, |p| if needs_v3(p) { VERSION } else { 2 });
+        let version = processes.map_or(1, |p| {
+            if !p.observed.is_empty() {
+                4
+            } else if needs_v3(p) {
+                3
+            } else {
+                2
+            }
+        });
         put_u16(w, version)?;
         let mut flags = 0;
         if self.four_state {
@@ -593,6 +603,9 @@ fn put_processes(w: &mut impl Write, processes: &ProcessRecord, version: u16) ->
     if version >= 3 {
         put_extension(w, processes)?;
     }
+    if version >= 4 {
+        put_process_list(w, &processes.observed, version)?;
+    }
     Ok(())
 }
 
@@ -684,6 +697,9 @@ fn get_processes(r: &mut impl Read, version: u16) -> Result<ProcessRecord, State
     if version >= 3 {
         get_extension(r, &mut result)?;
     }
+    if version >= 4 {
+        result.observed = get_process_list(r, version)?;
+    }
     Ok(result)
 }
 
@@ -893,6 +909,19 @@ mod tests {
         assert_eq!(StateFile::read_from(bytes.as_slice()).unwrap(), file);
     }
 
+    #[test]
+    fn observed_assertion_queue_round_trips_in_v4() {
+        let mut file = sample();
+        file.schedule.as_mut().unwrap().processes.observed = vec![
+            ProcessRef::Kernel("assertion.status".into()),
+            ProcessRef::Activation(12),
+        ];
+        let mut bytes = Vec::new();
+        file.write_to(&mut bytes).unwrap();
+        assert_eq!(bytes[8..10], 4u16.to_le_bytes());
+        assert_eq!(StateFile::read_from(bytes.as_slice()).unwrap(), file);
+    }
+
     #[test]
     fn rejects_foreign_and_truncated_input() {
         assert!(matches!(

crates/celox-runtime/src/timing.rs

@@ -443,6 +443,9 @@ pub struct ProcessState {
     /// Program processes ready to run in the Reactive region of the current
     /// time (IEEE 1800-2023 4.4.2.6).
     pub reactive: std::collections::BTreeSet<usize>,
+    /// Assertion predicates waiting for Active/NBA quiescence.
+    #[serde(default)]
+    pub observed: std::collections::BTreeSet<usize>,
     /// Program processes that resume in the Re-Inactive region (`#0`,
     /// 4.4.2.7).
     pub re_inactive: std::collections::BTreeSet<usize>,

crates/celox-sv-analyzer/src/ast/const_functions.rs

@@ -1791,6 +1791,7 @@ impl<'a> Frame<'a> {
                 return None;
             }
             Stmt::Fork { .. }
+            | Stmt::AssertionRegion { .. }
             | Stmt::WaitFork
             | Stmt::DisableFork
             | Stmt::AssignConcat { .. }

crates/celox-sv-analyzer/src/ast/const_functions/runtime.rs

@@ -100,6 +100,7 @@ impl<'a> RuntimeConstantFunctions<'a> {
                     | Stmt::WaitImplicit(_)
                     | Stmt::Wait(_)
                     | Stmt::Fork { .. }
+                    | Stmt::AssertionRegion { .. }
                     | Stmt::WaitFork
                     | Stmt::DisableFork => impure = true,
                     _ => {}

crates/celox-sv-analyzer/src/ast/lifetimes.rs

@@ -676,7 +676,9 @@ impl Flow<'_> {
                 self.read(expr, written)?;
                 Ok(Exits::next(written))
             }
-            Stmt::WaitFork | Stmt::DisableFork => Ok(Exits::next(written)),
+            Stmt::AssertionRegion { .. } | Stmt::WaitFork | Stmt::DisableFork => {
+                Ok(Exits::next(written))
+            }
             Stmt::WaitEvent(items) => {
                 for item in items {
                     self.read(&item.expr, written)?;
@@ -840,6 +842,7 @@ pub(super) fn stmt_exprs(stmt: &Stmt) -> Vec<&Expr> {
             .collect(),
         // The statements of an `@*` describe its reads and do not run.
         Stmt::Fork { .. }
+        | Stmt::AssertionRegion { .. }
         | Stmt::WaitFork
         | Stmt::DisableFork
         | Stmt::WaitImplicit(_)

crates/celox-sv-analyzer/src/ast/procedural/assertions.rs

@@ -18,3 +18,50 @@ impl BodyBuilder<'_, '_, '_> {
             .map(procedural_truth_condition)
     }
 }
+
+/// Until property calls have their own sampled formal bindings, reject
+/// calls that could read/write live state behind an operand's sampled copy.
+pub(super) fn concurrent_operand(expr: &Expr) -> Result<(), AnalyzerError> {
+    let mut unsupported_call = None;
+    const_functions::visit_expr_calls(expr, &mut |callee, _| {
+        if callee.is_effectful() {
+            unsupported_call = Some(callee.to_string());
+        }
+    });
+    if let Some(name) = unsupported_call {
+        return Err(unsupported(format!(
+            "call `{name}` in concurrent assertion operand"
+        )));
+    }
+    Ok(())
+}
+
+pub(super) fn concurrent_action(body: &[Stmt]) -> Result<(), AnalyzerError> {
+    let mut unsupported_action = false;
+    for stmt in body {
+        stmt.walk(&mut |stmt| {
+            unsupported_action |= matches!(
+                stmt,
+                Stmt::Delay { .. }
+                    | Stmt::WaitEvent(_)
+                    | Stmt::WaitImplicit(_)
+                    | Stmt::Wait(_)
+                    | Stmt::WaitFork
+                    | Stmt::DisableFork
+                    | Stmt::Fork { .. }
+                    | Stmt::Call { .. }
+                    | Stmt::Assign {
+                        nonblocking: true,
+                        ..
+                    }
+                    | Stmt::AssertionRegion { .. }
+            );
+        });
+    }
+    if unsupported_action {
+        return Err(unsupported(
+            "timed, nonblocking, or subroutine concurrent assertion action",
+        ));
+    }
+    Ok(())
+}