Skip to content
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

V2021 cec #54

Open
wants to merge 3 commits into
base: v2021-cec
Choose a base branch
from
Open

V2021 cec #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0967aac
Menghe JIN, modified project 2 implementations
MysticJ Dec 23, 2021
ea7d348
Update simulation_cec.cpp
MysticJ Dec 23, 2021
4dd4936
Update simulation_cec_rewriting.cpp
MysticJ Dec 23, 2021
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
111 changes: 110 additions & 1 deletion include/mockturtle/algorithms/simulation_cec.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@

#pragma once

#include <math.h>

#include <kitty/constructors.hpp>
#include <kitty/dynamic_truth_table.hpp>
#include <kitty/operations.hpp>
Expand Down Expand Up @@ -74,7 +76,114 @@ class simulation_cec_impl
bool run()
{
/* TODO: write your implementation here */
return false;

// Step 1: update simulation_cec_stats _st :
uint32_t num_nodes = _ntk.size(); // V
uint32_t num_inputs = _ntk.num_pis(); // n

std::cout << "\[simulation cec\] start new run ------------------------" << std::endl;
std::cout << "\[simulation cec\] num_inputs is " << num_inputs << std::endl;

assert( num_inputs <= 40u );

if ( num_inputs <= 6u )
{
_st.split_var = num_inputs;
}
else
{
uint32_t tmp = floor( log2( pow( 2, 29 ) / num_nodes - 32 ) + 3 );

// std::cout << "\[simulation cec\] tmp is " << tmp << std::endl;

_st.split_var = ( num_inputs <= tmp ? num_inputs : tmp );
}
_st.rounds = ( 1u << ( num_inputs - _st.split_var ) );

// For test only
// _st.split_var = 7u;
// _st.rounds = ( 1u << ( num_inputs - _st.split_var ) );

std::cout << "\[simulation cec\] split_var is " << _st.split_var << std::endl;
std::cout << "\[simulation cec\] rounds is " << _st.rounds << std::endl;

// Step 2: initialize patters (pattern_t), simulator :
pattern_t patterns( _ntk );
default_simulator<kitty::dynamic_truth_table> sim( num_inputs );
bool result = true;

// Step 3: iterate
if ( _st.rounds == 1u )
{
patterns.reset();
simulate_nodes<kitty::dynamic_truth_table>( _ntk, patterns, sim );
_ntk.foreach_po( [&]( signal const& f, uint32_t j )
{
std::vector<uint64_t> tt_bits = ( _ntk.is_complemented( f ) ? ~patterns[f] : patterns[f] )._bits;
// std::cout << "\t\t j = " << j << "; size of tt = " << tt_bits.size() << std::endl;

for ( std::vector<uint64_t>::iterator it = tt_bits.begin(); it != tt_bits.end(); ++it )
{
// std::cout << "\[simulation cec\] result is " << *it << std::endl;
if ( *it != 0x0 )
{
result = result && false;
std::cout << "\[simulation cec\] inconsistency detected." << std::endl;
}
}
} );
}
else
{
for ( uint32_t round = 0u; round < _st.rounds; round = round + 1u )
{
std::cout << "\[simulation cec\] round-1 is " << round << std::endl;

patterns.reset();

uint32_t split_var = _st.split_var;

_ntk.foreach_pi( [&]( node const& n, uint32_t i )
{
if ( i >= split_var )
{
uint32_t index = i - split_var;
// std::cout << "\[simulation cec\] - update_patterns, index is " << index << std::endl;

std::cout << "\[simulation cec\] - update_patterns, update to " << (( round >> index ) % 2u) << std::endl;
if ( ( round >> index ) % 2u )
{ // if this input should be set as 1:
patterns[n] = ~kitty::dynamic_truth_table( _ntk.num_pis() );
}
else
{ // if this input should be set as 0:
patterns[n] = kitty::dynamic_truth_table( _ntk.num_pis() );
}
}
} );
std::cout << "\[simulation cec\] end of update_patterns" << std::endl;

simulate_nodes<kitty::dynamic_truth_table>( _ntk, patterns, sim );

_ntk.foreach_po( [&]( signal const& f, uint32_t j )
{
std::vector<uint64_t> tt_bits = ( _ntk.is_complemented( f ) ? ~patterns[f] : patterns[f] )._bits;
for ( std::vector<uint64_t>::iterator it = tt_bits.begin(); it != tt_bits.end(); ++it )
{
if ( *it != 0x0 )
{
result = result && false;
std::cout << "\[simulation cec\] inconsistency detected." << std::endl;
}
}
} );
if ( !result )
{
return result;
}
}
}
return result;
}

private:
Expand Down
26 changes: 25 additions & 1 deletion test/algorithms/simulation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,9 @@ TEST_CASE( "Simulate XOR AIG circuit with pre-defined values", "[simulation]" )

unordered_node_map<kitty::dynamic_truth_table, aig_network> node_to_value( aig );
simulate_nodes<kitty::dynamic_truth_table>( aig, node_to_value, sim );

