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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
use crate::HashMap;
use crate::ir::VarId;
/// Identifies the LHS of an assignment: (VarId, Option<array_element_index>).
/// None index means dynamic (unknown at analysis time).
type AssignTarget = (VarId, Option<usize>);
#[derive(Clone, Debug)]
pub struct FfTableEntry {
pub assigned: Option<usize>,
/// (decl_index, assign_target, from_ff) pairs where this variable is referenced.
/// None assign_target for condition expressions (if/case).
/// from_ff: true if the reference is in an always_ff block (NBA-sensitive),
/// false if in always_comb / continuous assign (re-evaluated after NBA).
pub refered: Vec<(usize, Option<AssignTarget>, bool)>,
pub is_ff: bool,
pub assigned_comb: Option<usize>,
}
impl FfTableEntry {
fn update_is_ff(&mut self, self_key: (VarId, usize)) {
if let Some(assigned_decl) = self.assigned {
// FF classification rules (strict NBA semantics):
// - A variable may be treated as comb (ff_opt) only if no always_ff
// block reads it (cross-block NBA races would be violated).
// - always_comb / continuous assigns re-evaluate after NBA in SV,
// so they correctly see new FF values; ff_opt is safe for them.
// - Within the same always_ff (assigned_decl), self-reference is
// safe; but cross-variable assignments must see old values.
self.is_ff = self.refered.iter().any(|(decl, assign_target, from_ff)| {
if !from_ff {
return false;
}
if *decl != assigned_decl {
return true;
}
match assign_target {
Some((target_id, target_idx)) => {
if *target_id != self_key.0 {
return true;
}
// Same VarId: compare array index.
// None index (dynamic) is conservative → FF.
match target_idx {
Some(idx) => *idx != self_key.1,
None => true,
}
}
None => true,
}
});
}
}
}
#[derive(Clone, Debug, Default)]
pub struct FfTable {
pub table: HashMap<(VarId, usize), FfTableEntry>,
}
impl FfTable {
pub fn update_is_ff(&mut self) {
let keys: Vec<_> = self.table.keys().cloned().collect();
for key in keys {
self.table.get_mut(&key).unwrap().update_is_ff(key);
}
}
/// Force all always_ff-assigned variables to FF, disabling the
/// assign_target refinement. Used by --disable-ff-opt for debugging.
pub fn force_all_ff(&mut self) {
for entry in self.table.values_mut() {
if entry.assigned.is_some() {
entry.is_ff = true;
}
}
}
pub fn is_ff(&self, id: VarId, index: usize) -> bool {
if let Some(x) = self.table.get(&(id, index)) {
x.is_ff
} else {
false
}
}
pub fn insert_refered(
&mut self,
id: VarId,
index: usize,
decl: usize,
assign_target: Option<AssignTarget>,
from_ff: bool,
) {
self.table
.entry((id, index))
.and_modify(|x| x.refered.push((decl, assign_target, from_ff)))
.or_insert(FfTableEntry {
assigned: None,
refered: vec![(decl, assign_target, from_ff)],
is_ff: false,
assigned_comb: None,
});
}
pub fn insert_assigned(&mut self, id: VarId, index: usize, decl: usize) {
self.table
.entry((id, index))
.and_modify(|x| x.assigned = Some(decl))
.or_insert(FfTableEntry {
assigned: Some(decl),
refered: vec![],
is_ff: false,
assigned_comb: None,
});
}
pub fn insert_assigned_comb(&mut self, id: VarId, index: usize, decl: usize) {
self.table
.entry((id, index))
.and_modify(|x| x.assigned_comb = Some(decl))
.or_insert(FfTableEntry {
assigned: None,
refered: vec![],
is_ff: false,
assigned_comb: Some(decl),
});
}
#[cfg(debug_assertions)]
pub fn validate(&self) {
for ((id, index), entry) in &self.table {
if let (Some(ff_decl), Some(comb_decl)) = (entry.assigned, entry.assigned_comb) {
log::warn!(
"FfTable: variable {:?}[{}] assigned in both always_ff (decl {}) and always_comb (decl {})",
id,
index,
ff_decl,
comb_decl
);
}
}
}
}