Merge pull request #1079 from YosysHQ/eddie/fix_read_aiger

Fix read_aiger to really get tested, and fix some uncovered read_aiger issues

27 files changed, 128 insertions, 45 deletions

diff --git a/CHANGELOG b/CHANGELOG
index 36b64e111..839fefcf1 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -16,6 +16,7 @@ Yosys 0.8 .. Yosys 0.8-dev
     - Added "gate2lut.v" techmap rule
     - Added "rename -src"
     - Added "equiv_opt" pass
+    - Added "read_aiger" frontend
     - "synth_xilinx" to now infer hard shift registers, using new "shregmap -tech xilinx"
 
 
diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index 38348cd65..32be4cf6c 100644
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -81,11 +81,26 @@ end_of_header:
     else
         log_abort();
 
+    RTLIL::Wire* n0 = module->wire("\\n0");
+    if (n0)
+        module->connect(n0, RTLIL::S0);
+
+    for (unsigned i = 0; i < outputs.size(); ++i) {
+        RTLIL::Wire *wire = outputs[i];
+        if (wire->port_input) {
+            RTLIL::Wire *o_wire = module->addWire(wire->name.str() + "_o");
+            o_wire->port_output = true;
+            wire->port_output = false;
+            module->connect(o_wire, wire);
+            outputs[i] = o_wire;
+        }
+    }
+
     // Parse footer (symbol table, comments, etc.)
     unsigned l1;
     std::string s;
     for (int c = f.peek(); c != EOF; c = f.peek(), ++line_count) {
-        if (c == 'i' || c == 'l' || c == 'o') {
+        if (c == 'i' || c == 'l' || c == 'o' || c == 'b') {
             f.ignore(1);
             if (!(f >> l1 >> s))
                 log_error("Line %u cannot be interpreted as a symbol entry!\n", line_count);
@@ -97,11 +112,12 @@ end_of_header:
             if (c == 'i') wire = inputs[l1];
             else if (c == 'l') wire = latches[l1];
             else if (c == 'o') wire = outputs[l1];
+            else if (c == 'b') wire = bad_properties[l1];
             else log_abort();
 
             module->rename(wire, stringf("\\%s", s.c_str()));
         }
-        else if (c == 'b' || c == 'j' || c == 'f') {
+        else if (c == 'j' || c == 'f') {
             // TODO
         }
         else if (c == 'c') {
@@ -153,7 +169,7 @@ void AigerReader::parse_aiger_ascii()
     unsigned l1, l2, l3;
 
     // Parse inputs
-    for (unsigned i = 0; i < I; ++i, ++line_count) {
+    for (unsigned i = 1; i <= I; ++i, ++line_count) {
         if (!(f >> l1))
             log_error("Line %u cannot be interpreted as an input!\n", line_count);
         log_debug("%d is an input\n", l1);
@@ -187,8 +203,10 @@ void AigerReader::parse_aiger_ascii()
             if (!(f >> l3))
                 log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 
-            if (l3 == 0 || l3 == 1)
-                q_wire->attributes["\\init"] = RTLIL::Const(l3);
+            if (l3 == 0)
+                q_wire->attributes["\\init"] = RTLIL::S0;
+            else if (l3 == 1)
+                q_wire->attributes["\\init"] = RTLIL::S1;
             else if (l3 == l1) {
                 //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
             }
@@ -197,7 +215,7 @@ void AigerReader::parse_aiger_ascii()
         }
         else {
             // AIGER latches are assumed to be initialized to zero
-            q_wire->attributes["\\init"] = RTLIL::Const(0);
+            q_wire->attributes["\\init"] = RTLIL::S0;
         }
         latches.push_back(q_wire);
     }
@@ -212,11 +230,17 @@ void AigerReader::parse_aiger_ascii()
         wire->port_output = true;
         outputs.push_back(wire);
     }
-    std::getline(f, line); // Ignore up to start of next line
 
-    // TODO: Parse bad state properties
-    for (unsigned i = 0; i < B; ++i, ++line_count)
-        std::getline(f, line); // Ignore up to start of next line
+    // Parse bad properties
+    for (unsigned i = 0; i < B; ++i, ++line_count) {
+        if (!(f >> l1))
+            log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
+
+        log_debug("%d is a bad state property\n", l1);
+        RTLIL::Wire *wire = createWireIfNotExists(module, l1);
+        wire->port_output = true;
+        bad_properties.push_back(wire);
+    }
 
     // TODO: Parse invariant constraints
     for (unsigned i = 0; i < C; ++i, ++line_count)
@@ -290,8 +314,10 @@ void AigerReader::parse_aiger_binary()
             if (!(f >> l3))
                 log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 
-            if (l3 == 0 || l3 == 1)
-                q_wire->attributes["\\init"] = RTLIL::Const(l3);
+            if (l3 == 0)
+                q_wire->attributes["\\init"] = RTLIL::S0;
+            else if (l3 == 1)
+                q_wire->attributes["\\init"] = RTLIL::S1;
             else if (l3 == l1) {
                 //q_wire->attributes["\\init"] = RTLIL::Const(RTLIL::State::Sx);
             }
@@ -300,7 +326,7 @@ void AigerReader::parse_aiger_binary()
         }
         else {
             // AIGER latches are assumed to be initialized to zero
-            q_wire->attributes["\\init"] = RTLIL::Const(0);
+            q_wire->attributes["\\init"] = RTLIL::S0;
         }
         latches.push_back(q_wire);
     }
@@ -317,8 +343,17 @@ void AigerReader::parse_aiger_binary()
     }
     std::getline(f, line); // Ignore up to start of next line
 