CHECK( ( aig.is_complemented( f1 ) ? ~node_to_value[f1] : node_to_value[f1] )._bits[0] == 0x7 );
CHECK( ( aig.is_complemented( f2 ) ? ~node_to_value[f2] : node_to_value[f2] )._bits[0] == 0xd );
CHECK( ( aig.is_complemented( f3 ) ? ~node_to_value[f3] : node_to_value[f3] )._bits[0] == 0xb );
CHECK( ( aig.is_complemented( f4 ) ? ~node_to_value[f4] : node_to_value[f4] )._bits[0] == 0x6 );

node_to_value.reset();
Expand All @@ -90,6 +92,28 @@ TEST_CASE( "Simulate XOR AIG circuit with pre-defined values", "[simulation]" )
CHECK( ( aig.is_complemented( f2 ) ? ~node_to_value[f2] : node_to_value[f2] )._bits[0] == 0x5 );
CHECK( ( aig.is_complemented( f3 ) ? ~node_to_value[f3] : node_to_value[f3] )._bits[0] == 0x3 );
CHECK( ( aig.is_complemented( f4 ) ? ~node_to_value[f4] : node_to_value[f4] )._bits[0] == 0xe );

node_to_value.reset();

/* set node a to false, such that function f1 becomes true */
node_to_value[aig.get_node( a )] = ~kitty::dynamic_truth_table( 2 );
/* re-simulated with the fixed value for f1 */
simulate_nodes<kitty::dynamic_truth_table>( aig, node_to_value, sim );
CHECK( ( aig.is_complemented( f1 ) ? ~node_to_value[f1] : node_to_value[f1] )._bits[0] == 0x3 );
CHECK( ( aig.is_complemented( f2 ) ? ~node_to_value[f2] : node_to_value[f2] )._bits[0] == 0xc );
CHECK( ( aig.is_complemented( f3 ) ? ~node_to_value[f3] : node_to_value[f3] )._bits[0] == 0xf );
CHECK( ( aig.is_complemented( f4 ) ? ~node_to_value[f4] : node_to_value[f4] )._bits[0] == 0x3 );

node_to_value.reset();

/* set node a to false, such that function f1 becomes true */
node_to_value[aig.get_node( b )] = ~kitty::dynamic_truth_table( 2 );
/* re-simulated with the fixed value for f1 */
simulate_nodes<kitty::dynamic_truth_table>( aig, node_to_value, sim );
CHECK( ( aig.is_complemented( f1 ) ? ~node_to_value[f1] : node_to_value[f1] )._bits[0] == 0x5 );
CHECK( ( aig.is_complemented( f2 ) ? ~node_to_value[f2] : node_to_value[f2] )._bits[0] == 0xf );
CHECK( ( aig.is_complemented( f3 ) ? ~node_to_value[f3] : node_to_value[f3] )._bits[0] == 0xa );
CHECK( ( aig.is_complemented( f4 ) ? ~node_to_value[f4] : node_to_value[f4] )._bits[0] == 0x5 );
}

TEST_CASE( "Partial simulator", "[simulation]" )
Expand Down
39 changes: 22 additions & 17 deletions test/algorithms/simulation_cec.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ TEST_CASE( "CEC simple AIG", "[cec]" )
CHECK( st.rounds == 1 );
}


TEST_CASE( "CEC different #PIs", "[cec]" )
{
xag_network xag1;
Expand Down Expand Up @@ -127,6 +128,26 @@ TEST_CASE( "CEC different AIGs", "[cec]" )
CHECK( st.rounds == 1 );
}

TEST_CASE( "CEC on optimized design 2", "[cec]" )
{
xag_network xag1;

auto const result = lorina::read_aiger( fmt::format( "{}/int2float.aig", BENCHMARKS_PATH ), aiger_reader( xag1 ) );
CHECK( result == lorina::return_code::success );

xag_npn_resynthesis<xag_network> resyn;

exact_library<xag_network, xag_npn_resynthesis<xag_network>> lib( resyn );

xag_network xag2 = map( xag1, lib );

simulation_cec_stats st;
CHECK( *simulation_cec( xag1, xag2, &st ) );
CHECK( st.split_var == 11 );
CHECK( st.rounds == 1 );
}

/*
TEST_CASE( "CEC on optimized design 1", "[cec]" )
{
mig_network mig1;
Expand Down Expand Up @@ -170,22 +191,6 @@ TEST_CASE( "CEC on badly optimized design 1", "[cec]" )
CHECK( st.split_var == 18 );
CHECK( st.rounds == 64 );
}
*/

TEST_CASE( "CEC on optimized design 2", "[cec]" )
{
xag_network xag1;

auto const result = lorina::read_aiger( fmt::format( "{}/int2float.aig", BENCHMARKS_PATH ), aiger_reader( xag1 ) );
CHECK( result == lorina::return_code::success );

xag_npn_resynthesis<xag_network> resyn;

exact_library<xag_network, xag_npn_resynthesis<xag_network>> lib( resyn );

xag_network xag2 = map( xag1, lib );

simulation_cec_stats st;
CHECK( *simulation_cec( xag1, xag2, &st ) );
CHECK( st.split_var == 11 );
CHECK( st.rounds == 1 );
}
Loading