diff --git a/docs/changelog.rst b/docs/changelog.rst index 701ee68af..43dc4e029 100644 --- a/docs/changelog.rst +++ b/docs/changelog.rst @@ -39,6 +39,7 @@ v0.2 (not yet released) - Read BLIF files using *lorina* (`blif_reader`) `#167 `_ - Write networks to BLIF files (`write_blif`) `#169 `_ `#184 `_ - Create circuit from integer index list (`create_from_binary_index_list`) `#259 `_ + - Write networks to AIGER files (`write_aiger`) `#379 `_ * Resynthesis functions: - Resynthesis function based on DSD decomposition (`dsd_resynthesis`) `#182 `_ - Resynthesis function based on Shannon decomposition (`shannon_resynthesis`) `#185 `_ diff --git a/docs/io/writers.rst b/docs/io/writers.rst index f7a069054..de50acd31 100644 --- a/docs/io/writers.rst +++ b/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&) \ No newline at end of file +.. doxygenfunction:: mockturtle::write_patterns(partial_simulator const&, std::ostream&) diff --git a/include/mockturtle/io/write_aiger.hpp b/include/mockturtle/io/write_aiger.hpp new file mode 100644 index 000000000..1b19477c0 --- /dev/null +++ b/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 +#include +#include +#include + +namespace mockturtle +{ + +namespace detail +{ + +void encode( std::vector& 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, "Ntk is not a network type" ); + static_assert( has_num_cis_v, "Ntk does not implement the num_cis method" ); + static_assert( has_num_cos_v, "Ntk does not implement the num_cos method" ); + static_assert( has_foreach_gate_v, "Ntk does not implement the foreach_gate method" ); + static_assert( has_foreach_fanin_v, "Ntk does not implement the foreach_fanin method" ); + static_assert( has_foreach_po_v, "Ntk does not implement the foreach_po method" ); + static_assert( has_get_node_v, "Ntk does not implement the get_node method" ); + static_assert( has_is_complemented_v, "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 buffer; + aig.foreach_gate( [&]( node const& n ){ + std::vector 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 */ diff --git a/test/io/write_aiger.cpp b/test/io/write_aiger.cpp new file mode 100644 index 000000000..a6b5e9d8b --- /dev/null +++ b/test/io/write_aiger.cpp @@ -0,0 +1,99 @@ +#include + +#include +#include + +template< + typename T, + typename Traits = std::char_traits, + typename Container = std::vector +> +struct seq_buffer : std::basic_streambuf +{ + using base_type = std::basic_streambuf; + 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 buffer; + std::ostream os( &buffer ); + write_aiger( aig, os ); + + CHECK( buffer.data() == + std::vector{ + 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 buffer; + std::ostream os( &buffer ); + write_aiger( aig, os ); + write_aiger( aig, "test.aig" ); + + CHECK( buffer.data() == + std::vector{ + 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 + } ); +}