-    // TODO: Parse bad state properties
-    for (unsigned i = 0; i < B; ++i, ++line_count)
+    // Parse bad properties
+    for (unsigned i = 0; i < B; ++i, ++line_count) {
+        if (!(f >> l1))
+            log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
+
+        log_debug("%d is a bad state property\n", l1);
+        RTLIL::Wire *wire = createWireIfNotExists(module, l1);
+        wire->port_output = true;
+        bad_properties.push_back(wire);
+    }
+    if (B > 0)
         std::getline(f, line); // Ignore up to start of next line
 
     // TODO: Parse invariant constraints
diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h
index c49cd152d..0e3719cc4 100644
--- a/frontends/aiger/aigerparse.h
+++ b/frontends/aiger/aigerparse.h
@@ -39,6 +39,7 @@ struct AigerReader
     std::vector<RTLIL::Wire*> inputs;
     std::vector<RTLIL::Wire*> latches;
     std::vector<RTLIL::Wire*> outputs;
+    std::vector<RTLIL::Wire*> bad_properties;
 
     AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name);
     void parse_aiger();
diff --git a/tests/aiger/and.aig b/tests/aiger/and.aig
deleted file mode 100644
index da0fa0719..000000000
--- a/tests/aiger/and.aig
+++ /dev/null
@@ -1,3 +0,0 @@
-aig 3 2 0 1 1
-6
-
\ No newline at end of file
diff --git a/tests/aiger/and.aag b/tests/aiger/and_.aag
index d1ef2c5a5..cadd505f0 100644
--- a/tests/aiger/and.aag
+++ b/tests/aiger/and_.aag
@@ -3,3 +3,6 @@ aag 3 2 0 1 1
 4
 6
 6 2 4
+i0 pi0
+i1 pi1
+o0 po0
diff --git a/tests/aiger/and_.aig b/tests/aiger/and_.aig
new file mode 100644
index 000000000..13c7a0c17
--- /dev/null
+++ b/tests/aiger/and_.aig
@@ -0,0 +1,5 @@
+aig 3 2 0 1 1
+6
+i0 pi0
+i1 pi1
+o0 po0
diff --git a/tests/aiger/buffer.aag b/tests/aiger/buffer.aag
index 94a6fb1ed..211106ed6 100644
--- a/tests/aiger/buffer.aag
+++ b/tests/aiger/buffer.aag
@@ -1,3 +1,5 @@
 aag 1 1 0 1 0
 2
 2
