AIGER writer

docs/changelog.rst

@@ -39,6 +39,7 @@ v0.2 (not yet released)
     - Read BLIF files using *lorina* (`blif_reader`) `#167 <https://github.com/lsils/mockturtle/pull/167>`_
     - Write networks to BLIF files (`write_blif`) `#169 <https://github.com/lsils/mockturtle/pull/169>`_ `#184 <https://github.com/lsils/mockturtle/pull/184>`_
     - Create circuit from integer index list (`create_from_binary_index_list`) `#259 <https://github.com/lsils/mockturtle/pull/259>`_
+    - Write networks to AIGER files (`write_aiger`) `#379 <https://github.com/lsils/mockturtle/pull/379>`_
 * Resynthesis functions:
     - Resynthesis function based on DSD decomposition (`dsd_resynthesis`) `#182 <https://github.com/lsils/mockturtle/pull/182>`_
     - Resynthesis function based on Shannon decomposition (`shannon_resynthesis`) `#185 <https://github.com/lsils/mockturtle/pull/185>`_

docs/io/writers.rst

@@ -4,12 +4,30 @@ Write into file formats
 Write into BENCH files
 ~~~~~~~~~~~~~~~~~~~~~~
 
+**Header:** ``mockturtle/io/write_aiger.hpp``
+
+.. doxygenfunction:: mockturtle::write_aiger(Ntk const&, std::string const&)
+
+.. doxygenfunction:: mockturtle::write_aiger(Ntk const&, std::ostream&)
+
+Write into BENCH files
+~~~~~~~~~~~~~~~~~~~~~~
+
 **Header:** ``mockturtle/io/write_bench.hpp``
 
 .. doxygenfunction:: mockturtle::write_bench(Ntk const&, std::string const&)
 
 .. doxygenfunction:: mockturtle::write_bench(Ntk const&, std::ostream&)
 
+Write into BLIF files
+~~~~~~~~~~~~~~~~~~~~~~
+
+**Header:** ``mockturtle/io/write_blif.hpp``
+
+.. doxygenfunction:: mockturtle::write_blif(Ntk const&, std::string const&)
+
+.. doxygenfunction:: mockturtle::write_blif(Ntk const&, std::ostream&)
+
 Write into structural Verilog files
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -44,4 +62,4 @@ Write simulation patterns into file
 
 .. doxygenfunction:: mockturtle::write_patterns(partial_simulator const&, std::string const&)
 
-.. doxygenfunction:: mockturtle::write_patterns(partial_simulator const&, std::ostream&)
+.. doxygenfunction:: mockturtle::write_patterns(partial_simulator const&, std::ostream&)

include/mockturtle/io/write_aiger.hpp

@@ -0,0 +1,163 @@
+/* mockturtle: C++ logic network library
+ * Copyright (C) 2018-2020  EPFL
+ *
+ * Permission is hereby granted, free of charge, to any person
+ * obtaining a copy of this software and associated documentation
+ * files (the "Software"), to deal in the Software without
+ * restriction, including without limitation the rights to use,
+ * copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the
+ * Software is furnished to do so, subject to the following
+ * conditions:
+ *
+ * The above copyright notice and this permission notice shall be
+ * included in all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+ * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+ * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
+ * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
+ * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+ * OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/*!
+  \file write_aiger.hpp
+  \brief Write networks to AIGER format
+
+  \author Heinz Riener
+
+  A detailed description of the (binary) AIGER format and its encoding is available at [1].
+
+  [1] http://fmv.jku.at/aiger/
+*/
+
+#pragma once
+
+#include "../traits.hpp"
+
+#include <fstream>
+#include <iostream>
+#include <string>
+#include <cstdio>
+
+namespace mockturtle
+{
+
+namespace detail
+{
+
+void encode( std::vector<unsigned char>& buffer, uint32_t lit )
+{
+  unsigned char ch;
+  while ( lit & ~0x7f )
+  {
+    ch = ( lit & 0x7f ) | 0x80;
+    buffer.push_back( ch );
+    lit >>= 7;
+  }
+  ch = lit;
+  buffer.push_back( ch );
+}
+
+} /* detail */
+
+/*! \brief Writes a combinational AIG network in binary AIGER format into a file
+ *
+ * **Required network functions:**
+ * - `num_cis`
+ * - `num_cos`
+ * - `foreach_gate`
+ * - `foreach_fanin`
+ * - `foreach_po`
+ * - `get_node`
+ * - `is_complemented`
+ *
+ * \param aig Combinational AIG network
+ * \param os Output stream
+ */
+void write_aiger( aig_network const& aig, std::ostream& os )
+{
+  static_assert( is_network_type_v<aig_network>, "Ntk is not a network type" );
+  static_assert( has_num_cis_v<aig_network>, "Ntk does not implement the num_cis method" );
+  static_assert( has_num_cos_v<aig_network>, "Ntk does not implement the num_cos method" );
+  static_assert( has_foreach_gate_v<aig_network>, "Ntk does not implement the foreach_gate method" );
+  static_assert( has_foreach_fanin_v<aig_network>, "Ntk does not implement the foreach_fanin method" );
+  static_assert( has_foreach_po_v<aig_network>, "Ntk does not implement the foreach_po method" );
+  static_assert( has_get_node_v<aig_network>, "Ntk does not implement the get_node method" );
+  static_assert( has_is_complemented_v<aig_network>, "Ntk does not implement the is_complemented method" );
+
+  assert( aig.is_combinational() && "Network has to be combinational" );
+
+  using node = aig_network::node;
+  using signal = aig_network::signal;
+
+  assert( aig.num_latches() == 0u );
+  uint32_t const M = aig.num_cis() + aig.num_gates() + aig.num_latches();
+
+  /* HEADER */
+  char string_buffer[1024];
+  sprintf( string_buffer, "aig %u %u %u %u %u\n", M, aig.num_pis(), aig.num_latches(), aig.num_pos(), aig.num_gates() );
+  os.write( &string_buffer[0], sizeof( unsigned char )*strlen( string_buffer ) );
+
+  /* POs */
+  aig.foreach_po( [&]( signal const& f ){
+    sprintf( string_buffer, "%u\n", uint32_t(2*aig.get_node( f ) + aig.is_complemented( f )) );
+    os.write( &string_buffer[0], sizeof( unsigned char )*strlen( string_buffer ) );
+  });
+
+  /* GATES */
+  std::vector<unsigned char> buffer;
+  aig.foreach_gate( [&]( node const& n ){
+    std::vector<uint32_t> lits;
+    lits.push_back( 2*n );
+
+    aig.foreach_fanin( n, [&]( signal const& fi ){
+      lits.push_back( 2*aig.get_node( fi ) + aig.is_complemented( fi ) );
+    });
+
+    if ( lits[1] > lits[2] )
+    {
+      auto const tmp = lits[1];
+      lits[1] = lits[2];
+      lits[2] = tmp;
+    }
+
+    assert( lits[2] < lits[0] );
+    detail::encode( buffer, lits[0] - lits[2] );
+    detail::encode( buffer, lits[2] - lits[1] );
+  });
+
+  for ( const auto& b : buffer )
+  {
+    os.put( b );
+  }
+
+  /* COMMENT */
+  os.put( 'c' );
+}
+
+/*! \brief Writes a combinational AIG network in binary AIGER format into a file
+ *
+ * **Required network functions:**
+ * - `num_cis`
+ * - `num_cos`
+ * - `foreach_gate`
+ * - `foreach_fanin`
+ * - `foreach_po`
+ * - `get_node`
+ * - `is_complemented`
+ *
+ * \param aig Combinational AIG network
+ * \param filename Filename
+ */
+void write_aiger( aig_network const& aig, std::string const& filename )
+{
+  std::ofstream os( filename.c_str(), std::ofstream::out );
+  write_aiger( aig, os );
+  os.close();
+}
+
+} /* namespace mockturtle */

