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

Update simulation_cec.hpp #60

Open
wants to merge 1 commit into
base: v2021-cec
Choose a base branch
from
Open

Update simulation_cec.hpp #60

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
247 changes: 157 additions & 90 deletions include/mockturtle/algorithms/simulation_cec.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,95 +40,162 @@
#include "miter.hpp"
#include "simulation.hpp"

namespace mockturtle
{

/* Statistics to be reported */
struct simulation_cec_stats
{
/*! \brief Split variable (simulation size). */
uint32_t split_var{ 0 };

/*! \brief Number of simulation rounds. */
uint32_t rounds{ 0 };
};

namespace detail
{

template<class Ntk>
class simulation_cec_impl
{
public:
using pattern_t = unordered_node_map<kitty::dynamic_truth_table, Ntk>;
using node = typename Ntk::node;
using signal = typename Ntk::signal;

public:
explicit simulation_cec_impl( Ntk& ntk, simulation_cec_stats& st )
: _ntk( ntk ),
_st( st )
{
}

bool run()
{
/* TODO: write your implementation here */
return false;
}

private:
/* you can add additional methods here */

private:
Ntk& _ntk;
simulation_cec_stats& _st;
/* you can add other attributes here */
};

} // namespace detail

/* Entry point for users to call */

/*! \brief Simulation-based CEC.
*
* This function implements a simulation-based combinational equivalence checker.
* The implementation creates a miter network and run several rounds of simulation
* to verify the functional equivalence. For memory and speed reasons this approach
* is limited up to 40 input networks. It returns an optional which is `nullopt`,
* if the network has more than 40 inputs.
*/
template<class Ntk>
std::optional<bool> simulation_cec( Ntk const& ntk1, Ntk const& ntk2, simulation_cec_stats* pst = nullptr )
{
static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
static_assert( has_num_pis_v<Ntk>, "Ntk does not implement the num_pis method" );
static_assert( has_size_v<Ntk>, "Ntk does not implement the size method" );
static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node method" );
static_assert( has_foreach_pi_v<Ntk>, "Ntk does not implement the foreach_pi method" );
static_assert( has_foreach_po_v<Ntk>, "Ntk does not implement the foreach_po method" );
static_assert( has_foreach_node_v<Ntk>, "Ntk does not implement the foreach_node method" );
static_assert( has_is_complemented_v<Ntk>, "Ntk does not implement the is_complemented method" );

simulation_cec_stats st;

bool result = false;

if ( ntk1.num_pis() > 40 )
return std::nullopt;
namespace mockturtle {

/* Statistics to be reported */
struct simulation_cec_stats {
/*! \brief Split variable (simulation size). */
uint32_t split_var{ 0 };

/*! \brief Number of simulation rounds. */
uint32_t rounds{ 0 };
};

namespace detail {
class part_simulator {
public:
part_simulator() = delete;
part_simulator(uint32_t sp_var, uint32_t r): split_var(sp_var), round(r) {}

//simulate value for a constant value
kitty::dynamic_truth_table compute_constant(bool value) const {
kitty::dynamic_truth_table tt(split_var);
return value ? ~tt : tt;
}


//simulate a primary input based on its index
kitty::dynamic_truth_table compute_pi(uint32_t index) const {
kitty::dynamic_truth_table tt(split_var);
if (index < split_var) { //input within split_vars: simulate as usual
kitty::create_nth_var(tt, index);
}
else { //input outside: essentially the same as simulating a constant value
bool value = ((round >> (index - split_var)) & 1); //determine the value
if (value == 0){
tt = ~tt;
}
}
return tt;

}

//invert a simulate value
kitty::dynamic_truth_table compute_not(kitty::dynamic_truth_table const& value) const {
return ~value;
}

private:
uint32_t split_var;
uint32_t round;
};


template<class Ntk>
class simulation_cec_impl {
public:
using pattern_t = unordered_node_map<kitty::dynamic_truth_table, Ntk>;
using node = typename Ntk::node;
using signal = typename Ntk::signal;

public:
explicit simulation_cec_impl(Ntk& ntk, simulation_cec_stats& st) : _ntk(ntk), _st(st) {}

//function to compute split_var
uint32_t compute_split_var(uint32_t n, uint32_t V) {
if (n <= 6) {
return n;
}
else {
uint32_t m = 7;
while (m <= n && (32 + (1 << (m - 3))) * V <= (1 << 29)) {
m++;
}
return m-1;
}
}

//function to compute rounds
uint32_t compute_round(uint32_t n, uint32_t sp) {
uint32_t rounds = (1 << n - sp);
return rounds;
}


bool run() {
uint32_t n = _ntk.num_pis(); // number of inputs
uint32_t V = _ntk.num_gates(); // number of nodes in the network
uint32_t split_var = compute_split_var(n, V);
uint32_t rounds = compute_round(n, split_var);

// update the attribute
_st.split_var = split_var;
_st.rounds = rounds;

for (uint32_t i = 0; i < rounds; i++) {
part_simulator psim(split_var, i);
const auto tts = simulate<kitty::dynamic_truth_table>(_ntk, psim);
//returns a vector of truth tables: each represent a primary outputs

for (auto &out : tts) {
//is_const0 gives True if words is 0
if (kitty::is_const0(out) == 0) {
return false; //check if each output truth table is 0
}
}
}

return true;
}

private:


private:
Ntk& _ntk;
simulation_cec_stats& _st;
};
} // namespace detail

/* Entry point for users to call */

/*! \brief Simulation-based CEC.
*
* This function implements a simulation-based combinational equivalence checker.
* The implementation creates a miter network and run several rounds of simulation
* to verify the functional equivalence. For memory and speed reasons this approach
* is limited up to 40 input networks. It returns an optional which is `nullopt`,
* if the network has more than 40 inputs.
*/
template<class Ntk>
std::optional<bool> simulation_cec(Ntk const& ntk1, Ntk const& ntk2, simulation_cec_stats* pst = nullptr) {
static_assert(is_network_type_v<Ntk>, "Ntk is not a network type");
static_assert(has_num_pis_v<Ntk>, "Ntk does not implement the num_pis method");
static_assert(has_size_v<Ntk>, "Ntk does not implement the size method");
static_assert(has_get_node_v<Ntk>, "Ntk does not implement the get_node method");
static_assert(has_foreach_pi_v<Ntk>, "Ntk does not implement the foreach_pi method");
static_assert(has_foreach_po_v<Ntk>, "Ntk does not implement the foreach_po method");
static_assert(has_foreach_node_v<Ntk>, "Ntk does not implement the foreach_node method");
static_assert(has_is_complemented_v<Ntk>, "Ntk does not implement the is_complemented method");

simulation_cec_stats st;

bool result = false;

if (ntk1.num_pis() > 40)
return std::nullopt;

auto ntk_miter = miter<Ntk>(ntk1, ntk2);

if (ntk_miter.has_value()) {
detail::simulation_cec_impl p(*ntk_miter, st);
result = p.run();
}

if (pst)
*pst = st;

return result;
}

auto ntk_miter = miter<Ntk>( ntk1, ntk2 );

if ( ntk_miter.has_value() )
{
detail::simulation_cec_impl p( *ntk_miter, st );
result = p.run();
}

if ( pst )
*pst = st;

return result;
}

} // namespace mockturtle