1use std::fmt::Display;
2use std::collections::{BTreeMap, BTreeSet};
3
4use crate::{Cell, Design, IoNet, Net, Value};
5
6#[derive(Debug)]
7pub enum NotIsomorphic {
8 NoOutputLeft(String),
9 NoOutputRight(String),
10 OutputSizeMismatch(String),
11 IoSizeMismatch(String),
12 NameSizeMismatch(String),
13 ValueSizeMismatch(Value, Value),
14 NetMismatch(Net, Net),
15 IoNetMismatch(IoNet, IoNet),
16}
17
18impl Display for NotIsomorphic {
19 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
20 match self {
21 NotIsomorphic::NoOutputLeft(name) => write!(f, "output {name:?} is missing in the left design"),
22 NotIsomorphic::NoOutputRight(name) => write!(f, "output {name:?} is missing in the right design"),
23 NotIsomorphic::OutputSizeMismatch(name) => write!(f, "size of output {name:?} does not match"),
24 NotIsomorphic::IoSizeMismatch(name) => write!(f, "size of IO {name:?} does not match"),
25 NotIsomorphic::NameSizeMismatch(name) => write!(f, "size of name cell {name:?} does not match"),
26 NotIsomorphic::ValueSizeMismatch(value_l, value_r) => {
27 write!(f, "size of values {value_l} and {value_r} do not match")
28 }
29 NotIsomorphic::NetMismatch(net_l, net_r) => write!(f, "nets {net_l} and {net_r} are not isomorphic"),
30 NotIsomorphic::IoNetMismatch(io_net_l, io_net_r) => {
31 write!(f, "IO nets {io_net_l} and {io_net_r} are not isomorphic")
32 }
33 }
34 }
35}
36
37pub fn isomorphic(lft: &Design, rgt: &Design) -> Result<(), NotIsomorphic> {
39 let mut queue: BTreeSet<(Net, Net)> = BTreeSet::new();
40 fn queue_vals(queue: &mut BTreeSet<(Net, Net)>, val_l: &Value, val_r: &Value) -> Result<(), NotIsomorphic> {
41 if val_l.len() != val_r.len() {
42 return Err(NotIsomorphic::ValueSizeMismatch(val_l.clone(), val_r.clone()));
43 }
44 for (net_l, net_r) in val_l.iter().zip(val_r) {
45 queue.insert((net_l, net_r));
46 }
47 Ok(())
48 }
49
50 let mut visited: BTreeSet<(Net, Net)> = BTreeSet::new();
51 visited.insert((Net::UNDEF, Net::UNDEF));
52 visited.insert((Net::ZERO, Net::ZERO));
53 visited.insert((Net::ONE, Net::ONE));
54 let mut outputs_l = BTreeMap::new();
55 let mut names_l = BTreeMap::new();
56 for cell in lft.iter_cells() {
57 match &*cell.get() {
58 Cell::Output(name, value) => {
59 outputs_l.insert(name.clone(), value.clone());
60 }
61 Cell::Name(name, value) => {
62 names_l.insert(name.clone(), value.clone());
63 }
64 _ => (),
65 }
66 }
67 let mut outputs_r = BTreeMap::new();
68 let mut names_r = BTreeMap::new();
69 for cell in rgt.iter_cells() {
70 match &*cell.get() {
71 Cell::Output(name, value) => {
72 outputs_r.insert(name.clone(), value.clone());
73 }
74 Cell::Name(name, value) => {
75 names_r.insert(name.clone(), value.clone());
76 }
77 _ => (),
78 }
79 }
80 for (name, value_l) in &outputs_l {
81 if let Some(value_r) = outputs_r.get(name) {
82 if value_l.len() != value_r.len() {
83 return Err(NotIsomorphic::OutputSizeMismatch(name.clone()));
84 }
85 for (net_l, net_r) in value_l.iter().zip(value_r) {
86 queue.insert((net_l, net_r));
87 }
88 } else {
89 return Err(NotIsomorphic::NoOutputRight(name.clone()));
90 }
91 }
92 for name in outputs_r.keys() {
93 if !outputs_l.contains_key(name) {
94 return Err(NotIsomorphic::NoOutputLeft(name.clone()));
95 }
96 }
97 for (name, value_l) in &names_l {
98 if let Some(value_r) = names_r.get(name) {
99 if value_l.len() != value_r.len() {
100 return Err(NotIsomorphic::NameSizeMismatch(name.clone()));
101 }
102 for (net_l, net_r) in value_l.iter().zip(value_r) {
103 queue.insert((net_l, net_r));
104 }
105 }
106 }
107 let mut ios = BTreeSet::new();
108 ios.insert((IoNet::FLOATING, IoNet::FLOATING));
109 for (name, _) in lft.iter_ios() {
110 if let (Some(io_l), Some(io_r)) = (lft.get_io(name), rgt.get_io(name)) {
111 if io_l.len() != io_r.len() {
112 return Err(NotIsomorphic::IoSizeMismatch(name.to_owned()));
113 }
114 for (ionet_l, ionet_r) in io_l.iter().zip(io_r.iter()) {
115 ios.insert((ionet_l, ionet_r));
116 }
117 }
118 }
119 while let Some((net_l, net_r)) = queue.pop_first() {
120 if visited.contains(&(net_l, net_r)) {
121 continue;
122 }
123 if net_l.as_const().is_some() || net_r.as_const().is_some() {
124 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
126 }
127 let (cell_l, bit_l) = lft.find_cell(net_l);
128 let (cell_r, bit_r) = rgt.find_cell(net_r);
129 let out_l = cell_l.output();
130 let out_r = cell_r.output();
131 if bit_l != bit_r || out_l.len() != out_r.len() {
132 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
133 }
134 for (net_l, net_r) in out_l.iter().zip(out_r) {
135 visited.insert((net_l, net_r));
136 }
137 match (&*cell_l.get(), &*cell_r.get()) {
138 (Cell::Const(val_l), Cell::Const(val_r)) => {
139 if val_l != val_r {
140 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
141 }
142 }
143 (Cell::Buf(val_l), Cell::Buf(val_r)) | (Cell::Not(val_l), Cell::Not(val_r)) => {
144 queue_vals(&mut queue, val_l, val_r)?
145 }
146 (Cell::And(arg1_l, arg2_l), Cell::And(arg1_r, arg2_r))
147 | (Cell::Or(arg1_l, arg2_l), Cell::Or(arg1_r, arg2_r))
148 | (Cell::Xor(arg1_l, arg2_l), Cell::Xor(arg1_r, arg2_r))
149 | (Cell::Eq(arg1_l, arg2_l), Cell::Eq(arg1_r, arg2_r))
150 | (Cell::ULt(arg1_l, arg2_l), Cell::ULt(arg1_r, arg2_r))
151 | (Cell::SLt(arg1_l, arg2_l), Cell::SLt(arg1_r, arg2_r))
152 | (Cell::Mul(arg1_l, arg2_l), Cell::Mul(arg1_r, arg2_r))
153 | (Cell::UDiv(arg1_l, arg2_l), Cell::UDiv(arg1_r, arg2_r))
154 | (Cell::UMod(arg1_l, arg2_l), Cell::UMod(arg1_r, arg2_r))
155 | (Cell::SDivTrunc(arg1_l, arg2_l), Cell::SDivTrunc(arg1_r, arg2_r))
156 | (Cell::SDivFloor(arg1_l, arg2_l), Cell::SDivFloor(arg1_r, arg2_r))
157 | (Cell::SModTrunc(arg1_l, arg2_l), Cell::SModTrunc(arg1_r, arg2_r))
158 | (Cell::SModFloor(arg1_l, arg2_l), Cell::SModFloor(arg1_r, arg2_r)) => {
159 queue_vals(&mut queue, arg1_l, arg1_r)?;
160 queue_vals(&mut queue, arg2_l, arg2_r)?;
161 }
162 (Cell::Mux(arg1_l, arg2_l, arg3_l), Cell::Mux(sel_r, arg2_r, arg3_r)) => {
163 queue.insert((*arg1_l, *sel_r));
164 queue_vals(&mut queue, arg2_l, arg2_r)?;
165 queue_vals(&mut queue, arg3_l, arg3_r)?;
166 }
167 (Cell::Adc(arg1_l, arg2_l, arg3_l), Cell::Adc(arg1_r, arg2_r, arg3_r)) => {
168 queue_vals(&mut queue, arg1_l, arg1_r)?;
169 queue_vals(&mut queue, arg2_l, arg2_r)?;
170 queue.insert((*arg3_l, *arg3_r));
171 }
172 (Cell::Aig(arg1_l, arg2_l), Cell::Aig(arg1_r, arg2_r)) => {
173 queue.insert((arg1_l.net(), arg1_r.net()));
174 queue.insert((arg2_l.net(), arg2_r.net()));
175 if arg1_l.is_positive() != arg1_r.is_positive() || arg2_l.is_positive() != arg2_r.is_positive() {
176 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
177 }
178 }
179 (Cell::Shl(arg1_l, arg2_l, stride_l), Cell::Shl(arg1_r, arg2_r, stride_r))
180 | (Cell::UShr(arg1_l, arg2_l, stride_l), Cell::UShr(arg1_r, arg2_r, stride_r))
181 | (Cell::SShr(arg1_l, arg2_l, stride_l), Cell::SShr(arg1_r, arg2_r, stride_r))
182 | (Cell::XShr(arg1_l, arg2_l, stride_l), Cell::XShr(arg1_r, arg2_r, stride_r)) => {
183 queue_vals(&mut queue, arg1_l, arg1_r)?;
184 queue_vals(&mut queue, arg2_l, arg2_r)?;
185 if stride_l != stride_r {
186 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
187 }
188 }
189 (Cell::Dff(ff_l), Cell::Dff(ff_r)) => {
190 queue_vals(&mut queue, &ff_l.data, &ff_r.data)?;
191 queue_vals(&mut queue, &ff_l.load_data, &ff_r.load_data)?;
192 queue.insert((ff_l.clock.net(), ff_r.clock.net()));
193 queue.insert((ff_l.clear.net(), ff_r.clear.net()));
194 queue.insert((ff_l.load.net(), ff_r.load.net()));
195 queue.insert((ff_l.reset.net(), ff_r.reset.net()));
196 queue.insert((ff_l.enable.net(), ff_r.enable.net()));
197 if ff_l.clock.is_positive() != ff_r.clock.is_positive()
198 || ff_l.clear.is_positive() != ff_r.clear.is_positive()
199 || ff_l.load.is_positive() != ff_r.load.is_positive()
200 || ff_l.reset.is_positive() != ff_r.reset.is_positive()
201 || ff_l.enable.is_positive() != ff_r.enable.is_positive()
202 || (ff_l.reset_over_enable != ff_r.reset_over_enable
203 && !ff_l.reset.is_always(false)
204 && !ff_l.enable.is_always(true))
205 || ff_l.clear_value != ff_r.clear_value
206 || ff_l.reset_value != ff_r.reset_value
207 || ff_l.init_value != ff_r.init_value
208 {
209 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
210 }
211 }
212 (Cell::IoBuf(iobuf_l), Cell::IoBuf(iobuf_r)) => {
213 for (io_net_l, io_net_r) in iobuf_l.io.iter().zip(iobuf_r.io.iter()) {
214 if !ios.contains(&(io_net_l, io_net_r)) {
215 return Err(NotIsomorphic::IoNetMismatch(io_net_l, io_net_r));
216 }
217 }
218 queue_vals(&mut queue, &iobuf_l.output, &iobuf_r.output)?;
219 queue.insert((iobuf_l.enable.net(), iobuf_r.enable.net()));
220 if iobuf_l.enable.is_positive() != iobuf_r.enable.is_positive() {
221 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
222 }
223 }
224 (Cell::Memory(memory_l), Cell::Memory(memory_r)) => {
225 if memory_l.depth != memory_r.depth
226 || memory_l.width != memory_r.width
227 || memory_l.init_value != memory_r.init_value
228 || memory_l.write_ports.len() != memory_r.write_ports.len()
229 || memory_l.read_ports.len() != memory_r.read_ports.len()
230 {
231 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
232 }
233 for (write_port_l, write_port_r) in memory_l.write_ports.iter().zip(memory_r.write_ports.iter()) {
234 queue_vals(&mut queue, &write_port_l.addr, &write_port_r.addr)?;
235 queue_vals(&mut queue, &write_port_l.data, &write_port_r.data)?;
236 queue_vals(&mut queue, &write_port_l.mask, &write_port_r.mask)?;
237 queue.insert((write_port_l.clock.net(), write_port_r.clock.net()));
238 if write_port_l.clock.is_positive() != write_port_r.clock.is_positive() {
239 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
240 }
241 }
242 for (read_port_l, read_port_r) in memory_l.read_ports.iter().zip(memory_r.read_ports.iter()) {
243 queue_vals(&mut queue, &read_port_l.addr, &read_port_r.addr)?;
244 if read_port_l.data_len != read_port_r.data_len {
245 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
246 }
247 match (&read_port_l.flip_flop, &read_port_r.flip_flop) {
248 (None, None) => (),
249 (Some(ff_l), Some(ff_r)) => {
250 queue.insert((ff_l.clock.net(), ff_r.clock.net()));
251 queue.insert((ff_l.clear.net(), ff_r.clear.net()));
252 queue.insert((ff_l.reset.net(), ff_r.reset.net()));
253 queue.insert((ff_l.enable.net(), ff_r.enable.net()));
254 if ff_l.clock.is_positive() != ff_r.clock.is_positive()
255 || ff_l.clear.is_positive() != ff_r.clear.is_positive()
256 || ff_l.reset.is_positive() != ff_r.reset.is_positive()
257 || ff_l.enable.is_positive() != ff_r.enable.is_positive()
258 || (ff_l.reset_over_enable != ff_r.reset_over_enable
259 && !ff_l.reset.is_always(false)
260 && !ff_l.enable.is_always(true))
261 || ff_l.clear_value != ff_r.clear_value
262 || ff_l.reset_value != ff_r.reset_value
263 || ff_l.init_value != ff_r.init_value
264 || ff_l.relations != ff_r.relations
265 {
266 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
267 }
268 }
269 _ => return Err(NotIsomorphic::NetMismatch(net_l, net_r)),
270 }
271 }
272 }
273 (Cell::Target(target_cell_l), Cell::Target(target_cell_r)) => {
274 for (io_net_l, io_net_r) in target_cell_l.ios.iter().zip(target_cell_r.ios.iter()) {
275 if !ios.contains(&(io_net_l, io_net_r)) {
276 return Err(NotIsomorphic::IoNetMismatch(io_net_l, io_net_r));
277 }
278 }
279 if target_cell_l.kind != target_cell_r.kind || target_cell_l.params != target_cell_r.params {
280 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
281 }
282 queue_vals(&mut queue, &target_cell_l.inputs, &target_cell_r.inputs)?;
283 }
284 (Cell::Other(inst_l), Cell::Other(inst_r)) => {
285 if inst_l.kind != inst_r.kind || inst_l.params != inst_r.params || inst_l.outputs != inst_r.outputs {
286 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
287 }
288 for (name, value_l) in &inst_l.inputs {
289 let Some(value_r) = inst_r.inputs.get(name) else {
290 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
291 };
292 queue_vals(&mut queue, value_l, value_r)?;
293 }
294 for name in inst_r.inputs.keys() {
295 if !inst_l.inputs.contains_key(name) {
296 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
297 }
298 }
299 for (name, io_value_l) in &inst_l.ios {
300 let Some(io_value_r) = inst_r.ios.get(name) else {
301 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
302 };
303 for (io_net_l, io_net_r) in io_value_l.iter().zip(io_value_r.iter()) {
304 if !ios.contains(&(io_net_l, io_net_r)) {
305 return Err(NotIsomorphic::IoNetMismatch(io_net_l, io_net_r));
306 }
307 }
308 }
309 for name in inst_r.ios.keys() {
310 if !inst_l.ios.contains_key(name) {
311 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
312 }
313 }
314 }
315 (Cell::Input(name_l, _), Cell::Input(name_r, _)) => {
316 if name_l != name_r {
317 return Err(NotIsomorphic::NetMismatch(net_l, net_r));
318 }
319 }
320 _ => return Err(NotIsomorphic::NetMismatch(net_l, net_r)),
321 }
322 }
323 Ok(())
324}
325
326#[macro_export]
327macro_rules! assert_isomorphic {
328 ( $lft:ident, $rgt:ident ) => {
329 $lft.apply();
330 $rgt.apply();
331 let result = prjunnamed_netlist::isomorphic(&$lft, &$rgt);
332 if let Err(error) = result {
333 panic!("{}\nleft design:\n{}\nright design:\n{}", error, $lft, $rgt);
334 }
335 };
336}