Skip to content

🐛 Fix reading a latched AIGER file into a combinational network #705

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myskyko merged 2 commits into from
Aug 29, 2026
Merged

🐛 Fix reading a latched AIGER file into a combinational network #705

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e3ff01c
🐛 Fix reading a latched AIGER file into a combinational network
marcelwa Aug 21, 2026
4d2aa08
Warn when flattening latched AIGER
myskyko Aug 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
101 changes: 62 additions & 39 deletions include/mockturtle/io/aiger_reader.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@
#include "../networks/sequential.hpp"
#include "../traits.hpp"
#include <lorina/aiger.hpp>
#include <iostream>

namespace mockturtle
{
Expand All @@ -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<Ntk>` to
* read the design as the sequential network it is.
*
\verbatim embed:rst

Expand Down Expand Up @@ -82,6 +91,9 @@ class aiger_reader : public lorina::aiger_reader
static_assert( has_create_and_v<Ntk>, "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<Ntk> && has_create_ro_v<Ntk>;

~aiger_reader()
{
uint32_t output_id{ 0 };
Expand All @@ -104,39 +116,48 @@ class aiger_reader : public lorina::aiger_reader
_ntk.create_po( signal );
}

if constexpr ( has_create_ri_v<Ntk> )
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> )
{
_ntk.set_name( signal, std::get<2>( latch ) + "_next" );
}
if constexpr ( has_set_name_v<Ntk> )
{
_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<Ntk> || !has_create_ro_v<Ntk> )
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<uint32_t>( num_inputs );
Expand All @@ -150,13 +171,21 @@ class aiger_reader : public lorina::aiger_reader
signals.push_back( _ntk.create_pi() );
}

if constexpr ( has_create_ro_v<Ntk> )
/* 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() );
}
}
}

Expand All @@ -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<Ntk> && has_create_ro_v<Ntk> )
if constexpr ( has_set_name_v<Ntk> )
{
if constexpr ( has_set_name_v<Ntk> )
{
_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
Expand All @@ -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<Ntk> && has_create_ro_v<Ntk> )
{
(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
Expand Down Expand Up @@ -255,4 +278,4 @@ class aiger_reader : public lorina::aiger_reader
mutable std::vector<std::tuple<unsigned, uint8_t, std::string>> latches;
};

} /* namespace mockturtle */
} /* namespace mockturtle */
104 changes: 104 additions & 0 deletions test/io/aiger_reader.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@

#include <lorina/aiger.hpp>

#include <iostream>
#include <sstream>
#include <string>
#include <utility>
Expand Down Expand Up @@ -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<aig_network> 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_network> 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 );
}
Loading