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

nl_compiler/
aig.rs
