From e3ff01c8035bd72ac5355ad2a9df5aaddfb817f0 Mon Sep 17 00:00:00 2001 From: Marcel Walter Date: Fri, 21 Aug 2026 17:09:39 +0200 Subject: [PATCH 1/2] =?UTF-8?q?=F0=9F=90=9B=20Fix=20reading=20a=20latched?= =?UTF-8?q?=20AIGER=20file=20into=20a=20combinational=20network?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `aiger_reader::on_header` only materialized the latch outputs when the network type implements `create_ro`. For one that does not, the reader's `signals` vector was left short by exactly the latch count, while every AIGER literal above the primary inputs still assumed those slots existed. `on_and` then indexed past the end of the vector and handed the garbage it read to `create_and`. The only thing standing between that and undefined behaviour was assert( num_latches == 0 && "network type does not support the creation of latches" ); which is compiled out under `NDEBUG` -- that is, in every release build. The result was a segmentation fault on any design whose logic reaches far enough past the latch outputs, and a silently wrong network on any that does not: a one-latch file whose literals all stay in bounds parsed "successfully" into a network missing its registers entirely. Reading a latched file into a combinational network now flattens one timeframe of the design instead. 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. That is the transformation ABC calls `comb`; it loses no logic, keeps every literal resolving to the signal the file names, and makes the network type in this reader's own documented example -- `mig_network`, which has no registers -- work on a sequential file rather than crash on one. Recording and naming latches is no longer conditional on the network type either, since the flattened path needs both. The header and the destructor also disagreed about which trait decides whether a network can hold registers, `create_ro` in one and `create_ri` in the other; both now consult a single `has_registers` predicate, which is what let them drift apart to begin with. Co-Authored-By: Claude Opus 5 --- include/mockturtle/io/aiger_reader.hpp | 96 +++++++++++++++----------- test/io/aiger_reader.cpp | 85 +++++++++++++++++++++++ 2 files changed, 140 insertions(+), 41 deletions(-) diff --git a/include/mockturtle/io/aiger_reader.hpp b/include/mockturtle/io/aiger_reader.hpp index 218d01519..3e69afdbf 100644 --- a/include/mockturtle/io/aiger_reader.hpp +++ b/include/mockturtle/io/aiger_reader.hpp @@ -54,6 +54,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 +90,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,41 +115,42 @@ 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 ) - { - assert( num_latches == 0 && "network type does not support the creation of latches" ); - } - _num_inputs = static_cast( num_inputs ); /* constant */ @@ -150,13 +162,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 +195,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 +224,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 diff --git a/test/io/aiger_reader.cpp b/test/io/aiger_reader.cpp index 1258e67c9..8cfbb6ed2 100644 --- a/test/io/aiger_reader.cpp +++ b/test/io/aiger_reader.cpp @@ -246,3 +246,88 @@ 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::istringstream in( file ); + CHECK( lorina::read_ascii_aiger( in, aiger_reader( combinational ) ) == lorina::return_code::success ); + + 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() ); +} + +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::istringstream in( file ); + CHECK( lorina::read_ascii_aiger( in, aiger_reader( combinational ) ) == lorina::return_code::success ); + + CHECK( combinational.num_pis() == 2 ); + CHECK( combinational.num_pos() == 3 ); + CHECK( combinational.num_gates() == 1 ); +} + +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::istringstream in( file ); + CHECK( lorina::read_ascii_aiger( in, aiger_reader( aig ) ) == lorina::return_code::success ); + + CHECK( aig.get_name( aig.make_signal( aig.pi_at( 0 ) ) ) == "x0" ); + CHECK( aig.get_name( aig.make_signal( aig.pi_at( 2 ) ) ) == "s0" ); +} From 4d2aa08c6082ec1e74f79ce73e0008c9d4d69351 Mon Sep 17 00:00:00 2001 From: MyskYko Date: Sat, 29 Aug 2026 19:34:17 +0200 Subject: [PATCH 2/2] Warn when flattening latched AIGER --- include/mockturtle/io/aiger_reader.hpp | 11 ++++++++++- test/io/aiger_reader.cpp | 19 +++++++++++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) diff --git a/include/mockturtle/io/aiger_reader.hpp b/include/mockturtle/io/aiger_reader.hpp index 3e69afdbf..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 { @@ -151,6 +152,14 @@ class aiger_reader : public lorina::aiger_reader void on_header( uint64_t, uint64_t num_inputs, uint64_t num_latches, uint64_t, uint64_t ) const override { + if constexpr ( !has_registers ) + { + 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 ); /* constant */ @@ -269,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 8cfbb6ed2..c40f17689 100644 --- a/test/io/aiger_reader.cpp +++ b/test/io/aiger_reader.cpp @@ -7,6 +7,7 @@ #include +#include #include #include #include @@ -268,9 +269,14 @@ TEST_CASE( "read a latched Aiger file into a combinational network", "[aiger_rea "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 ); @@ -283,6 +289,7 @@ TEST_CASE( "read a latched Aiger file into a combinational network", "[aiger_rea 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]" ) @@ -298,12 +305,18 @@ TEST_CASE( "read a latched Aiger file with no primary inputs", "[aiger_reader]" "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]" ) @@ -325,9 +338,15 @@ TEST_CASE( "name a flattened latch output", "[aiger_reader]" ) "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 ); }