+i0 pi0
+o0 po0
diff --git a/tests/aiger/buffer.aig b/tests/aiger/buffer.aig
index 0c715fdeb..01df6f1cf 100644
--- a/tests/aiger/buffer.aig
+++ b/tests/aiger/buffer.aig
@@ -1,2 +1,4 @@
 aig 1 1 0 1 0
 2
+i0 pi0
+o0 po0
diff --git a/tests/aiger/cnt1.aag b/tests/aiger/cnt1.aag
index ce4f28fcb..75598862c 100644
--- a/tests/aiger/cnt1.aag
+++ b/tests/aiger/cnt1.aag
@@ -1,3 +1,4 @@
 aag 1 0 1 0 0 1
 2 3
 2
+b0 po0
diff --git a/tests/aiger/cnt1.aig b/tests/aiger/cnt1.aig
index 8d0ba13b1..6fcf62522 100644
--- a/tests/aiger/cnt1.aig
+++ b/tests/aiger/cnt1.aig
@@ -1,3 +1,4 @@
 aig 1 0 1 0 0 1
 3
 2
+b0 po0
diff --git a/tests/aiger/cnt1e.aag b/tests/aiger/cnt1e.aag
index 6db3f0ffd..35cd5a482 100644
--- a/tests/aiger/cnt1e.aag
+++ b/tests/aiger/cnt1e.aag
@@ -6,3 +6,4 @@ aag 5 1 1 0 3 1
 8 4 2
 10 9 7
 b0 AIGER_NEVER
+i0 po0
diff --git a/tests/aiger/cnt1e.aig b/tests/aiger/cnt1e.aig
index d8d159f11..7284dd42a 100644
--- a/tests/aiger/cnt1e.aig
+++ b/tests/aiger/cnt1e.aig
@@ -1,4 +1,5 @@
 aig 5 1 1 0 3 1
 10
 4
-

b0 AIGER_NEVER
+

i0 po0
+b0 AIGER_NEVER
diff --git a/tests/aiger/false.aag b/tests/aiger/false.aag
index 421e64a91..bab4a06a6 100644
--- a/tests/aiger/false.aag
+++ b/tests/aiger/false.aag
@@ -1,2 +1,3 @@
 aag 0 0 0 1 0
 0
+o0 po0
diff --git a/tests/aiger/false.aig b/tests/aiger/false.aig
index ad7d039fa..4dc442d7b 100644
--- a/tests/aiger/false.aig
+++ b/tests/aiger/false.aig
@@ -1,2 +1,3 @@
 aig 0 0 0 1 0
 0
+o0 po0
diff --git a/tests/aiger/inverter.aag b/tests/aiger/inverter.aag
index ff7c28542..428bad9e4 100644
--- a/tests/aiger/inverter.aag
+++ b/tests/aiger/inverter.aag
@@ -1,3 +1,5 @@
 aag 1 1 0 1 0
 2
 3
+i0 pi0
+o0 po0
diff --git a/tests/aiger/inverter.aig b/tests/aiger/inverter.aig
index 525d82392..5bec90ae3 100644
--- a/tests/aiger/inverter.aig
+++ b/tests/aiger/inverter.aig
@@ -1,2 +1,4 @@
 aig 1 1 0 1 0
 3
+i0 pi0
+o0 po0
diff --git a/tests/aiger/notcnt1e.aag b/tests/aiger/notcnt1e.aag
index 141c864f7..2ed645d84 100644
--- a/tests/aiger/notcnt1e.aag
+++ b/tests/aiger/notcnt1e.aag
@@ -6,3 +6,4 @@ aag 5 1 1 0 3 1
 8 4 2
 10 9 7
 b0 AIGER_NEVER
+i0 pi0
diff --git a/tests/aiger/notcnt1e.aig b/tests/aiger/notcnt1e.aig
index 7c85a7290..fd7e94508 100644
--- a/tests/aiger/notcnt1e.aig
+++ b/tests/aiger/notcnt1e.aig
@@ -1,4 +1,5 @@
 aig 5 1 1 0 3 1
 10
 5
-

b0 AIGER_NEVER
+

