diff --git a/include/mockturtle/io/aiger_reader.hpp b/include/mockturtle/io/aiger_reader.hpp index 218d01519..905cd6c55 100644 --- a/include/mockturtle/io/aiger_reader.hpp +++ b/include/mockturtle/io/aiger_reader.hpp @@ -38,6 +38,7 @@ #include "../networks/sequential.hpp" #include "../traits.hpp" #include +#include namespace mockturtle { @@ -54,6 +55,14 @@ namespace mockturtle * **Optional network functions to support sequential networks:** * - `create_ri` * - `create_ro` + * + * A network type that implements neither cannot hold registers. Reading a + * latched AIGER file into one flattens a single timeframe of the design: each + * latch output becomes a primary input, appended behind the file's own primary + * inputs, and each latch next-state function becomes a primary output, appended + * behind the file's own primary outputs. No logic is lost, but the sequential + * behaviour is: the registers become free inputs. Use a `sequential` to + * read the design as the sequential network it is. * \verbatim embed:rst @@ -82,6 +91,9 @@ class aiger_reader : public lorina::aiger_reader static_assert( has_create_and_v, "Ntk does not implement the create_and function" ); } + /*! \brief Whether the network type can hold registers. */ + static constexpr bool has_registers = has_create_ri_v && has_create_ro_v; + ~aiger_reader() { uint32_t output_id{ 0 }; @@ -104,39 +116,48 @@ class aiger_reader : public lorina::aiger_reader _ntk.create_po( signal ); } - if constexpr ( has_create_ri_v ) + for ( auto i = 0u; i < latches.size(); ++i ) { - for ( auto i = 0u; i < latches.size(); ++i ) - { - auto& latch = latches[i]; - auto const lit = std::get<0>( latch ); - auto const reset = std::get<1>( latch ); + auto& latch = latches[i]; + auto const lit = std::get<0>( latch ); - auto signal = signals[lit >> 1]; - if ( lit & 1 ) - { - signal = _ntk.create_not( signal ); - } + auto signal = signals[lit >> 1]; + if ( lit & 1 ) + { + signal = _ntk.create_not( signal ); + } - if constexpr ( has_set_name_v ) - { - _ntk.set_name( signal, std::get<2>( latch ) + "_next" ); - } + if constexpr ( has_set_name_v ) + { + _ntk.set_name( signal, std::get<2>( latch ) + "_next" ); + } + if constexpr ( has_registers ) + { _ntk.create_ri( signal ); register_t reg; - reg.init = reset; + reg.init = std::get<1>( latch ); _ntk.set_register( i, reg ); } + else + { + /* The network cannot hold registers. `on_header` materialized the latch + outputs as primary inputs, so keep their next-state functions by + appending them as primary outputs; dropping them would silently + discard every gate that only feeds a register. */ + _ntk.create_po( signal ); + } } } void on_header( uint64_t, uint64_t num_inputs, uint64_t num_latches, uint64_t, uint64_t ) const override { - (void)num_latches; - if constexpr ( !has_create_ri_v || !has_create_ro_v ) + if constexpr ( !has_registers ) { - assert( num_latches == 0 && "network type does not support the creation of latches" ); + if ( num_latches != 0u ) + { + std::cerr << "[w] network type does not support latches, applying comb: ROs become PIs, RIs become POs\n"; + } } _num_inputs = static_cast( num_inputs ); @@ -150,13 +171,21 @@ class aiger_reader : public lorina::aiger_reader signals.push_back( _ntk.create_pi() ); } - if constexpr ( has_create_ro_v ) + /* create latch outputs (ro), or primary inputs standing in for them. Every + AIGER literal above `1 + num_inputs` refers to one of these, so a signal + must be pushed for each of them whether the network can hold registers or + not: skipping them leaves `signals` short and `on_and` reads past its + end. */ + for ( auto i = 0u; i < num_latches; ++i ) { - /* create latch outputs (ro) */ - for ( auto i = 0u; i < num_latches; ++i ) + if constexpr ( has_registers ) { signals.push_back( _ntk.create_ro() ); } + else + { + signals.push_back( _ntk.create_pi() ); + } } } @@ -175,14 +204,11 @@ class aiger_reader : public lorina::aiger_reader void on_latch_name( unsigned index, const std::string& name ) const override { - if constexpr ( has_create_ri_v && has_create_ro_v ) + if constexpr ( has_set_name_v ) { - if constexpr ( has_set_name_v ) - { - _ntk.set_name( signals[1 + _num_inputs + index], name ); - } - std::get<2>( latches[index] ) = name; + _ntk.set_name( signals[1 + _num_inputs + index], name ); } + std::get<2>( latches[index] ) = name; } void on_and( unsigned index, unsigned left_lit, unsigned right_lit ) const override @@ -207,16 +233,13 @@ class aiger_reader : public lorina::aiger_reader void on_latch( unsigned index, unsigned next, latch_init_value reset ) const override { - if constexpr ( has_create_ri_v && has_create_ro_v ) - { - (void)index; - /* AIGER cannot express `unknown`: a latch either has a defined reset value - or is explicitly nondeterministic. */ - uint8_t const r = reset == latch_init_value::NONDETERMINISTIC ? register_init::dont_care - : reset == latch_init_value::ONE ? register_init::one - : register_init::zero; - latches.push_back( std::make_tuple( next, r, "" ) ); - } + (void)index; + /* AIGER cannot express `unknown`: a latch either has a defined reset value + or is explicitly nondeterministic. */ + uint8_t const r = reset == latch_init_value::NONDETERMINISTIC ? register_init::dont_care + : reset == latch_init_value::ONE ? register_init::one + : register_init::zero; + latches.push_back( std::make_tuple( next, r, "" ) ); } void on_output( unsigned index, unsigned lit ) const override @@ -255,4 +278,4 @@ class aiger_reader : public lorina::aiger_reader mutable std::vector> latches; }; -} /* namespace mockturtle */ \ No newline at end of file +} /* namespace mockturtle */ diff --git a/test/io/aiger_reader.cpp b/test/io/aiger_reader.cpp index 1258e67c9..c40f17689 100644 --- a/test/io/aiger_reader.cpp +++ b/test/io/aiger_reader.cpp @@ -7,6 +7,7 @@ #include +#include #include #include #include @@ -246,3 +247,106 @@ TEST_CASE( "register initialization stays valid across formats", "[aiger_reader] CHECK( register_init::is_defined( aig.register_at( 0 ).init ) == ( expected <= register_init::one ) ); } } + +TEST_CASE( "read a latched Aiger file into a combinational network", "[aiger_reader]" ) +{ + /* a network that cannot hold registers flattens one timeframe of the design: + the latch outputs become primary inputs and their next-state functions + become primary outputs. The latch outputs used to be skipped entirely, + which left the reader's signal vector short of every literal above the + primary inputs and made `on_and` read past its end. */ + aig_network combinational; + sequential seq; + + std::string const file{ "aag 7 2 1 2 4\n" + "2\n" + "4\n" + "6 8\n" + "6\n" + "7\n" + "8 2 6\n" + "10 3 7\n" + "12 9 11\n" + "14 4 12\n" }; + + std::stringstream err; + auto* old_err = std::cerr.rdbuf( err.rdbuf() ); + + std::istringstream in( file ); + CHECK( lorina::read_ascii_aiger( in, aiger_reader( combinational ) ) == lorina::return_code::success ); + + std::cerr.rdbuf( old_err ); + + std::istringstream seq_in( file ); + CHECK( lorina::read_ascii_aiger( seq_in, aiger_reader( seq ) ) == lorina::return_code::success ); + + /* the latch output is an input and its next-state function an output */ + CHECK( combinational.num_pis() == 3 ); + CHECK( combinational.num_pos() == 3 ); + + /* no logic is gained or lost by flattening */ + CHECK( combinational.num_gates() == seq.num_gates() ); + CHECK( combinational.size() == seq.size() ); + CHECK( combinational.num_cis() == seq.num_cis() ); + CHECK( combinational.num_cos() == seq.num_cos() ); + CHECK( err.str().find( "applying comb: ROs become PIs, RIs become POs" ) != std::string::npos ); +} + +TEST_CASE( "read a latched Aiger file with no primary inputs", "[aiger_reader]" ) +{ + /* a design driven only by its registers -- an LFSR, say -- reaches every one + of its literals through a latch output, so it flattens into a network whose + inputs are all former latch outputs */ + aig_network combinational; + + std::string const file{ "aag 3 0 2 1 1\n" + "2 6\n" + "4 2\n" + "6\n" + "6 2 4\n" }; + + std::stringstream err; + auto* old_err = std::cerr.rdbuf( err.rdbuf() ); + + std::istringstream in( file ); + CHECK( lorina::read_ascii_aiger( in, aiger_reader( combinational ) ) == lorina::return_code::success ); + + std::cerr.rdbuf( old_err ); + + CHECK( combinational.num_pis() == 2 ); + CHECK( combinational.num_pos() == 3 ); + CHECK( combinational.num_gates() == 1 ); + CHECK( err.str().find( "applying comb: ROs become PIs, RIs become POs" ) != std::string::npos ); +} + +TEST_CASE( "name a flattened latch output", "[aiger_reader]" ) +{ + /* the symbol table still applies: a latch name belongs to the input that + stands in for it, and its next-state function keeps the `_next` suffix */ + names_view aig; + + std::string const file{ "aag 7 2 1 2 4\n" + "2\n" + "4\n" + "6 8\n" + "6\n" + "7\n" + "8 2 6\n" + "10 3 7\n" + "12 9 11\n" + "14 4 12\n" + "i0 x0\n" + "l0 s0\n" }; + + std::stringstream err; + auto* old_err = std::cerr.rdbuf( err.rdbuf() ); + + std::istringstream in( file ); + CHECK( lorina::read_ascii_aiger( in, aiger_reader( aig ) ) == lorina::return_code::success ); + + std::cerr.rdbuf( old_err ); + + CHECK( aig.get_name( aig.make_signal( aig.pi_at( 0 ) ) ) == "x0" ); + CHECK( aig.get_name( aig.make_signal( aig.pi_at( 2 ) ) ) == "s0" ); + CHECK( err.str().find( "applying comb: ROs become PIs, RIs become POs" ) != std::string::npos ); +}