test/io/write_aiger.cpp

@@ -0,0 +1,99 @@
+#include <catch.hpp>
+
+#include <mockturtle/networks/aig.hpp>
+#include <mockturtle/io/write_aiger.hpp>
+
+template<
+  typename T,
+  typename Traits = std::char_traits<T>,
+  typename Container = std::vector<T>
+>
+struct seq_buffer : std::basic_streambuf<T, Traits>
+{
+  using base_type = std::basic_streambuf<T, Traits>;
+  using int_type = typename base_type::int_type;
+  using traits_type = typename base_type::traits_type;
+
+  virtual int_type overflow( int_type ch )
+  {
+    if ( traits_type::eq_int_type( ch, traits_type::eof() ) )
+    {
+      return traits_type::eof();
+    }
+    c.push_back( traits_type::to_char_type( ch ) );
+    return ch;
+  }
+
+  Container const& data() const
+  {
+    return c;
+  }
+
+private:
+  Container c;
+};
+
+using namespace mockturtle;
+
+TEST_CASE( "write single-gate AIG into AIGER file", "[write_aiger]" )
+{
+  aig_network aig;
+
+  const auto a = aig.create_pi();
+  const auto b = aig.create_pi();
+
+  const auto f1 = aig.create_or( a, b );
+  aig.create_po( f1 );
+
+  seq_buffer<char> buffer;
+  std::ostream os( &buffer );
+  write_aiger( aig, os );
+
+  CHECK( buffer.data() ==
+         std::vector<char>{
+           0x61, 0x69, 0x67, 0x20, // aig
+           0x33, 0x20, // M=3 (I+L+A)
+           0x32, 0x20, // I=2
+           0x30, 0x20, // L=0
+           0x31, 0x20, // O=1
+           0x31, 0x0a, // A=1
+           0x37, 0x0a, // 1 PO
+           0x01, 0x02, // 1 AND gate
+           0x63 // comment
+         } );
+}
+
+TEST_CASE( "write AIG for XOR into AIGERfile", "[write_aiger]" )
+{
+  aig_network aig;
+
+  const auto a = aig.create_pi();
+  const auto b = aig.create_pi();
+
+  const auto f1 = aig.create_nand( a, b );
+  const auto f2 = aig.create_nand( a, f1 );
+  const auto f3 = aig.create_nand( b, f1 );
+  const auto f4 = aig.create_nand( f2, f3 );
+  aig.create_po( f4 );
+
+  seq_buffer<char> buffer;
+  std::ostream os( &buffer );
+  write_aiger( aig, os );
+  write_aiger( aig, "test.aig" );
+
+  CHECK( buffer.data() ==
+         std::vector<char>{
+           0x61, 0x69, 0x67, 0x20, // aig
+           0x36, 0x20, // M=6 (I+L+A)
+           0x32, 0x20, // I=2
+           0x30, 0x20, // L=0
+           0x31, 0x20, // O=1
+           0x34, 0x0a, // A=4
+           0x31, 0x33, 0x0a, // 1 PO
+           0x02, 0x02, // 4 AND gates
+           0x01, 0x05,
+           0x03, 0x03,
+           0x01, 0x02,
+           0x63 // comment
+         } );
+}