i0 pi0
+b0 AIGER_NEVER
diff --git a/tests/aiger/or.aig b/tests/aiger/or.aig
deleted file mode 100644
index 75c9e4480..000000000
--- a/tests/aiger/or.aig
+++ /dev/null
@@ -1,3 +0,0 @@
-aig 3 2 0 1 1
-7
-

\ No newline at end of file
diff --git a/tests/aiger/or.aag b/tests/aiger/or_.aag
index f780e339f..0f619dba3 100644
--- a/tests/aiger/or.aag
+++ b/tests/aiger/or_.aag
@@ -3,3 +3,6 @@ aag 3 2 0 1 1
 4
 7
 6 3 5
+i0 pi0
+i1 pi1
+o0 po0
diff --git a/tests/aiger/or_.aig b/tests/aiger/or_.aig
new file mode 100644
index 000000000..051687512
--- /dev/null
+++ b/tests/aiger/or_.aig
@@ -0,0 +1,5 @@
+aig 3 2 0 1 1
+7
+
i0 pi0
+i1 pi1
+o0 po0
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index e0a34f023..e56d0fa80 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -1,24 +1,37 @@
 #!/bin/bash
 
-OPTIND=1
-seed=""    # default to no seed specified
-while getopts "S:" opt
-do
-    case "$opt" in
-	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
-	   seed="SEED=$arg" ;;
-    esac
-done
-shift "$((OPTIND-1))"
-
-# check for Icarus Verilog
-if ! which iverilog > /dev/null ; then
-  echo "$0: Error: Icarus Verilog 'iverilog' not found."
-  exit 1
-fi
+set -e
 
-echo "===== AAG ======"
-${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger"
+for aag in *.aag; do
+    # Since ABC cannot read *.aag, read the *.aig instead
+    # (which would have been created by the reference aig2aig utility)
+    ../../yosys-abc -c "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
+    ../../yosys -p "
+read_verilog ${aag%.*}_ref.v
+prep
+design -stash gold
+read_aiger -clk_name clock $aag
+prep
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 16 miter
+"
+done
 
-echo "===== AIG ======"
-exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aig EXTRA_FLAGS="-f aiger"
+for aig in *.aig; do
+    ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
+    ../../yosys -p "
+read_verilog ${aig%.*}_ref.v
+prep
+design -stash gold
+read_aiger -clk_name clock $aig
+prep
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -seq 16 miter
+"
+done
diff --git a/tests/aiger/toggle.aag b/tests/aiger/toggle.aag
index 09651012d..b1a1582d7 100644
--- a/tests/aiger/toggle.aag
+++ b/tests/aiger/toggle.aag
@@ -2,3 +2,5 @@ aag 1 0 1 2 0
 2 3
 2
 3
+o0 po0
+o1 po1
diff --git a/tests/aiger/toggle.aig b/tests/aiger/toggle.aig
index b69e21aaf..68b41763f 100644
--- a/tests/aiger/toggle.aig
+++ b/tests/aiger/toggle.aig
@@ -2,3 +2,5 @@ aig 1 0 1 2 0
 3
 2
 3
+o0 po0
+o1 po1
diff --git a/tests/aiger/true.aag b/tests/aiger/true.aag
index 366893648..66a9eab46 100644
--- a/tests/aiger/true.aag
+++ b/tests/aiger/true.aag
@@ -1,2 +1,3 @@
 aag 0 0 0 1 0
 1
+o0 po0
diff --git a/tests/aiger/true.aig b/tests/aiger/true.aig
index 10086f389..f9bad6000 100644
--- a/tests/aiger/true.aig
+++ b/tests/aiger/true.aig
@@ -1,2 +1,3 @@
 aig 0 0 0 1 0
 1
+o0 po0
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 0a511f29c..23964a751 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -146,9 +146,10 @@ do
 		rm -f ${bn}_ref.fir
 		if [[ "$ext" == "v" ]]; then
 			egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
+		elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then
+			"$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.v"
 		else
-			"$toolsdir"/../../yosys -f "$frontend $include_opts" -b "verilog" -o ${bn}_ref.v ../${fn}
-			frontend="verilog -noblackbox"
+			cp ../${fn} ${bn}_ref.${ext}
 		fi
 
 		if [ ! -f ../${bn}_tb.v ]; then