nl_compiler/
aig.rs

1/*!
2
3  Compile AIG to Safety Net netlist
4
5*/
6
7use crate::error::AigError;
8use flussab::DeferredWriter;
9use flussab_aiger::aig::{Aig, AndGate, Renumber, RenumberConfig};
10use flussab_aiger::ascii;
11use safety_net::iter::DFSIterator;
12use safety_net::{DrivenNet, Identifier, Instantiable, Logic, Net, Netlist};
13use std::collections::HashSet;
14use std::{collections::HashMap, io::Write, rc::Rc};
15
16/// The index type for the AIG
17pub type U = u64;
18
19/// Compile an AIG to a Safety Net netlist from bytes
20pub fn from_aig_bytes<I: Instantiable>(
21    buf: &[u8],
22    and: I,
23    inv: I,
24) -> Result<Rc<Netlist<I>>, AigError> {
25    use flussab_aiger::binary;
26    let rdr = binary::Parser::<u64>::from_read(buf, binary::Config::default())?;
27
28    let aig = rdr.parse()?;
29
30    from_aig::<I>(&aig.into(), and, inv)
31}
32
33/// Construct a Safety Net [Netlist] from a AIG
34/// Type parameter I defines the primitive library to parse into.
35pub fn from_aig<I: Instantiable>(aig: &Aig<U>, and: I, inv: I) -> Result<Rc<Netlist<I>>, AigError> {
36    if !aig.bad_state_properties.is_empty() {
37        return Err(AigError::ContainsBadStates(
38            aig.bad_state_properties.clone(),
39        ));
40    }
41
42    if !aig.latches.is_empty() {
43        return Err(AigError::ContainsLatches(
44            aig.latches.iter().map(|l| l.state).collect(),
45        ));
46    }
47
48    let netlist = Netlist::<I>::new("top".into());
49
50    let inputs: Vec<(U, Identifier)> = aig
51        .inputs
52        .iter()
53        .map(|&id| (id, id.to_string().into()))
54        .collect();
55
56    let inputs: Vec<(U, DrivenNet<I>)> = inputs
57        .into_iter()
58        .map(|(u, id)| (u, netlist.insert_input(Net::new_logic(id))))
59        .collect();
60
61    let mut mapping: HashMap<U, DrivenNet<I>> = HashMap::new();
62
63    for (u, n) in inputs {
64        mapping.insert(u, n.clone());
65        let inv_id = n.get_identifier() + "_inv".into();
66        let inverted = netlist.insert_gate(inv.clone(), inv_id, &[n])?;
67        mapping.insert(u + 1, inverted.get_output(0));
68    }
69
70    for gate in &aig.and_gates {
71        let id = Identifier::new(gate.output.to_string());
72        let inv_id = id.clone() + "_inv".into();
73        let operands: Vec<_> = gate.inputs.iter().map(|u| mapping[u].clone()).collect();
74        let n = netlist
75            .insert_gate(and.clone(), id, &operands)?
76            .get_output(0);
77        mapping.insert(gate.output, n.clone());
78        let inverted = netlist.insert_gate(inv.clone(), inv_id, std::slice::from_ref(&n))?;
79        mapping.insert(gate.output + 1, inverted.get_output(0));
80    }
81
82    for o in &aig.outputs {
83        let n = mapping[o].clone();
84        netlist.expose_net(n)?;
85    }
86
87    drop(mapping);
88
89    netlist.clean()?;
90
91    Ok(netlist)
92}
93
94/// Write an AIG to an ASCII file
95pub fn write_aig<'a>(aig: &Aig<U>, output: impl Write + 'a) -> Result<(), AigError> {
96    let mut aag_writer = DeferredWriter::from_write(output);
97    let aag_writer = ascii::Writer::<U>::new(&mut aag_writer);
98
99    let (aig, _) = Renumber::renumber_aig(
100        RenumberConfig::default()
101            .trim(false)
102            .structural_hash(false)
103            .const_fold(false),
104        aig,
105    )?;
106
107    aag_writer.write_ordered_aig(&aig);
108
109    aag_writer.flush()?;
110    Ok(())
111}
112
113fn topo_sort_iter<I: Instantiable>(
114    netlist: &Netlist<I>,
115    item: DrivenNet<I>,
116    sorted: &mut Vec<DrivenNet<I>>,
117    rdy: &mut HashSet<DrivenNet<I>>,
118) -> Result<(), AigError> {
119    if rdy.contains(&item) {
120        return Ok(());
121    }
122
123    let mut dfs = DFSIterator::new(netlist, item.clone().unwrap());
124    dfs.next();
125    while let Some(n) = dfs.next() {
126        if n.is_an_input() {
127            continue;
128        }
129
130        if n.outputs().count() != 1 {
131            return Err(AigError::ContainsOtherGates);
132        }
133
134        if dfs.check_cycles() {
135            return Err(AigError::ContainsCycle);
136        }
137
138        let output = n.get_output(0);
139        if !rdy.contains(&output) {
140            topo_sort_iter(netlist, output, sorted, rdy)?;
141        }
142    }
143
144    rdy.insert(item.clone());
145    if !item.is_an_input() {
146        sorted.push(item);
147    }
148
149    Ok(())
150}
151
152fn topo_sort<I: Instantiable>(netlist: &Netlist<I>) -> Result<Vec<DrivenNet<I>>, AigError> {
153    let mut sorted = Vec::new();
154    let mut rdy = HashSet::new();
155
156    for (output, _) in netlist.outputs() {
157        topo_sort_iter(netlist, output, &mut sorted, &mut rdy)?;
158    }
159    Ok(sorted)
160}
161
162/// Convert a Safety Net [Netlist] to an AIG
163pub fn to_aig<I: Instantiable, And: Fn(&I) -> bool, Inv: Fn(&I) -> bool>(
164    netlist: &Rc<Netlist<I>>,
165    and: And,
166    inv: Inv,
167) -> Result<Aig<U>, AigError> {
168    let mut aig = Aig::<U>::default();
169
170    let mut mapping: HashMap<DrivenNet<I>, U> = HashMap::new();
171    for input in netlist.inputs() {
172        let id = aig.inputs.len() as U * 2 + 2;
173        mapping.insert(input.clone(), id);
174        aig.inputs.push(id);
175    }
176
177    // Aig is supposed to be acyclic
178    let nodes = topo_sort(netlist)?;
179
180    for gate in nodes {
181        if mapping.contains_key(&gate) {
182            continue;
183        }
184
185        if inv(&gate.get_instance_type().unwrap()) {
186            let input = gate
187                .clone()
188                .unwrap()
189                .get_input(0)
190                .get_driver()
191                .ok_or(AigError::DisconnectedGates)?;
192            let id = mapping[&input] + 1;
193            mapping.insert(gate, id);
194        } else if and(&gate.get_instance_type().unwrap()) {
195            let input1 = gate
196                .clone()
197                .unwrap()
198                .get_input(0)
199                .get_driver()
200                .ok_or(AigError::DisconnectedGates)?;
201            let input2 = gate
202                .clone()
203                .unwrap()
204                .get_input(1)
205                .get_driver()
206                .ok_or(AigError::DisconnectedGates)?;
207            let id = (aig.and_gates.len() as U * 2) + (aig.inputs.len() as U * 2) + 2;
208            let input_ids = [mapping[&input1], mapping[&input2]];
209            aig.and_gates.push(AndGate {
210                output: id,
211                inputs: input_ids,
212            });
213            mapping.insert(gate, id);
214        } else if let Some(b) = gate.clone().get_instance_type().unwrap().get_constant() {
215            let id = match b {
216                Logic::False => 0,
217                Logic::True => 1,
218                _ => return Err(AigError::ContainsOtherGates),
219            };
220            mapping.insert(gate, id);
221        } else {
222            return Err(AigError::ContainsOtherGates);
223        }
224    }
225
226    for (output, _) in netlist.outputs() {
227        let id = mapping[&output];
228        aig.outputs.push(id);
229    }
230
231    aig.max_var_index = aig.inputs.len() + 1;
232    aig.comment = Some(format!(
233        "/* Generated by {} {} */",
234        env!("CARGO_PKG_NAME"),
235        env!("CARGO_PKG_VERSION")
236    ));
237    Ok(aig)
238}
nl_compiler/aig.rs

nl_compiler/
aig.rs
