1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
//! The identity of one controllable assertion (LRM 1800-2023 20.11): the
//! [`SiteDesc`] the assertion control registry
//! (`sv_sim_sim::sched::assert_control`) addresses it by.
//!
//! The control tasks name an assertion by its label (`a1: assert property ...`)
//! or by a scope that holds it, so every assertion site is lowered together with
//! the hierarchical name of its label and of the scope around it.
use sv_lang::kinds::StatementKind;
use sv_lang::{AssertionKind, Statement, Symbol};
use sv_sim_sim::process::cfg::shown_path;
use sv_sim_sim::sched::assert_control::{
ASSERT_CONCURRENT, ASSERT_EXPECT, ASSERT_FINAL_DEFERRED, ASSERT_OBSERVED_DEFERRED,
ASSERT_SIMPLE_IMMEDIATE, DIR_ASSERT, DIR_ASSUME, DIR_COVER, SiteDesc,
};
/// The label of the assertion statement `stmt` inside the procedure or
/// subroutine `owner`: the block slang wraps around a labeled statement
/// (`a1: assert ...`), which holds nothing but the statement. `None` when the
/// statement has no label.
fn label_block<'d>(owner: &Symbol<'d>, stmt: Statement<'d>) -> Option<Symbol<'d>> {
let at = stmt.source_range();
let mut stack = vec![sv_sim_sim::process::cfg::proc_body(owner)?.as_sem_node()];
while let Some(node) = stack.pop() {
if let Some(s) = node.as_statement()
&& s.kind() == StatementKind::Block
&& let Some(block) = s.block_symbol()
&& !block.name().is_empty()
&& let [only] = sv_sim_sim::process::cfg::live_statements(&s).as_slice()
&& only.source_range() == at
&& s.source_range().end == at.end
{
return Some(block);
}
stack.extend(sv_sim_sim::process::cfg::live_children(&node));
}
None
}
/// The Table 20-6 directive bit of an assertion statement, `None` for the
/// directives the control tasks cannot select (`restrict`).
pub fn directive_bit(kind: AssertionKind) -> Option<u32> {
match kind {
AssertionKind::Assert => Some(DIR_ASSERT),
AssertionKind::Assume => Some(DIR_ASSUME),
AssertionKind::CoverProperty | AssertionKind::CoverSequence => Some(DIR_COVER),
AssertionKind::Restrict => None,
// 20.11: the directive type "is checked only for assertions"; an
// `expect` is not one.
AssertionKind::Expect => Some(0),
}
}
/// The Table 20-5 `assertion_type` bit of an assertion statement.
fn assertion_type_bit(stmt: &Statement<'_>, kind: AssertionKind) -> u32 {
if kind == AssertionKind::Expect {
return ASSERT_EXPECT;
}
if stmt.kind() == StatementKind::ConcurrentAssertion {
return ASSERT_CONCURRENT;
}
if stmt.is_final_assertion() == Some(true) {
ASSERT_FINAL_DEFERRED
} else if stmt.is_deferred_assertion() == Some(true) {
ASSERT_OBSERVED_DEFERRED
} else {
ASSERT_SIMPLE_IMMEDIATE
}
}
/// The site of the assertion statement `stmt` (written in `owner`, the
/// procedure or subroutine holding it), `None` for a directive no control task
/// reaches (`restrict`).
pub fn describe<'d>(owner: &Symbol<'d>, stmt: Statement<'d>) -> Option<SiteDesc> {
let kind = match stmt.assertion_kind() {
Some(k) => k,
None => stmt.immediate_assertion_kind()?,
};
let directive_type = directive_bit(kind)?;
let assertion_type = assertion_type_bit(&stmt, kind);
let (scope, label) = match label_block(owner, stmt) {
Some(block) => {
let label = shown_path(&block);
let scope = block.parent().map(|p| shown_path(&p)).unwrap_or_default();
(scope, label)
}
// An unlabeled assertion is told apart from the others of its scope by
// its source offset (`#<offset>`, see `anonymous_label`), so that
// `vpi_control` can address it one by one.
None => (
shown_path(owner),
anonymous_label(stmt.source_range().start.offset),
),
};
Some(SiteDesc {
assertion_type,
directive_type,
scope,
label,
})
}
/// The label an unlabeled assertion statement gets in the registry: `#` and its
/// source offset. `#` cannot start an identifier, so it never names a real
/// assertion; the control tasks reach it through its scope only, while
/// `vpi_control` names it as `#<offset>@<scope>`
/// (`assert_control::anonymous_target`).
pub fn anonymous_label(offset: u64) -> String {
format!("#{offset}")
}
/// A violation report site (`unique`/`unique0`/`priority` `if`/`case`) in
/// `owner`, `assertion_type` the Table 20-5 bit of its type.
pub fn violation_site(owner: &Symbol<'_>, assertion_type: u32) -> SiteDesc {
SiteDesc {
assertion_type,
directive_type: 0,
scope: shown_path(owner),
label: String::new(),
}
}