version 2 - logic synthesis commands
parent
6f3be84299
commit
78bda87307
|
@ -0,0 +1,76 @@
|
||||||
|
/* phyLS: powerful heightened yielded Logic Synthesis
|
||||||
|
* Copyright (C) 2022 */
|
||||||
|
|
||||||
|
/**
|
||||||
|
* @file aig_balancing.hpp
|
||||||
|
*
|
||||||
|
* @brief transforms the current network into a well-balanced AIG
|
||||||
|
*
|
||||||
|
* @author Homyoung
|
||||||
|
* @since 2022/12/14
|
||||||
|
*/
|
||||||
|
|
||||||
|
#ifndef BALANCE_HPP
|
||||||
|
#define BALANCE_HPP
|
||||||
|
|
||||||
|
#include <algorithm>
|
||||||
|
#include <mockturtle/algorithms/aig_balancing.hpp>
|
||||||
|
#include <mockturtle/networks/aig.hpp>
|
||||||
|
#include <mockturtle/views/depth_view.hpp>
|
||||||
|
#include <vector>
|
||||||
|
|
||||||
|
#include "../core/misc.hpp"
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
|
||||||
|
namespace alice {
|
||||||
|
|
||||||
|
class balance_command : public command {
|
||||||
|
public:
|
||||||
|
explicit balance_command(const environment::ptr& env)
|
||||||
|
: command(env,
|
||||||
|
"transforms the current network into a well-balanced AIG") {
|
||||||
|
add_flag("--strash, -s", "Balance AND finding structural hashing");
|
||||||
|
add_flag("--verbose, -v", "print the information");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() {
|
||||||
|
clock_t begin, end;
|
||||||
|
double totalTime;
|
||||||
|
|
||||||
|
if (store<aig_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty AIG network\n";
|
||||||
|
else {
|
||||||
|
auto aig = store<aig_network>().current();
|
||||||
|
if (is_set("strash")) {
|
||||||
|
begin = clock();
|
||||||
|
aig_balancing_params ps;
|
||||||
|
ps.minimize_levels = false;
|
||||||
|
aig_balance(aig, ps);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
} else {
|
||||||
|
begin = clock();
|
||||||
|
aig_balance(aig);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
}
|
||||||
|
phyLS::print_stats(aig);
|
||||||
|
|
||||||
|
store<aig_network>().extend();
|
||||||
|
store<aig_network>().current() = aig;
|
||||||
|
}
|
||||||
|
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
private:
|
||||||
|
};
|
||||||
|
|
||||||
|
ALICE_ADD_COMMAND(balance, "Logic synthesis")
|
||||||
|
|
||||||
|
} // namespace alice
|
||||||
|
|
||||||
|
#endif
|
|
@ -15,70 +15,62 @@
|
||||||
|
|
||||||
#include "../store.hpp"
|
#include "../store.hpp"
|
||||||
|
|
||||||
namespace alice
|
using namespace std;
|
||||||
{
|
|
||||||
|
|
||||||
class exprsim_command: public command
|
namespace alice {
|
||||||
{
|
|
||||||
public:
|
|
||||||
explicit exprsim_command( const environment::ptr& env )
|
|
||||||
: command( env, "expression simulation, return a truth table" )
|
|
||||||
{
|
|
||||||
add_flag( "--verbose, -v", "print the information" );
|
|
||||||
add_option( "-e,--expression", expression, "creates truth table from expression" );
|
|
||||||
add_flag( "-n,--new", "adds new store entry" );
|
|
||||||
add_option( "-m,--max_num_vars", max_num_vars, "set the maximum number of variables" );
|
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
class exprsim_command : public command {
|
||||||
void execute()
|
public:
|
||||||
{
|
explicit exprsim_command(const environment::ptr& env)
|
||||||
auto& opt_ntks = store<optimum_network>();
|
: command(env, "expression simulation, return a truth table") {
|
||||||
|
add_flag("--verbose, -v", "print the information");
|
||||||
if ( opt_ntks.empty() || is_set( "new" ) )
|
add_option("-e,--expression", expression,
|
||||||
{
|
"creates truth table from expression");
|
||||||
opt_ntks.extend();
|
add_flag("-n,--new", "adds new store entry");
|
||||||
}
|
add_option("-m,--max_num_vars", max_num_vars,
|
||||||
|
"set the maximum number of variables");
|
||||||
|
}
|
||||||
|
|
||||||
/* find max var */
|
protected:
|
||||||
uint32_t num_vars{0u};
|
void execute() {
|
||||||
|
clock_t begin, end;
|
||||||
for (auto c : expression)
|
double totalTime;
|
||||||
{
|
auto& opt_ntks = store<optimum_network>();
|
||||||
if (c >= 'a' && c <= 'p')
|
begin = clock();
|
||||||
{
|
if (opt_ntks.empty() || is_set("new")) opt_ntks.extend();
|
||||||
num_vars = std::max<uint32_t>( num_vars, c - 'a' + 1u );
|
/* find max var */
|
||||||
}
|
uint32_t num_vars{0u};
|
||||||
}
|
for (auto c : expression) {
|
||||||
|
if (c >= 'a' && c <= 'p')
|
||||||
|
num_vars = std::max<uint32_t>(num_vars, c - 'a' + 1u);
|
||||||
|
}
|
||||||
|
if (is_set("max_num_vars"))
|
||||||
|
num_vars = max_num_vars > num_vars ? max_num_vars : num_vars;
|
||||||
|
kitty::dynamic_truth_table tt(num_vars);
|
||||||
|
if (kitty::create_from_expression(tt, expression)) {
|
||||||
|
optimum_network opt;
|
||||||
|
opt.function = tt;
|
||||||
|
opt.network = expression;
|
||||||
|
opt_ntks.current() = opt;
|
||||||
|
std::cout << fmt::format("tt: 0x{}", kitty::to_hex(opt.function))
|
||||||
|
<< std::endl;
|
||||||
|
|
||||||
if( is_set( "max_num_vars" ) )
|
store<optimum_network>().extend();
|
||||||
{
|
store<optimum_network>().current() = opt;
|
||||||
num_vars = max_num_vars > num_vars ? max_num_vars : num_vars;
|
}
|
||||||
}
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
|
||||||
kitty::dynamic_truth_table tt( num_vars );
|
private:
|
||||||
|
std::string expression = "";
|
||||||
|
uint32_t max_num_vars = 0u;
|
||||||
|
};
|
||||||
|
|
||||||
if ( kitty::create_from_expression( tt, expression ) )
|
ALICE_ADD_COMMAND(exprsim, "I/O")
|
||||||
{
|
|
||||||
optimum_network opt;
|
|
||||||
opt.function = tt;
|
|
||||||
opt.network = expression;
|
|
||||||
opt_ntks.current() = opt;
|
|
||||||
std::cout << fmt::format( "tt: 0x{}", kitty::to_hex( opt.function ) ) << std::endl;
|
|
||||||
|
|
||||||
store<optimum_network>().extend();
|
} // namespace alice
|
||||||
store<optimum_network>().current() = opt;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
std::string expression = "";
|
|
||||||
uint32_t max_num_vars = 0u;
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
ALICE_ADD_COMMAND( exprsim, "I/O" )
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -37,79 +37,67 @@
|
||||||
|
|
||||||
#include "../store.hpp"
|
#include "../store.hpp"
|
||||||
|
|
||||||
namespace alice
|
namespace alice {
|
||||||
{
|
|
||||||
|
|
||||||
void add_optimum_network_entry(command &cmd, kitty::dynamic_truth_table &function)
|
void add_optimum_network_entry(command &cmd,
|
||||||
{
|
kitty::dynamic_truth_table &function) {
|
||||||
if (cmd.env->variable("npn") != "")
|
if (cmd.env->variable("npn") != "") {
|
||||||
{
|
function = std::get<0>(kitty::exact_npn_canonization(function));
|
||||||
function = std::get<0>(kitty::exact_npn_canonization(function));
|
|
||||||
}
|
|
||||||
|
|
||||||
optimum_network entry(function);
|
|
||||||
|
|
||||||
if (!entry.exists())
|
|
||||||
{
|
|
||||||
cmd.store<optimum_network>().extend();
|
|
||||||
cmd.store<optimum_network>().current() = entry;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
class load_command : public command
|
optimum_network entry(function);
|
||||||
{
|
|
||||||
public:
|
|
||||||
load_command(const environment::ptr &env) : command(env, "Load new entry")
|
|
||||||
{
|
|
||||||
add_option("truth_table,--tt", truth_table, "truth table in hex format");
|
|
||||||
add_flag("--binary,-b", "read truth table as binary string");
|
|
||||||
add_option("--majn,-m", odd_inputs, "generate majority-of-n truth table ");
|
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
|
||||||
void execute() override
|
|
||||||
{
|
|
||||||
auto function = [this]()
|
|
||||||
{
|
|
||||||
if (is_set("binary"))
|
|
||||||
{
|
|
||||||
const unsigned num_vars = ::log(truth_table.size()) / ::log(2.0);
|
|
||||||
kitty::dynamic_truth_table function(num_vars);
|
|
||||||
kitty::create_from_binary_string(function, truth_table);
|
|
||||||
return function;
|
|
||||||
}
|
|
||||||
else if (is_set("majn"))
|
|
||||||
{
|
|
||||||
if (!(odd_inputs & 1))
|
|
||||||
{
|
|
||||||
std::cout << " majority-of-n, n must be an odd number\n ";
|
|
||||||
assert(false);
|
|
||||||
}
|
|
||||||
|
|
||||||
kitty::dynamic_truth_table maj(odd_inputs);
|
|
||||||
kitty::create_majority(maj);
|
|
||||||
std::cout << " MAJ" << odd_inputs << " : " << kitty::to_hex(maj) << std::endl;
|
|
||||||
return maj;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
const unsigned num_vars = ::log(truth_table.size() * 4) / ::log(2.0);
|
|
||||||
kitty::dynamic_truth_table function(num_vars);
|
|
||||||
kitty::create_from_hex_string(function, truth_table);
|
|
||||||
return function;
|
|
||||||
}
|
|
||||||
}();
|
|
||||||
|
|
||||||
add_optimum_network_entry(*this, function);
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
std::string truth_table;
|
|
||||||
unsigned odd_inputs;
|
|
||||||
};
|
|
||||||
|
|
||||||
ALICE_ADD_COMMAND(load, "I/O");
|
|
||||||
|
|
||||||
|
if (!entry.exists()) {
|
||||||
|
cmd.store<optimum_network>().extend();
|
||||||
|
cmd.store<optimum_network>().current() = entry;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
class load_command : public command {
|
||||||
|
public:
|
||||||
|
load_command(const environment::ptr &env) : command(env, "Load new entry") {
|
||||||
|
add_option("truth_table,--tt", truth_table, "truth table in hex format");
|
||||||
|
add_flag("--binary,-b", "read truth table as binary string");
|
||||||
|
add_option("--majn,-m", odd_inputs, "generate majority-of-n truth table ");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() override {
|
||||||
|
auto function = [this]() {
|
||||||
|
if (is_set("binary")) {
|
||||||
|
const unsigned num_vars = ::log(truth_table.size()) / ::log(2.0);
|
||||||
|
kitty::dynamic_truth_table function(num_vars);
|
||||||
|
kitty::create_from_binary_string(function, truth_table);
|
||||||
|
return function;
|
||||||
|
} else if (is_set("majn")) {
|
||||||
|
if (!(odd_inputs & 1)) {
|
||||||
|
std::cout << " majority-of-n, n must be an odd number\n ";
|
||||||
|
assert(false);
|
||||||
|
}
|
||||||
|
|
||||||
|
kitty::dynamic_truth_table maj(odd_inputs);
|
||||||
|
kitty::create_majority(maj);
|
||||||
|
std::cout << " MAJ" << odd_inputs << " : " << kitty::to_hex(maj)
|
||||||
|
<< std::endl;
|
||||||
|
return maj;
|
||||||
|
} else {
|
||||||
|
const unsigned num_vars = ::log(truth_table.size() * 4) / ::log(2.0);
|
||||||
|
kitty::dynamic_truth_table function(num_vars);
|
||||||
|
kitty::create_from_hex_string(function, truth_table);
|
||||||
|
return function;
|
||||||
|
}
|
||||||
|
}();
|
||||||
|
|
||||||
|
add_optimum_network_entry(*this, function);
|
||||||
|
}
|
||||||
|
|
||||||
|
private:
|
||||||
|
std::string truth_table;
|
||||||
|
unsigned odd_inputs;
|
||||||
|
};
|
||||||
|
|
||||||
|
ALICE_ADD_COMMAND(load, "I/O");
|
||||||
|
|
||||||
|
} // namespace alice
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -13,95 +13,107 @@
|
||||||
#ifndef LUT_MAPPING_HPP
|
#ifndef LUT_MAPPING_HPP
|
||||||
#define LUT_MAPPING_HPP
|
#define LUT_MAPPING_HPP
|
||||||
|
|
||||||
#include <mockturtle/mockturtle.hpp>
|
#include <mockturtle/algorithms/collapse_mapped.hpp>
|
||||||
|
#include <mockturtle/algorithms/lut_mapping.hpp>
|
||||||
#include <mockturtle/algorithms/satlut_mapping.hpp>
|
#include <mockturtle/algorithms/satlut_mapping.hpp>
|
||||||
|
#include <mockturtle/generators/arithmetic.hpp>
|
||||||
|
#include <mockturtle/networks/aig.hpp>
|
||||||
|
#include <mockturtle/networks/klut.hpp>
|
||||||
|
#include <mockturtle/networks/sequential.hpp>
|
||||||
|
#include <mockturtle/traits.hpp>
|
||||||
|
#include <mockturtle/views/mapping_view.hpp>
|
||||||
|
|
||||||
namespace alice
|
using namespace mockturtle;
|
||||||
{
|
using namespace std;
|
||||||
|
|
||||||
class lut_mapping_command : public command
|
namespace alice {
|
||||||
{
|
|
||||||
public:
|
|
||||||
explicit lut_mapping_command(const environment::ptr &env) : command(env, "LUT mapping : using AIG as default")
|
|
||||||
{
|
|
||||||
add_option("cut_size, -k", cut_size, "set the cut size from 2 to 8, default = 4");
|
|
||||||
add_flag("--verbose, -v", "print the information");
|
|
||||||
add_flag("--satlut, -s", "satlut mapping");
|
|
||||||
add_flag("--xag, -g", "LUT mapping for XAG");
|
|
||||||
add_flag("--mig, -m", "LUT mapping for MIG");
|
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
class lut_mapping_command : public command {
|
||||||
void execute()
|
public:
|
||||||
{
|
explicit lut_mapping_command(const environment::ptr &env)
|
||||||
lut_mapping_params ps;
|
: command(env, "LUT mapping : using AIG as default") {
|
||||||
|
add_option("cut_size, -k", cut_size,
|
||||||
|
"set the cut size from 2 to 8, default = 4");
|
||||||
|
add_flag("--verbose, -v", "print the information");
|
||||||
|
add_flag("--satlut, -s", "satlut mapping");
|
||||||
|
add_flag("--xag, -g", "LUT mapping for XAG");
|
||||||
|
add_flag("--mig, -m", "LUT mapping for MIG");
|
||||||
|
}
|
||||||
|
|
||||||
if (is_set("mig"))
|
protected:
|
||||||
{
|
void execute() {
|
||||||
/* derive some MIG */
|
clock_t begin, end;
|
||||||
assert(store<mig_network>().size() > 0);
|
double totalTime;
|
||||||
mig_network mig = store<mig_network>().current();
|
lut_mapping_params ps;
|
||||||
|
|
||||||
mapping_view<mig_network, true> mapped_mig{mig};
|
if (is_set("mig")) {
|
||||||
|
/* derive some MIG */
|
||||||
|
assert(store<mig_network>().size() > 0);
|
||||||
|
begin = clock();
|
||||||
|
mig_network mig = store<mig_network>().current();
|
||||||
|
|
||||||
|
mapping_view<mig_network, true> mapped_mig{mig};
|
||||||
|
ps.cut_enumeration_ps.cut_size = cut_size;
|
||||||
|
lut_mapping<mapping_view<mig_network, true>, true>(mapped_mig, ps);
|
||||||
|
|
||||||
|
/* collapse into k-LUT network */
|
||||||
|
const auto klut = *collapse_mapped_network<klut_network>(mapped_mig);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
store<klut_network>().extend();
|
||||||
|
store<klut_network>().current() = klut;
|
||||||
|
} else if (is_set("xag")) {
|
||||||
|
/* derive some XAG */
|
||||||
|
assert(store<xag_network>().size() > 0);
|
||||||
|
begin = clock();
|
||||||
|
xag_network xag = store<xag_network>().current();
|
||||||
|
|
||||||
|
mapping_view<xag_network, true> mapped_xag{xag};
|
||||||
|
ps.cut_enumeration_ps.cut_size = cut_size;
|
||||||
|
lut_mapping<mapping_view<xag_network, true>, true>(mapped_xag, ps);
|
||||||
|
|
||||||
|
/* collapse into k-LUT network */
|
||||||
|
const auto klut = *collapse_mapped_network<klut_network>(mapped_xag);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
store<klut_network>().extend();
|
||||||
|
store<klut_network>().current() = klut;
|
||||||
|
} else {
|
||||||
|
if (store<aig_network>().size() == 0) {
|
||||||
|
assert(false && "Error: Empty AIG network\n");
|
||||||
|
}
|
||||||
|
/* derive some AIG */
|
||||||
|
aig_network aig = store<aig_network>().current();
|
||||||
|
begin = clock();
|
||||||
|
mapping_view<aig_network, true> mapped_aig{aig};
|
||||||
|
|
||||||
|
/* LUT mapping */
|
||||||
|
if (is_set("satlut")) {
|
||||||
|
satlut_mapping_params ps;
|
||||||
ps.cut_enumeration_ps.cut_size = cut_size;
|
ps.cut_enumeration_ps.cut_size = cut_size;
|
||||||
lut_mapping<mapping_view<mig_network, true>, true>(mapped_mig, ps);
|
satlut_mapping<mapping_view<aig_network, true>, true>(mapped_aig, ps);
|
||||||
|
} else {
|
||||||
/* collapse into k-LUT network */
|
|
||||||
const auto klut = *collapse_mapped_network<klut_network>(mapped_mig);
|
|
||||||
store<klut_network>().extend();
|
|
||||||
store<klut_network>().current() = klut;
|
|
||||||
}
|
|
||||||
else if (is_set("xag"))
|
|
||||||
{
|
|
||||||
/* derive some XAG */
|
|
||||||
assert(store<xag_network>().size() > 0);
|
|
||||||
xag_network xag = store<xag_network>().current();
|
|
||||||
|
|
||||||
mapping_view<xag_network, true> mapped_xag{xag};
|
|
||||||
ps.cut_enumeration_ps.cut_size = cut_size;
|
ps.cut_enumeration_ps.cut_size = cut_size;
|
||||||
lut_mapping<mapping_view<xag_network, true>, true>(mapped_xag, ps);
|
lut_mapping<mapping_view<aig_network, true>, true,
|
||||||
|
cut_enumeration_mf_cut>(mapped_aig, ps);
|
||||||
/* collapse into k-LUT network */
|
|
||||||
const auto klut = *collapse_mapped_network<klut_network>(mapped_xag);
|
|
||||||
store<klut_network>().extend();
|
|
||||||
store<klut_network>().current() = klut;
|
|
||||||
}
|
}
|
||||||
else
|
|
||||||
{
|
|
||||||
if (store<aig_network>().size() == 0)
|
|
||||||
{
|
|
||||||
assert(false && "no AIG in the store");
|
|
||||||
}
|
|
||||||
/* derive some AIG */
|
|
||||||
aig_network aig = store<aig_network>().current();
|
|
||||||
|
|
||||||
mapping_view<aig_network, true> mapped_aig{aig};
|
/* collapse into k-LUT network */
|
||||||
|
const auto klut = *collapse_mapped_network<klut_network>(mapped_aig);
|
||||||
/* LUT mapping */
|
end = clock();
|
||||||
if (is_set("satlut"))
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
{
|
store<klut_network>().extend();
|
||||||
satlut_mapping_params ps;
|
store<klut_network>().current() = klut;
|
||||||
ps.cut_enumeration_ps.cut_size = cut_size;
|
|
||||||
satlut_mapping<mapping_view<aig_network, true>, true>(mapped_aig, ps);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
ps.cut_enumeration_ps.cut_size = cut_size;
|
|
||||||
lut_mapping<mapping_view<aig_network, true>, true, cut_enumeration_mf_cut>(mapped_aig, ps);
|
|
||||||
}
|
|
||||||
|
|
||||||
/* collapse into k-LUT network */
|
|
||||||
const auto klut = *collapse_mapped_network<klut_network>(mapped_aig);
|
|
||||||
store<klut_network>().extend();
|
|
||||||
store<klut_network>().current() = klut;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
unsigned cut_size = 4u;
|
unsigned cut_size = 4u;
|
||||||
};
|
};
|
||||||
|
|
||||||
ALICE_ADD_COMMAND(lut_mapping, "Mapping")
|
ALICE_ADD_COMMAND(lut_mapping, "Mapping")
|
||||||
}
|
} // namespace alice
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -0,0 +1,113 @@
|
||||||
|
/* phyLS: powerful heightened yielded Logic Synthesis
|
||||||
|
* Copyright (C) 2022 */
|
||||||
|
|
||||||
|
/**
|
||||||
|
* @file node_resynthesis.hpp
|
||||||
|
*
|
||||||
|
* @brief Node resynthesis
|
||||||
|
*
|
||||||
|
* @author Homyoung
|
||||||
|
* @since 2022/12/14
|
||||||
|
*/
|
||||||
|
|
||||||
|
#ifndef NODE_RESYNTHESIS_HPP
|
||||||
|
#define NODE_RESYNTHESIS_HPP
|
||||||
|
|
||||||
|
#include <time.h>
|
||||||
|
|
||||||
|
#include <algorithm>
|
||||||
|
#include <kitty/constructors.hpp>
|
||||||
|
#include <kitty/dynamic_truth_table.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/akers.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/direct.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/mig_npn.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/xmg_npn.hpp>
|
||||||
|
#include <mockturtle/algorithms/simulation.hpp>
|
||||||
|
#include <mockturtle/networks/aig.hpp>
|
||||||
|
#include <mockturtle/networks/klut.hpp>
|
||||||
|
#include <mockturtle/networks/mig.hpp>
|
||||||
|
#include <mockturtle/networks/xag.hpp>
|
||||||
|
#include <mockturtle/networks/xmg.hpp>
|
||||||
|
|
||||||
|
#include "../core/misc.hpp"
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
using namespace mockturtle;
|
||||||
|
|
||||||
|
namespace alice {
|
||||||
|
class resyn_command : public command {
|
||||||
|
public:
|
||||||
|
explicit resyn_command(const environment::ptr& env)
|
||||||
|
: command(env,
|
||||||
|
"performs technology-independent restructuring : using MIG as default") {
|
||||||
|
add_flag("--xmg, -x", "Resubstitution for XMG");
|
||||||
|
add_flag("--xag, -g", "Resubstitution for XAG");
|
||||||
|
add_flag("--direct, -d", "Node resynthesis with direct synthesis");
|
||||||
|
add_flag("--verbose, -v", "print the information");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() {
|
||||||
|
clock_t begin, end;
|
||||||
|
double totalTime;
|
||||||
|
if (store<klut_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty k-LUT network\n";
|
||||||
|
else {
|
||||||
|
auto klut = store<klut_network>().current();
|
||||||
|
if (is_set("xmg")) {
|
||||||
|
begin = clock();
|
||||||
|
if (is_set("direct")) {
|
||||||
|
direct_resynthesis<xmg_network> xmg_resyn;
|
||||||
|
const auto xmg = node_resynthesis<xmg_network>(klut, xmg_resyn);
|
||||||
|
store<xmg_network>().extend();
|
||||||
|
store<xmg_network>().current() = cleanup_dangling(xmg);
|
||||||
|
phyLS::print_stats(xmg);
|
||||||
|
} else {
|
||||||
|
xmg_npn_resynthesis resyn;
|
||||||
|
const auto xmg = node_resynthesis<xmg_network>(klut, resyn);
|
||||||
|
store<xmg_network>().extend();
|
||||||
|
store<xmg_network>().current() = cleanup_dangling(xmg);
|
||||||
|
phyLS::print_stats(xmg);
|
||||||
|
}
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
} else if (is_set("xag")) {
|
||||||
|
begin = clock();
|
||||||
|
direct_resynthesis<xag_network> xag_resyn;
|
||||||
|
const auto xag = node_resynthesis<xag_network>(klut, xag_resyn);
|
||||||
|
store<xag_network>().extend();
|
||||||
|
store<xag_network>().current() = cleanup_dangling(xag);
|
||||||
|
phyLS::print_stats(xag);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
} else {
|
||||||
|
begin = clock();
|
||||||
|
if (is_set("direct")) {
|
||||||
|
direct_resynthesis<mig_network> mig_resyn;
|
||||||
|
const auto mig = node_resynthesis<mig_network>(klut, mig_resyn);
|
||||||
|
store<mig_network>().extend();
|
||||||
|
store<mig_network>().current() = cleanup_dangling(mig);
|
||||||
|
phyLS::print_stats(mig);
|
||||||
|
} else {
|
||||||
|
mig_npn_resynthesis resyn;
|
||||||
|
const auto mig = node_resynthesis<mig_network>(klut, resyn);
|
||||||
|
store<mig_network>().extend();
|
||||||
|
store<mig_network>().current() = cleanup_dangling(mig);
|
||||||
|
phyLS::print_stats(mig);
|
||||||
|
}
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
}
|
||||||
|
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(3) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
ALICE_ADD_COMMAND(resyn, "Logic synthesis")
|
||||||
|
|
||||||
|
} // namespace alice
|
||||||
|
|
||||||
|
#endif
|
|
@ -0,0 +1,113 @@
|
||||||
|
/* phyLS: powerful heightened yielded Logic Synthesis
|
||||||
|
* Copyright (C) 2022 */
|
||||||
|
|
||||||
|
/**
|
||||||
|
* @file aig_balancing.hpp
|
||||||
|
*
|
||||||
|
* @brief performs technology-independent refactoring
|
||||||
|
*
|
||||||
|
* @author Homyoung
|
||||||
|
* @since 2022/12/14
|
||||||
|
*/
|
||||||
|
|
||||||
|
#ifndef REFACTOR_HPP
|
||||||
|
#define REFACTOR_HPP
|
||||||
|
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/akers.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/bidecomposition.hpp>
|
||||||
|
#include <mockturtle/algorithms/node_resynthesis/mig_npn.hpp>
|
||||||
|
#include <mockturtle/algorithms/refactoring.hpp>
|
||||||
|
#include <mockturtle/networks/mig.hpp>
|
||||||
|
#include <mockturtle/networks/xag.hpp>
|
||||||
|
#include <mockturtle/traits.hpp>
|
||||||
|
|
||||||
|
#include "../core/misc.hpp"
|
||||||
|
|
||||||
|
using namespace mockturtle;
|
||||||
|
using namespace std;
|
||||||
|
|
||||||
|
namespace alice {
|
||||||
|
|
||||||
|
class refactor_command : public command {
|
||||||
|
public:
|
||||||
|
explicit refactor_command(const environment::ptr& env)
|
||||||
|
: command(env, "performs technology-independent refactoring") {
|
||||||
|
add_flag("--mig, -m", "refactoring for MIG");
|
||||||
|
add_flag("--xag, -g", "refactoring for XAG");
|
||||||
|
add_flag("--xmg, -x", "refactoring for XMG");
|
||||||
|
add_flag("--akers, -a", "Refactoring with Akers synthesis for MIG");
|
||||||
|
add_flag("--verbose, -v", "print the information");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() {
|
||||||
|
clock_t begin, end;
|
||||||
|
double totalTime;
|
||||||
|
|
||||||
|
if (is_set("mig")) {
|
||||||
|
if (store<mig_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty MIG network\n";
|
||||||
|
else {
|
||||||
|
auto mig = store<mig_network>().current();
|
||||||
|
if (is_set("akers")) {
|
||||||
|
akers_resynthesis<mig_network> resyn;
|
||||||
|
refactoring(mig, resyn);
|
||||||
|
} else {
|
||||||
|
mig_npn_resynthesis resyn;
|
||||||
|
refactoring(mig, resyn);
|
||||||
|
}
|
||||||
|
mig = cleanup_dangling(mig);
|
||||||
|
phyLS::print_stats(mig);
|
||||||
|
store<mig_network>().extend();
|
||||||
|
store<mig_network>().current() = mig;
|
||||||
|
}
|
||||||
|
} else if (is_set("xag")) {
|
||||||
|
if (store<xag_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty XAG network\n";
|
||||||
|
else {
|
||||||
|
auto xag = store<xag_network>().current();
|
||||||
|
bidecomposition_resynthesis<xag_network> resyn;
|
||||||
|
refactoring(xag, resyn);
|
||||||
|
xag = cleanup_dangling(xag);
|
||||||
|
phyLS::print_stats(xag);
|
||||||
|
store<xag_network>().extend();
|
||||||
|
store<xag_network>().current() = xag;
|
||||||
|
}
|
||||||
|
} else if (is_set("xmg")) {
|
||||||
|
if (store<xmg_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty XMG network\n";
|
||||||
|
else {
|
||||||
|
auto xmg = store<xmg_network>().current();
|
||||||
|
xmg_npn_resynthesis resyn;
|
||||||
|
refactoring(xmg, resyn);
|
||||||
|
xmg = cleanup_dangling(xmg);
|
||||||
|
phyLS::print_stats(xmg);
|
||||||
|
store<xmg_network>().extend();
|
||||||
|
store<xmg_network>().current() = xmg;
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
if (store<aig_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty AIG network\n";
|
||||||
|
else {
|
||||||
|
auto aig = store<aig_network>().current();
|
||||||
|
direct_resynthesis<aig_network> aig_resyn;
|
||||||
|
refactoring(aig, aig_resyn);
|
||||||
|
aig = cleanup_dangling(aig);
|
||||||
|
phyLS::print_stats(aig);
|
||||||
|
store<aig_network>().extend();
|
||||||
|
store<aig_network>().current() = aig;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
private:
|
||||||
|
};
|
||||||
|
|
||||||
|
ALICE_ADD_COMMAND(refactor, "Logic synthesis")
|
||||||
|
|
||||||
|
} // namespace alice
|
||||||
|
|
||||||
|
#endif
|
|
@ -0,0 +1,144 @@
|
||||||
|
/* phyLS: powerful heightened yielded Logic Synthesis
|
||||||
|
* Copyright (C) 2022 */
|
||||||
|
|
||||||
|
/**
|
||||||
|
* @file resub.hpp
|
||||||
|
*
|
||||||
|
* @brief performs technology-independent restructuring
|
||||||
|
*
|
||||||
|
* @author Homyoung
|
||||||
|
* @since 2022/12/14
|
||||||
|
*/
|
||||||
|
|
||||||
|
#ifndef RESUB_HPP
|
||||||
|
#define RESUB_HPP
|
||||||
|
|
||||||
|
#include <time.h>
|
||||||
|
|
||||||
|
#include <kitty/static_truth_table.hpp>
|
||||||
|
#include <mockturtle/algorithms/aig_resub.hpp>
|
||||||
|
#include <mockturtle/algorithms/cleanup.hpp>
|
||||||
|
#include <mockturtle/algorithms/mig_resub.hpp>
|
||||||
|
#include <mockturtle/algorithms/resubstitution.hpp>
|
||||||
|
#include <mockturtle/algorithms/sim_resub.hpp>
|
||||||
|
#include <mockturtle/algorithms/simulation.hpp>
|
||||||
|
#include <mockturtle/algorithms/xag_resub_withDC.hpp>
|
||||||
|
#include <mockturtle/algorithms/xmg_resub.hpp>
|
||||||
|
#include <mockturtle/io/write_verilog.hpp>
|
||||||
|
#include <mockturtle/networks/aig.hpp>
|
||||||
|
#include <mockturtle/networks/mig.hpp>
|
||||||
|
#include <mockturtle/networks/xmg.hpp>
|
||||||
|
#include <mockturtle/traits.hpp>
|
||||||
|
#include <mockturtle/views/depth_view.hpp>
|
||||||
|
#include <mockturtle/views/fanout_view.hpp>
|
||||||
|
|
||||||
|
#include "../core/misc.hpp"
|
||||||
|
|
||||||
|
using namespace std;
|
||||||
|
|
||||||
|
namespace alice {
|
||||||
|
class resub_command : public command {
|
||||||
|
public:
|
||||||
|
explicit resub_command(const environment::ptr& env)
|
||||||
|
: command(env, "performs technology-independent restructuring : using AIG as default") {
|
||||||
|
add_flag("--xmg, -x", "Resubstitution for XMG");
|
||||||
|
add_flag("--mig, -m", "Resubstitution for MIG");
|
||||||
|
add_flag("--xag, -g", "Resubstitution for XAG");
|
||||||
|
add_flag("--simulation, -s", "Simulation-guided resubstitution for AIG");
|
||||||
|
add_flag("--verbose, -v", "print the information");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() {
|
||||||
|
clock_t begin, end;
|
||||||
|
double totalTime;
|
||||||
|
|
||||||
|
if (is_set("xmg")) {
|
||||||
|
if (store<xmg_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty XMG network\n";
|
||||||
|
else {
|
||||||
|
auto xmg = store<xmg_network>().current();
|
||||||
|
begin = clock();
|
||||||
|
using view_t = depth_view<fanout_view<xmg_network>>;
|
||||||
|
fanout_view<xmg_network> fanout_view{xmg};
|
||||||
|
view_t resub_view{fanout_view};
|
||||||
|
xmg_resubstitution(resub_view);
|
||||||
|
xmg = cleanup_dangling(xmg);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
phyLS::print_stats(xmg);
|
||||||
|
store<xmg_network>().extend();
|
||||||
|
store<xmg_network>().current() = xmg;
|
||||||
|
}
|
||||||
|
} else if (is_set("mig")) {
|
||||||
|
if (store<mig_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty MIG network\n";
|
||||||
|
else {
|
||||||
|
auto mig = store<mig_network>().current();
|
||||||
|
begin = clock();
|
||||||
|
using view_t = depth_view<fanout_view<mig_network>>;
|
||||||
|
fanout_view<mig_network> fanout_view{mig};
|
||||||
|
view_t resub_view{fanout_view};
|
||||||
|
mig_resubstitution(resub_view);
|
||||||
|
mig = cleanup_dangling(mig);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
phyLS::print_stats(mig);
|
||||||
|
store<mig_network>().extend();
|
||||||
|
store<mig_network>().current() = mig;
|
||||||
|
}
|
||||||
|
} else if (is_set("xag")) {
|
||||||
|
if (store<xag_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty XAG network\n";
|
||||||
|
else {
|
||||||
|
auto xag = store<xag_network>().current();
|
||||||
|
begin = clock();
|
||||||
|
resubstitution_params ps;
|
||||||
|
using view_t = depth_view<fanout_view<xag_network>>;
|
||||||
|
fanout_view<xag_network> fanout_view{xag};
|
||||||
|
view_t resub_view{fanout_view};
|
||||||
|
resubstitution_minmc_withDC(resub_view, ps);
|
||||||
|
xag = cleanup_dangling(xag);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
phyLS::print_stats(xag);
|
||||||
|
store<xag_network>().extend();
|
||||||
|
store<xag_network>().current() = xag;
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
if (store<aig_network>().size() == 0u)
|
||||||
|
std::cerr << "Error: Empty AIG network\n";
|
||||||
|
else {
|
||||||
|
auto aig = store<aig_network>().current();
|
||||||
|
if (is_set("simulation")) {
|
||||||
|
begin = clock();
|
||||||
|
sim_resubstitution(aig);
|
||||||
|
aig = cleanup_dangling(aig);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
} else {
|
||||||
|
begin = clock();
|
||||||
|
using view_t = depth_view<fanout_view<aig_network>>;
|
||||||
|
fanout_view<aig_network> fanout_view{aig};
|
||||||
|
view_t resub_view{fanout_view};
|
||||||
|
aig_resubstitution(resub_view);
|
||||||
|
aig = cleanup_dangling(aig);
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
}
|
||||||
|
phyLS::print_stats(aig);
|
||||||
|
store<aig_network>().extend();
|
||||||
|
store<aig_network>().current() = aig;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
ALICE_ADD_COMMAND(resub, "Logic synthesis")
|
||||||
|
|
||||||
|
} // namespace alice
|
||||||
|
|
||||||
|
#endif
|
|
@ -15,72 +15,85 @@
|
||||||
|
|
||||||
#include <mockturtle/algorithms/simulation.hpp>
|
#include <mockturtle/algorithms/simulation.hpp>
|
||||||
|
|
||||||
namespace alice
|
using namespace std;
|
||||||
{
|
|
||||||
|
|
||||||
class sim_command : public command
|
namespace alice {
|
||||||
{
|
|
||||||
public:
|
class sim_command : public command {
|
||||||
explicit sim_command(const environment::ptr &env) : command(env, "logic network simulation")
|
public:
|
||||||
{
|
explicit sim_command(const environment::ptr &env)
|
||||||
add_flag("-a, --aig_network", " simulate current aig network");
|
: command(env, "logic network simulation") {
|
||||||
add_flag("-x, --xmg_network", " simulate current xmg network");
|
add_flag("-a, --aig_network", " simulate current aig network");
|
||||||
add_flag("-p, --partial_simulate", " simulate current logic network using partial simulator ");
|
add_flag("-x, --xmg_network", " simulate current xmg network");
|
||||||
|
add_flag("-p, --partial_simulate",
|
||||||
|
" simulate current logic network using partial simulator ");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() {
|
||||||
|
clock_t begin, end;
|
||||||
|
double totalTime;
|
||||||
|
if (is_set("xmg_network")) {
|
||||||
|
begin = clock();
|
||||||
|
if (is_set("partial_simulate")) {
|
||||||
|
xmg_network xmg = store<xmg_network>().current();
|
||||||
|
std::vector<kitty::partial_truth_table> pats(xmg.num_pis());
|
||||||
|
for (auto i = 0; i < xmg.num_pis(); i++)
|
||||||
|
pats[i].add_bits(0x12345678, 32);
|
||||||
|
partial_simulator sim(pats);
|
||||||
|
unordered_node_map<kitty::partial_truth_table, xmg_network>
|
||||||
|
node_to_value(xmg);
|
||||||
|
simulate_nodes(xmg, node_to_value, sim);
|
||||||
|
|
||||||
|
xmg.foreach_po([&](auto const &f) {
|
||||||
|
std::cout << "tt: 0x"
|
||||||
|
<< (xmg.is_complemented(f) ? ~node_to_value[f]
|
||||||
|
: node_to_value[f])
|
||||||
|
._bits[0]
|
||||||
|
<< std::endl;
|
||||||
|
});
|
||||||
|
} else {
|
||||||
|
xmg_network xmg = store<xmg_network>().current();
|
||||||
|
default_simulator<kitty::dynamic_truth_table> sim(xmg.num_pis());
|
||||||
|
unordered_node_map<kitty::dynamic_truth_table, xmg_network>
|
||||||
|
node_to_value(xmg);
|
||||||
|
simulate_nodes(xmg, node_to_value, sim);
|
||||||
|
|
||||||
|
xmg.foreach_gate([&](auto const &n) {
|
||||||
|
std::cout << "node " << n << " tt: " << node_to_value[n]._bits[0]
|
||||||
|
<< std::endl;
|
||||||
|
});
|
||||||
|
|
||||||
|
xmg.foreach_po([&](auto const &f) {
|
||||||
|
std::cout << "PO tt: "
|
||||||
|
<< (xmg.is_complemented(f) ? ~node_to_value[f]
|
||||||
|
: node_to_value[f])
|
||||||
|
._bits[0]
|
||||||
|
<< std::endl;
|
||||||
|
});
|
||||||
|
// const auto tt = simulate<kitty::dynamic_truth_table>( xmg, sim )[0];
|
||||||
|
// std::cout << "tt: 0x" << tt._bits[0] << std::endl;
|
||||||
|
}
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
} else if (is_set("aig_network")) {
|
||||||
|
begin = clock();
|
||||||
|
aig_network aig = store<aig_network>().current();
|
||||||
|
default_simulator<kitty::dynamic_truth_table> sim(aig.num_pis());
|
||||||
|
const auto tt = simulate<kitty::dynamic_truth_table>(aig, sim)[0];
|
||||||
|
std::cout << "tt: " << tt._bits[0] << std::endl;
|
||||||
|
end = clock();
|
||||||
|
totalTime = (double)(end - begin) / CLOCKS_PER_SEC;
|
||||||
|
} else {
|
||||||
|
std::cout << "At least one store should be specified, see 'sim -h' for "
|
||||||
|
"help. \n";
|
||||||
}
|
}
|
||||||
|
cout.setf(ios::fixed);
|
||||||
|
cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
protected:
|
ALICE_ADD_COMMAND(sim, "Verification")
|
||||||
void execute()
|
} // namespace alice
|
||||||
{
|
|
||||||
if (is_set("xmg_network"))
|
|
||||||
{
|
|
||||||
if (is_set("partial_simulate"))
|
|
||||||
{
|
|
||||||
xmg_network xmg = store<xmg_network>().current();
|
|
||||||
std::vector<kitty::partial_truth_table> pats(xmg.num_pis());
|
|
||||||
for (auto i = 0; i < xmg.num_pis(); i++)
|
|
||||||
{
|
|
||||||
pats[i].add_bits(0x12345678, 32);
|
|
||||||
}
|
|
||||||
partial_simulator sim(pats);
|
|
||||||
|
|
||||||
unordered_node_map<kitty::partial_truth_table, xmg_network> node_to_value(xmg);
|
|
||||||
simulate_nodes(xmg, node_to_value, sim);
|
|
||||||
|
|
||||||
xmg.foreach_po([&](auto const &f)
|
|
||||||
{ std::cout << "tt: 0x" << (xmg.is_complemented(f) ? ~node_to_value[f] : node_to_value[f])._bits[0] << std::endl; });
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
xmg_network xmg = store<xmg_network>().current();
|
|
||||||
default_simulator<kitty::dynamic_truth_table> sim(xmg.num_pis());
|
|
||||||
unordered_node_map<kitty::dynamic_truth_table, xmg_network> node_to_value(xmg);
|
|
||||||
simulate_nodes(xmg, node_to_value, sim);
|
|
||||||
|
|
||||||
xmg.foreach_gate([&](auto const &n)
|
|
||||||
{ std::cout << "node " << n << " tt: " << node_to_value[n]._bits[0] << std::endl; });
|
|
||||||
|
|
||||||
xmg.foreach_po([&](auto const &f)
|
|
||||||
{ std::cout << "PO tt: " << (xmg.is_complemented(f) ? ~node_to_value[f] : node_to_value[f])._bits[0] << std::endl; });
|
|
||||||
|
|
||||||
// const auto tt = simulate<kitty::dynamic_truth_table>( xmg, sim )[0];
|
|
||||||
// std::cout << "tt: 0x" << tt._bits[0] << std::endl;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else if (is_set("aig_network"))
|
|
||||||
{
|
|
||||||
aig_network aig = store<aig_network>().current();
|
|
||||||
default_simulator<kitty::dynamic_truth_table> sim(aig.num_pis());
|
|
||||||
const auto tt = simulate<kitty::dynamic_truth_table>(aig, sim)[0];
|
|
||||||
std::cout << "tt: " << tt._bits[0] << std::endl;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
std::cout << "At least one store should be specified, see 'sim -h' for help. \n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
ALICE_ADD_COMMAND(sim, "Verification")
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -13,187 +13,161 @@
|
||||||
#ifndef STPSAT_HPP
|
#ifndef STPSAT_HPP
|
||||||
#define STPSAT_HPP
|
#define STPSAT_HPP
|
||||||
|
|
||||||
#include "../core/stp_sat.hpp"
|
|
||||||
#include <alice/alice.hpp>
|
#include <alice/alice.hpp>
|
||||||
#include <mockturtle/mockturtle.hpp>
|
#include <mockturtle/mockturtle.hpp>
|
||||||
|
|
||||||
|
#include "../core/stp_sat.hpp"
|
||||||
|
|
||||||
using namespace std;
|
using namespace std;
|
||||||
|
|
||||||
namespace alice
|
namespace alice {
|
||||||
{
|
class sat_command : public command {
|
||||||
class sat_command : public command
|
public:
|
||||||
{
|
explicit sat_command(const environment::ptr &env)
|
||||||
public:
|
: command(env, " circuit-based SAT solver") {
|
||||||
explicit sat_command(const environment::ptr &env) : command(env, " circuit-based SAT solver")
|
add_option("filename, -f", filename, "the input file name (CNF or BENCH)");
|
||||||
{
|
add_option("single_po, -s", strategy,
|
||||||
add_option("filename, -f", filename, "the input file name (CNF or BENCH)");
|
"select PO to solve (only in BENCH file)");
|
||||||
add_option("single_po, -s", strategy, "select PO to solve (only in BENCH file)");
|
add_flag("--verbose, -v", "verbose output");
|
||||||
add_flag("--verbose, -v", "verbose output");
|
}
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
void execute()
|
void execute() {
|
||||||
{
|
in.clear();
|
||||||
in.clear();
|
mtx.clear();
|
||||||
mtx.clear();
|
expre.clear();
|
||||||
expre.clear();
|
tt.clear();
|
||||||
tt.clear();
|
vec.clear();
|
||||||
vec.clear();
|
|
||||||
|
|
||||||
string tmp;
|
string tmp;
|
||||||
string s_cnf = ".cnf";
|
string s_cnf = ".cnf";
|
||||||
string s_bench = ".bench";
|
string s_bench = ".bench";
|
||||||
if (filename.find(s_bench) != string::npos)
|
if (filename.find(s_bench) != string::npos)
|
||||||
flag = 1;
|
flag = 1;
|
||||||
else if (filename.find(s_cnf) != string::npos)
|
else if (filename.find(s_cnf) != string::npos)
|
||||||
flag = 2;
|
flag = 2;
|
||||||
if (flag == 1)
|
if (flag == 1) {
|
||||||
{
|
ifstream fin_bench(filename);
|
||||||
ifstream fin_bench(filename);
|
|
||||||
|
|
||||||
if (fin_bench.is_open())
|
if (fin_bench.is_open()) {
|
||||||
{
|
while (getline(fin_bench, tmp)) in.push_back(tmp);
|
||||||
while (getline(fin_bench, tmp))
|
fin_bench.close();
|
||||||
in.push_back(tmp);
|
po = strategy;
|
||||||
fin_bench.close();
|
vector<string> &it = in;
|
||||||
po = strategy;
|
vector<vector<int>> &mtxvec = mtx;
|
||||||
vector<string> &it = in;
|
int &po_tmp = po;
|
||||||
vector<vector<int>> &mtxvec = mtx;
|
|
||||||
int &po_tmp = po;
|
|
||||||
stopwatch<>::duration time{0};
|
|
||||||
if (po < 0)
|
|
||||||
{
|
|
||||||
call_with_stopwatch(time, [&]()
|
|
||||||
{ phyLS::cdccl_for_all(it, mtxvec); });
|
|
||||||
if (it.size() == 0)
|
|
||||||
cout << "UNSAT" << endl;
|
|
||||||
else
|
|
||||||
cout << "SAT" << endl;
|
|
||||||
if (is_set("verbose"))
|
|
||||||
{
|
|
||||||
int count = 0;
|
|
||||||
cout << "SAT Result : " << endl;
|
|
||||||
for (string i : it)
|
|
||||||
{
|
|
||||||
cout << i << " ";
|
|
||||||
count += 1;
|
|
||||||
if (count == 10)
|
|
||||||
{
|
|
||||||
cout << endl;
|
|
||||||
count = 0;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
cout << endl
|
|
||||||
<< "Numbers of SAT Result : " << it.size() << endl;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
call_with_stopwatch(time, [&]()
|
|
||||||
{ phyLS::cdccl_for_single_po(it, mtxvec, po_tmp); });
|
|
||||||
if (it.size() == 0)
|
|
||||||
cout << "UNSAT" << endl;
|
|
||||||
else
|
|
||||||
cout << "SAT" << endl;
|
|
||||||
if (is_set("verbose"))
|
|
||||||
{
|
|
||||||
int count = 0;
|
|
||||||
cout << " SAT Result of "
|
|
||||||
<< "PO" << po << " : " << endl;
|
|
||||||
for (string i : it)
|
|
||||||
{
|
|
||||||
cout << i << " ";
|
|
||||||
count += 1;
|
|
||||||
if (count == 10)
|
|
||||||
{
|
|
||||||
cout << endl;
|
|
||||||
count = 0;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
cout << endl
|
|
||||||
<< "Numbers of SAT Result : " << it.size() << endl;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time));
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
cerr << "Cannot open input file" << endl;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else if (flag == 2)
|
|
||||||
{
|
|
||||||
ifstream fin_cnf(filename);
|
|
||||||
|
|
||||||
stringstream buffer;
|
|
||||||
buffer << fin_cnf.rdbuf();
|
|
||||||
string str(buffer.str());
|
|
||||||
string expression;
|
|
||||||
vector<int> expre;
|
|
||||||
for (int i = 6; i < (str.size() - 1); i++)
|
|
||||||
{
|
|
||||||
expression += str[i];
|
|
||||||
if ((str[i] == ' ') || (str[i] == '\n'))
|
|
||||||
{
|
|
||||||
expression.pop_back();
|
|
||||||
int intstr = atoi(expression.c_str());
|
|
||||||
expre.push_back(intstr);
|
|
||||||
expression.clear();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fin_cnf.close();
|
|
||||||
|
|
||||||
vector<int> &exp = expre;
|
|
||||||
vector<string> &t = tt;
|
|
||||||
vector<MatrixXi> &mtxvec = vec;
|
|
||||||
stopwatch<>::duration time{0};
|
stopwatch<>::duration time{0};
|
||||||
|
if (po < 0) {
|
||||||
call_with_stopwatch(time, [&]()
|
call_with_stopwatch(time,
|
||||||
{ phyLS::stp_cnf(exp, t, mtxvec); });
|
[&]() { phyLS::cdccl_for_all(it, mtxvec); });
|
||||||
|
if (it.size() == 0)
|
||||||
if (t.size() == 0)
|
cout << "UNSAT" << endl;
|
||||||
cout << "UNSAT" << endl;
|
else
|
||||||
else
|
cout << "SAT" << endl;
|
||||||
cout << "SAT" << endl;
|
if (is_set("verbose")) {
|
||||||
if (is_set("verbose"))
|
int count = 0;
|
||||||
{
|
cout << "SAT Result : " << endl;
|
||||||
int count = 0;
|
for (string i : it) {
|
||||||
cout << "SAT Result : " << endl;
|
cout << i << " ";
|
||||||
for (string i : t)
|
count += 1;
|
||||||
{
|
if (count == 10) {
|
||||||
cout << i << " ";
|
cout << endl;
|
||||||
count += 1;
|
count = 0;
|
||||||
if (count == 10)
|
}
|
||||||
{
|
|
||||||
cout << endl;
|
|
||||||
count = 0;
|
|
||||||
}
|
}
|
||||||
|
cout << endl << "Numbers of SAT Result : " << it.size() << endl;
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
call_with_stopwatch(
|
||||||
|
time, [&]() { phyLS::cdccl_for_single_po(it, mtxvec, po_tmp); });
|
||||||
|
if (it.size() == 0)
|
||||||
|
cout << "UNSAT" << endl;
|
||||||
|
else
|
||||||
|
cout << "SAT" << endl;
|
||||||
|
if (is_set("verbose")) {
|
||||||
|
int count = 0;
|
||||||
|
cout << " SAT Result of "
|
||||||
|
<< "PO" << po << " : " << endl;
|
||||||
|
for (string i : it) {
|
||||||
|
cout << i << " ";
|
||||||
|
count += 1;
|
||||||
|
if (count == 10) {
|
||||||
|
cout << endl;
|
||||||
|
count = 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
cout << endl << "Numbers of SAT Result : " << it.size() << endl;
|
||||||
}
|
}
|
||||||
cout << endl
|
|
||||||
<< "Numbers of SAT Result : " << t.size() << endl;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time));
|
cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time));
|
||||||
|
} else {
|
||||||
|
cerr << "Cannot open input file" << endl;
|
||||||
}
|
}
|
||||||
|
} else if (flag == 2) {
|
||||||
|
ifstream fin_cnf(filename);
|
||||||
|
|
||||||
|
stringstream buffer;
|
||||||
|
buffer << fin_cnf.rdbuf();
|
||||||
|
string str(buffer.str());
|
||||||
|
string expression;
|
||||||
|
vector<int> expre;
|
||||||
|
for (int i = 6; i < (str.size() - 1); i++) {
|
||||||
|
expression += str[i];
|
||||||
|
if ((str[i] == ' ') || (str[i] == '\n')) {
|
||||||
|
expression.pop_back();
|
||||||
|
int intstr = atoi(expression.c_str());
|
||||||
|
expre.push_back(intstr);
|
||||||
|
expression.clear();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fin_cnf.close();
|
||||||
|
|
||||||
|
vector<int> &exp = expre;
|
||||||
|
vector<string> &t = tt;
|
||||||
|
vector<MatrixXi> &mtxvec = vec;
|
||||||
|
stopwatch<>::duration time{0};
|
||||||
|
|
||||||
|
call_with_stopwatch(time, [&]() { phyLS::stp_cnf(exp, t, mtxvec); });
|
||||||
|
|
||||||
|
if (t.size() == 0)
|
||||||
|
cout << "UNSAT" << endl;
|
||||||
|
else
|
||||||
|
cout << "SAT" << endl;
|
||||||
|
if (is_set("verbose")) {
|
||||||
|
int count = 0;
|
||||||
|
cout << "SAT Result : " << endl;
|
||||||
|
for (string i : t) {
|
||||||
|
cout << i << " ";
|
||||||
|
count += 1;
|
||||||
|
if (count == 10) {
|
||||||
|
cout << endl;
|
||||||
|
count = 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
cout << endl << "Numbers of SAT Result : " << t.size() << endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
cout << fmt::format("[CPU time]: {:5.4f} seconds\n", to_seconds(time));
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
string filename;
|
string filename;
|
||||||
string cnf;
|
string cnf;
|
||||||
int strategy = -1;
|
int strategy = -1;
|
||||||
int po;
|
int po;
|
||||||
int flag = 0;
|
int flag = 0;
|
||||||
|
|
||||||
vector<string> in;
|
vector<string> in;
|
||||||
vector<vector<int>> mtx;
|
vector<vector<int>> mtx;
|
||||||
|
|
||||||
vector<int> expre;
|
vector<int> expre;
|
||||||
vector<string> tt;
|
vector<string> tt;
|
||||||
vector<MatrixXi> vec;
|
vector<MatrixXi> vec;
|
||||||
};
|
};
|
||||||
|
|
||||||
ALICE_ADD_COMMAND(sat, "Verification")
|
ALICE_ADD_COMMAND(sat, "Verification")
|
||||||
} // namespace alice
|
} // namespace alice
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -1,36 +1,35 @@
|
||||||
/* phyLS: powerful heightened yielded Logic Synthesis
|
/* phyLS: powerful heightened yielded Logic Synthesis
|
||||||
* Copyright (C) 2022 */
|
* Copyright (C) 2022 */
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @file techmap.hpp
|
* @file techmap.hpp
|
||||||
*
|
*
|
||||||
* @brief Standard cell mapping
|
* @brief Standard cell mapping
|
||||||
*
|
*
|
||||||
* @author Homyoung
|
* @author Homyoung
|
||||||
* @since 2022/12/14
|
* @since 2022/12/14
|
||||||
*/
|
*/
|
||||||
|
|
||||||
#ifndef TECHMAP_HPP
|
#ifndef TECHMAP_HPP
|
||||||
#define TECHMAP_HPP
|
#define TECHMAP_HPP
|
||||||
|
|
||||||
#include <mockturtle/algorithms/mapper.hpp>
|
#include <mockturtle/algorithms/mapper.hpp>
|
||||||
#include <mockturtle/utils/tech_library.hpp>
|
|
||||||
#include <mockturtle/io/genlib_reader.hpp>
|
#include <mockturtle/io/genlib_reader.hpp>
|
||||||
#include <mockturtle/io/write_verilog.hpp>
|
#include <mockturtle/io/write_verilog.hpp>
|
||||||
#include <mockturtle/networks/mig.hpp>
|
|
||||||
#include <mockturtle/networks/aig.hpp>
|
#include <mockturtle/networks/aig.hpp>
|
||||||
|
#include <mockturtle/networks/mig.hpp>
|
||||||
#include <mockturtle/networks/xmg.hpp>
|
#include <mockturtle/networks/xmg.hpp>
|
||||||
#include <mockturtle/properties/xmgcost.hpp>
|
#include <mockturtle/properties/xmgcost.hpp>
|
||||||
|
#include <mockturtle/utils/tech_library.hpp>
|
||||||
|
|
||||||
#include "../core/properties.hpp"
|
#include "../core/properties.hpp"
|
||||||
|
|
||||||
namespace alice
|
namespace alice {
|
||||||
{
|
|
||||||
|
|
||||||
class tech_mapping_command : public command
|
class tech_mapping_command: public command {
|
||||||
{
|
|
||||||
public:
|
public:
|
||||||
explicit tech_mapping_command(const environment::ptr &env) : command(env, "Standard cell mapping : using AIG as default")
|
explicit tech_mapping_command(const environment::ptr& env)
|
||||||
{
|
: command(env, "Standard cell mapping : using AIG as default") {
|
||||||
add_flag("--xmg, -x", "Standard cell mapping for XMG");
|
add_flag("--xmg, -x", "Standard cell mapping for XMG");
|
||||||
add_flag("--mig, -m", "Standard cell mapping for MIG");
|
add_flag("--mig, -m", "Standard cell mapping for MIG");
|
||||||
add_flag("--lut, -l", "Standard cell mapping for k-LUT");
|
add_flag("--lut, -l", "Standard cell mapping for k-LUT");
|
||||||
|
@ -38,32 +37,27 @@ namespace alice
|
||||||
add_flag("--verbose, -v", "print the information");
|
add_flag("--verbose, -v", "print the information");
|
||||||
}
|
}
|
||||||
|
|
||||||
rules validity_rules() const
|
rules validity_rules() const {
|
||||||
{
|
return { has_store_element<std::vector<mockturtle::gate>>(env) };
|
||||||
return {has_store_element<std::vector<mockturtle::gate>>(env)};
|
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
std::string filename = "techmap.v";
|
std::string filename = "techmap.v";
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
void execute()
|
void execute() {
|
||||||
{
|
|
||||||
/* derive genlib */
|
/* derive genlib */
|
||||||
std::vector<mockturtle::gate> gates = store<std::vector<mockturtle::gate>>().current();
|
std::vector<mockturtle::gate> gates =
|
||||||
|
store<std::vector<mockturtle::gate>>().current();
|
||||||
|
|
||||||
mockturtle::tech_library<5> lib(gates);
|
mockturtle::tech_library<5> lib(gates);
|
||||||
mockturtle::map_params ps;
|
mockturtle::map_params ps;
|
||||||
mockturtle::map_stats st;
|
mockturtle::map_stats st;
|
||||||
|
|
||||||
if (is_set("xmg"))
|
if (is_set("xmg")) {
|
||||||
{
|
|
||||||
if (store<xmg_network>().size() == 0u)
|
if (store<xmg_network>().size() == 0u)
|
||||||
{
|
|
||||||
std::cerr << "[e] no XMG in the store\n";
|
std::cerr << "[e] no XMG in the store\n";
|
||||||
}
|
else {
|
||||||
else
|
|
||||||
{
|
|
||||||
auto xmg = store<xmg_network>().current();
|
auto xmg = store<xmg_network>().current();
|
||||||
xmg_gate_stats stats;
|
xmg_gate_stats stats;
|
||||||
xmg_profile_gates(xmg, stats);
|
xmg_profile_gates(xmg, stats);
|
||||||
|
@ -77,72 +71,67 @@ namespace alice
|
||||||
|
|
||||||
auto res = mockturtle::map(xmg, lib, ps, &st);
|
auto res = mockturtle::map(xmg, lib, ps, &st);
|
||||||
|
|
||||||
if (is_set("output"))
|
if (is_set("output")) {
|
||||||
{
|
|
||||||
write_verilog_with_binding(res, filename);
|
write_verilog_with_binding(res, filename);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::cout << fmt::format("[i] Mapped XMG into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay);
|
std::cout << fmt::format(
|
||||||
|
"[i] Mapped XMG into #gates = {} area = {:.2f} delay = {:.2f}\n",
|
||||||
|
res.num_gates(), st.area, st.delay);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (is_set("mig"))
|
else if (is_set("mig")) {
|
||||||
{
|
if (store<mig_network>().size() == 0u) {
|
||||||
if (store<mig_network>().size() == 0u)
|
|
||||||
{
|
|
||||||
std::cerr << "[e] no MIG in the store\n";
|
std::cerr << "[e] no MIG in the store\n";
|
||||||
}
|
}
|
||||||
else
|
else {
|
||||||
{
|
|
||||||
auto mig = store<mig_network>().current();
|
auto mig = store<mig_network>().current();
|
||||||
|
|
||||||
auto res = mockturtle::map(mig, lib, ps, &st);
|
auto res = mockturtle::map(mig, lib, ps, &st);
|
||||||
|
|
||||||
if (is_set("output"))
|
if (is_set("output")) {
|
||||||
{
|
|
||||||
write_verilog_with_binding(res, filename);
|
write_verilog_with_binding(res, filename);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::cout << fmt::format("Mapped MIG into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay);
|
std::cout << fmt::format(
|
||||||
|
"Mapped MIG into #gates = {} area = {:.2f} delay = {:.2f}\n",
|
||||||
|
res.num_gates(), st.area, st.delay);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (is_set("lut"))
|
else if (is_set("lut")) {
|
||||||
{
|
if (store<klut_network>().size() == 0u) {
|
||||||
if (store<klut_network>().size() == 0u)
|
|
||||||
{
|
|
||||||
std::cerr << "[e] no k-LUT in the store\n";
|
std::cerr << "[e] no k-LUT in the store\n";
|
||||||
}
|
}
|
||||||
else
|
else {
|
||||||
{
|
|
||||||
auto lut = store<klut_network>().current();
|
auto lut = store<klut_network>().current();
|
||||||
|
|
||||||
auto res = mockturtle::map(lut, lib, ps, &st);
|
auto res = mockturtle::map(lut, lib, ps, &st);
|
||||||
|
|
||||||
if (is_set("output"))
|
if (is_set("output")) {
|
||||||
{
|
|
||||||
write_verilog_with_binding(res, filename);
|
write_verilog_with_binding(res, filename);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::cout << fmt::format("Mapped k-LUT into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay);
|
std::cout << fmt::format(
|
||||||
|
"Mapped k-LUT into #gates = {} area = {:.2f} delay = {:.2f}\n",
|
||||||
|
res.num_gates(), st.area, st.delay);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else
|
else {
|
||||||
{
|
if (store<aig_network>().size() == 0u) {
|
||||||
if (store<aig_network>().size() == 0u)
|
|
||||||
{
|
|
||||||
std::cerr << "[e] no AIG in the store\n";
|
std::cerr << "[e] no AIG in the store\n";
|
||||||
}
|
}
|
||||||
else
|
else {
|
||||||
{
|
|
||||||
auto aig = store<aig_network>().current();
|
auto aig = store<aig_network>().current();
|
||||||
|
|
||||||
auto res = mockturtle::map(aig, lib, ps, &st);
|
auto res = mockturtle::map(aig, lib, ps, &st);
|
||||||
|
|
||||||
if (is_set("output"))
|
if (is_set("output")) {
|
||||||
{
|
|
||||||
write_verilog_with_binding(res, filename);
|
write_verilog_with_binding(res, filename);
|
||||||
}
|
}
|
||||||
|
|
||||||
std::cout << fmt::format("Mapped AIG into #gates = {} area = {:.2f} delay = {:.2f}\n", res.num_gates(), st.area, st.delay);
|
std::cout << fmt::format(
|
||||||
|
"Mapped AIG into #gates = {} area = {:.2f} delay = {:.2f}\n",
|
||||||
|
res.num_gates(), st.area, st.delay);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -150,6 +139,6 @@ namespace alice
|
||||||
|
|
||||||
ALICE_ADD_COMMAND(tech_mapping, "Mapping")
|
ALICE_ADD_COMMAND(tech_mapping, "Mapping")
|
||||||
|
|
||||||
}
|
} // namespace alice
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -13,63 +13,52 @@
|
||||||
#ifndef WRITE_DOT_HPP
|
#ifndef WRITE_DOT_HPP
|
||||||
#define WRITE_DOT_HPP
|
#define WRITE_DOT_HPP
|
||||||
|
|
||||||
#include <mockturtle/mockturtle.hpp>
|
|
||||||
#include <mockturtle/io/write_dot.hpp>
|
#include <mockturtle/io/write_dot.hpp>
|
||||||
|
#include <mockturtle/mockturtle.hpp>
|
||||||
|
|
||||||
namespace alice
|
namespace alice {
|
||||||
{
|
|
||||||
|
|
||||||
class write_dot_command : public command
|
class write_dot_command : public command {
|
||||||
{
|
public:
|
||||||
public:
|
explicit write_dot_command(const environment::ptr &env)
|
||||||
explicit write_dot_command(const environment::ptr &env) : command(env, "write dot file")
|
: command(env, "write dot file") {
|
||||||
{
|
add_flag("--xmg_network,-x", "write xmg_network into dot files");
|
||||||
add_flag("--xmg_network,-x", "write xmg_network into dot files");
|
add_flag("--aig_network,-a", "write aig_network into dot files");
|
||||||
add_flag("--aig_network,-a", "write aig_network into dot files");
|
add_flag("--mig_network,-m", "write mig_network into dot files");
|
||||||
add_flag("--mig_network,-m", "write mig_network into dot files");
|
add_flag("--klut_network,-l", "write klut_network into dot files");
|
||||||
add_flag("--klut_network,-l", "write klut_network into dot files");
|
add_option("--filename, -f", filename,
|
||||||
add_option("--filename, -f", filename, "The path to store dot file, default: /tmp/test.dot");
|
"The path to store dot file, default: /tmp/test.dot");
|
||||||
|
}
|
||||||
|
|
||||||
|
protected:
|
||||||
|
void execute() {
|
||||||
|
if (is_set("xmg_network")) {
|
||||||
|
xmg_network xmg = store<xmg_network>().current();
|
||||||
|
|
||||||
|
write_dot(xmg, filename, gate_dot_drawer<xmg_network>{});
|
||||||
|
} else if (is_set("aig_network")) {
|
||||||
|
aig_network aig = store<aig_network>().current();
|
||||||
|
|
||||||
|
write_dot(aig, filename, gate_dot_drawer<aig_network>{});
|
||||||
|
} else if (is_set("mig_network")) {
|
||||||
|
mig_network mig = store<mig_network>().current();
|
||||||
|
|
||||||
|
write_dot(mig, filename, gate_dot_drawer<mig_network>{});
|
||||||
|
} else if (is_set("klut_network")) {
|
||||||
|
klut_network klut = store<klut_network>().current();
|
||||||
|
|
||||||
|
write_dot(klut, filename, gate_dot_drawer<klut_network>{});
|
||||||
|
} else {
|
||||||
|
assert(false && " at least one store should be specified ");
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
protected:
|
private:
|
||||||
void execute()
|
std::string filename = "/tmp/test.dot";
|
||||||
{
|
};
|
||||||
if (is_set("xmg_network"))
|
|
||||||
{
|
|
||||||
xmg_network xmg = store<xmg_network>().current();
|
|
||||||
|
|
||||||
write_dot(xmg, filename, gate_dot_drawer<xmg_network>{});
|
ALICE_ADD_COMMAND(write_dot, "I/O")
|
||||||
}
|
|
||||||
else if (is_set("aig_network"))
|
|
||||||
{
|
|
||||||
aig_network aig = store<aig_network>().current();
|
|
||||||
|
|
||||||
write_dot(aig, filename, gate_dot_drawer<aig_network>{});
|
} // namespace alice
|
||||||
}
|
|
||||||
else if (is_set("mig_network"))
|
|
||||||
{
|
|
||||||
mig_network mig = store<mig_network>().current();
|
|
||||||
|
|
||||||
write_dot(mig, filename, gate_dot_drawer<mig_network>{});
|
|
||||||
}
|
|
||||||
else if (is_set("klut_network"))
|
|
||||||
{
|
|
||||||
klut_network klut = store<klut_network>().current();
|
|
||||||
|
|
||||||
write_dot(klut, filename, gate_dot_drawer<klut_network>{});
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
assert(false && " at least one store should be specified ");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
std::string filename = "/tmp/test.dot";
|
|
||||||
};
|
|
||||||
|
|
||||||
ALICE_ADD_COMMAND(write_dot, "I/O")
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -10,14 +10,10 @@
|
||||||
|
|
||||||
using namespace std;
|
using namespace std;
|
||||||
|
|
||||||
class MatrixXi
|
class MatrixXi {
|
||||||
{
|
friend ostream &operator<<(ostream &os, const MatrixXi &m) {
|
||||||
friend ostream &operator<<(ostream &os, const MatrixXi &m)
|
for (size_t i = 0; i < m.row; i++) {
|
||||||
{
|
for (size_t j = 0; j < m.col; j++) {
|
||||||
for (size_t i = 0; i < m.row; i++)
|
|
||||||
{
|
|
||||||
for (size_t j = 0; j < m.col; j++)
|
|
||||||
{
|
|
||||||
os << m.data[i][j] << " ";
|
os << m.data[i][j] << " ";
|
||||||
}
|
}
|
||||||
os << endl;
|
os << endl;
|
||||||
|
@ -25,60 +21,49 @@ class MatrixXi
|
||||||
return os;
|
return os;
|
||||||
}
|
}
|
||||||
|
|
||||||
friend istream &operator>>(istream &is, MatrixXi &m)
|
friend istream &operator>>(istream &is, MatrixXi &m) {
|
||||||
{
|
for (size_t i = 0; i < m.row; i++) {
|
||||||
for (size_t i = 0; i < m.row; i++)
|
for (size_t j = 0; j < m.col; j++) {
|
||||||
{
|
|
||||||
for (size_t j = 0; j < m.col; j++)
|
|
||||||
{
|
|
||||||
is >> m.data[i][j];
|
is >> m.data[i][j];
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return is;
|
return is;
|
||||||
}
|
}
|
||||||
|
|
||||||
public:
|
public:
|
||||||
typedef int value_type;
|
typedef int value_type;
|
||||||
typedef vector<int>::size_type size_type;
|
typedef vector<int>::size_type size_type;
|
||||||
|
|
||||||
MatrixXi()
|
MatrixXi() {
|
||||||
{
|
|
||||||
row = 0;
|
row = 0;
|
||||||
col = 0;
|
col = 0;
|
||||||
data.clear();
|
data.clear();
|
||||||
}
|
}
|
||||||
MatrixXi(size_t i, size_t j)
|
MatrixXi(size_t i, size_t j) {
|
||||||
{
|
|
||||||
row = i;
|
row = i;
|
||||||
col = j;
|
col = j;
|
||||||
vector<vector<int>> vdata(row, vector<int>(col, 0));
|
vector<vector<int>> vdata(row, vector<int>(col, 0));
|
||||||
data = move(vdata);
|
data = move(vdata);
|
||||||
}
|
}
|
||||||
|
|
||||||
MatrixXi(const MatrixXi &m)
|
MatrixXi(const MatrixXi &m) {
|
||||||
{
|
|
||||||
row = m.row;
|
row = m.row;
|
||||||
col = m.col;
|
col = m.col;
|
||||||
data = m.data;
|
data = m.data;
|
||||||
}
|
}
|
||||||
|
|
||||||
MatrixXi &operator=(const MatrixXi &m)
|
MatrixXi &operator=(const MatrixXi &m) {
|
||||||
{
|
|
||||||
row = m.row;
|
row = m.row;
|
||||||
col = m.col;
|
col = m.col;
|
||||||
data = m.data;
|
data = m.data;
|
||||||
return *this;
|
return *this;
|
||||||
}
|
}
|
||||||
|
|
||||||
static MatrixXi product(MatrixXi &m, MatrixXi &n)
|
static MatrixXi product(MatrixXi &m, MatrixXi &n) {
|
||||||
{
|
|
||||||
MatrixXi t(m.row, n.col);
|
MatrixXi t(m.row, n.col);
|
||||||
for (size_t i = 0; i < m.row; i++)
|
for (size_t i = 0; i < m.row; i++) {
|
||||||
{
|
for (size_t j = 0; j < n.col; j++) {
|
||||||
for (size_t j = 0; j < n.col; j++)
|
for (size_t k = 0; k < m.col; k++) {
|
||||||
{
|
|
||||||
for (size_t k = 0; k < m.col; k++)
|
|
||||||
{
|
|
||||||
t.data[i][j] += (m.data[i][k] * n.data[k][j]);
|
t.data[i][j] += (m.data[i][k] * n.data[k][j]);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -86,19 +71,13 @@ public:
|
||||||
return t;
|
return t;
|
||||||
}
|
}
|
||||||
|
|
||||||
static MatrixXi eye(size_t n)
|
static MatrixXi eye(size_t n) {
|
||||||
{
|
|
||||||
MatrixXi A(n, n);
|
MatrixXi A(n, n);
|
||||||
for (size_t i = 0; i < n; i++)
|
for (size_t i = 0; i < n; i++) {
|
||||||
{
|
for (size_t j = 0; j < n; j++) {
|
||||||
for (size_t j = 0; j < n; j++)
|
if (i == j) {
|
||||||
{
|
|
||||||
if (i == j)
|
|
||||||
{
|
|
||||||
A.data[i][j] = 1;
|
A.data[i][j] = 1;
|
||||||
}
|
} else {
|
||||||
else
|
|
||||||
{
|
|
||||||
A.data[i][j] = 0;
|
A.data[i][j] = 0;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -106,57 +85,37 @@ public:
|
||||||
return A;
|
return A;
|
||||||
}
|
}
|
||||||
|
|
||||||
static MatrixXi kron(const MatrixXi &m, const MatrixXi &n)
|
static MatrixXi kron(const MatrixXi &m, const MatrixXi &n) {
|
||||||
{
|
|
||||||
size_t a = m.row;
|
size_t a = m.row;
|
||||||
size_t b = m.col;
|
size_t b = m.col;
|
||||||
size_t c = n.row;
|
size_t c = n.row;
|
||||||
size_t d = n.col;
|
size_t d = n.col;
|
||||||
MatrixXi t(a * c, b * d);
|
MatrixXi t(a * c, b * d);
|
||||||
for (size_t i = 0; i < a * c; i++)
|
for (size_t i = 0; i < a * c; i++) {
|
||||||
{
|
for (size_t j = 0; j < b * d; j++) {
|
||||||
for (size_t j = 0; j < b * d; j++)
|
|
||||||
{
|
|
||||||
t.data[i][j] = m.data[i / c][j / d] * n.data[i % c][j % d];
|
t.data[i][j] = m.data[i / c][j / d] * n.data[i % c][j % d];
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return t;
|
return t;
|
||||||
}
|
}
|
||||||
|
|
||||||
~MatrixXi()
|
~MatrixXi() { data.clear(); }
|
||||||
{
|
|
||||||
data.clear();
|
|
||||||
}
|
|
||||||
|
|
||||||
int &operator()(size_t i, size_t j)
|
int &operator()(size_t i, size_t j) { return data[i][j]; }
|
||||||
{
|
const int &operator()(size_t i, size_t j) const { return data[i][j]; }
|
||||||
return data[i][j];
|
size_t rows() const { return row; }
|
||||||
}
|
size_t cols() const { return col; }
|
||||||
const int &operator()(size_t i, size_t j) const
|
|
||||||
{
|
|
||||||
return data[i][j];
|
|
||||||
}
|
|
||||||
size_t rows() const
|
|
||||||
{
|
|
||||||
return row;
|
|
||||||
}
|
|
||||||
size_t cols() const
|
|
||||||
{
|
|
||||||
return col;
|
|
||||||
}
|
|
||||||
|
|
||||||
void resize(size_t nr, size_t nc)
|
void resize(size_t nr, size_t nc) {
|
||||||
{
|
|
||||||
data.resize(nr);
|
data.resize(nr);
|
||||||
for (size_t i = 0; i < nr; i++)
|
for (size_t i = 0; i < nr; i++) {
|
||||||
{
|
|
||||||
data[i].resize(nc);
|
data[i].resize(nc);
|
||||||
}
|
}
|
||||||
col = nc;
|
col = nc;
|
||||||
row = nr;
|
row = nr;
|
||||||
}
|
}
|
||||||
|
|
||||||
private:
|
private:
|
||||||
size_t row;
|
size_t row;
|
||||||
size_t col;
|
size_t col;
|
||||||
vector<vector<int>> data;
|
vector<vector<int>> data;
|
||||||
|
|
|
@ -0,0 +1,158 @@
|
||||||
|
#include <algorithm>
|
||||||
|
#include <percy/percy.hpp>
|
||||||
|
#include <string>
|
||||||
|
#include <sstream>
|
||||||
|
|
||||||
|
#include "misc.hpp"
|
||||||
|
|
||||||
|
using namespace percy;
|
||||||
|
using namespace mockturtle;
|
||||||
|
|
||||||
|
namespace phyLS
|
||||||
|
{
|
||||||
|
std::vector<std::string> split_by_delim(const std::string& s, char delim)
|
||||||
|
{
|
||||||
|
std::vector<std::string> elems;
|
||||||
|
split_by_delim(s, delim, std::back_inserter(elems));
|
||||||
|
return elems;
|
||||||
|
}
|
||||||
|
|
||||||
|
template <typename Iterator>
|
||||||
|
inline bool next_combination(const Iterator first, Iterator k, const Iterator last)
|
||||||
|
{
|
||||||
|
/* Credits: Thomas Draper */
|
||||||
|
if ((first == last) || (first == k) || (last == k))
|
||||||
|
return false;
|
||||||
|
Iterator itr1 = first;
|
||||||
|
Iterator itr2 = last;
|
||||||
|
++itr1;
|
||||||
|
if (last == itr1)
|
||||||
|
return false;
|
||||||
|
itr1 = last;
|
||||||
|
--itr1;
|
||||||
|
itr1 = k;
|
||||||
|
--itr2;
|
||||||
|
while (first != itr1)
|
||||||
|
{
|
||||||
|
if (*--itr1 < *itr2)
|
||||||
|
{
|
||||||
|
Iterator j = k;
|
||||||
|
while (!(*itr1 < *j)) ++j;
|
||||||
|
std::iter_swap(itr1, j);
|
||||||
|
++itr1;
|
||||||
|
++j;
|
||||||
|
itr2 = k;
|
||||||
|
std::rotate(itr1, j, last);
|
||||||
|
while (last != j)
|
||||||
|
{
|
||||||
|
++j;
|
||||||
|
++itr2;
|
||||||
|
}
|
||||||
|
std::rotate(k, itr2, last);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
std::rotate(first, k, last);
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
std::vector<std::vector<unsigned>> get_all_combination_index(std::vector<unsigned>& vars,
|
||||||
|
const unsigned& n,
|
||||||
|
const unsigned& k)
|
||||||
|
{
|
||||||
|
std::vector<std::vector<unsigned>> index;
|
||||||
|
std::vector<unsigned> tmp;
|
||||||
|
|
||||||
|
do
|
||||||
|
{
|
||||||
|
tmp.clear();
|
||||||
|
for (unsigned i = 0; i < k; ++i)
|
||||||
|
{
|
||||||
|
tmp.push_back(vars[i]);
|
||||||
|
}
|
||||||
|
index.push_back(tmp);
|
||||||
|
} while (next_combination(vars.begin(), vars.begin() + k, vars.end()));
|
||||||
|
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
|
||||||
|
std::vector<std::vector<unsigned>> get_all_permutation(const std::vector<unsigned>& vars)
|
||||||
|
{
|
||||||
|
std::vector<std::vector<unsigned>> v;
|
||||||
|
auto vec_copy = vars;
|
||||||
|
|
||||||
|
std::sort(vec_copy.begin(), vec_copy.end());
|
||||||
|
|
||||||
|
do
|
||||||
|
{
|
||||||
|
v.push_back(vec_copy);
|
||||||
|
} while (std::next_permutation(vec_copy.begin(), vec_copy.end()));
|
||||||
|
|
||||||
|
return v;
|
||||||
|
}
|
||||||
|
|
||||||
|
void print_sat_clause(solver_wrapper* solver, pabc::lit* begin, pabc::lit* end)
|
||||||
|
{
|
||||||
|
printf("Add clause: ");
|
||||||
|
pabc::lit* i;
|
||||||
|
for (i = begin; i < end; i++)
|
||||||
|
printf("%s%d ", (*i) & 1 ? "!" : "", (*i) >> 1);
|
||||||
|
printf("\n");
|
||||||
|
}
|
||||||
|
|
||||||
|
int add_print_clause(std::vector<std::vector<int>>& clauses, pabc::lit* begin, pabc::lit* end)
|
||||||
|
{
|
||||||
|
std::vector<int> clause;
|
||||||
|
while (begin != end) {
|
||||||
|
clause.push_back(*begin);
|
||||||
|
begin++;
|
||||||
|
}
|
||||||
|
clauses.push_back(clause);
|
||||||
|
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
|
||||||
|
std::vector<std::string> split(const std::string& s, char delimiter)
|
||||||
|
{
|
||||||
|
std::vector<std::string> tokens;
|
||||||
|
std::string token;
|
||||||
|
std::istringstream tokenStream(s);
|
||||||
|
while (std::getline(tokenStream, token, delimiter))
|
||||||
|
{
|
||||||
|
tokens.push_back(token);
|
||||||
|
std::cout << token << std::endl;
|
||||||
|
}
|
||||||
|
return tokens;
|
||||||
|
}
|
||||||
|
|
||||||
|
std::vector<std::string> split(const std::string& str, const std::string& sep)
|
||||||
|
{
|
||||||
|
std::vector<std::string> result;
|
||||||
|
|
||||||
|
size_t last = 0;
|
||||||
|
size_t next = 0;
|
||||||
|
while ((next = str.find(sep, last)) != std::string::npos)
|
||||||
|
{
|
||||||
|
result.push_back(str.substr(last, next - last));
|
||||||
|
last = next + 1;
|
||||||
|
}
|
||||||
|
result.push_back(str.substr(last));
|
||||||
|
|
||||||
|
return result;
|
||||||
|
}
|
||||||
|
|
||||||
|
void to_dimacs(FILE* f, solver_wrapper* solver, std::vector<std::vector<int>>& clauses)
|
||||||
|
{
|
||||||
|
fprintf(f, "p cnf %d %d\n", solver->nr_vars(), clauses.size());
|
||||||
|
for (const auto& clause : clauses) {
|
||||||
|
for (const auto lit : clause) {
|
||||||
|
// NOTE: variable 0 does not exist in DIMACS format
|
||||||
|
const auto var = pabc::Abc_Lit2Var(lit) + 1;
|
||||||
|
const auto is_c = pabc::Abc_LitIsCompl(lit);
|
||||||
|
fprintf(f, "%d ", is_c ? -var : var);
|
||||||
|
}
|
||||||
|
fprintf(f, "0\n");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,59 @@
|
||||||
|
#pragma once
|
||||||
|
|
||||||
|
#include <mockturtle/mockturtle.hpp>
|
||||||
|
#include <percy/percy.hpp>
|
||||||
|
|
||||||
|
using namespace percy;
|
||||||
|
using namespace mockturtle;
|
||||||
|
|
||||||
|
namespace phyLS
|
||||||
|
{
|
||||||
|
template<typename Out>
|
||||||
|
void split_by_delim(const std::string& s, char delim, Out result)
|
||||||
|
{
|
||||||
|
std::stringstream ss(s);
|
||||||
|
std::string item;
|
||||||
|
while (std::getline(ss, item, delim)) {
|
||||||
|
*(result++) = item;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
std::vector<std::string> split_by_delim(const std::string& s, char delim);
|
||||||
|
|
||||||
|
template <typename Iterator>
|
||||||
|
inline bool next_combination(const Iterator first, Iterator k, const Iterator last);
|
||||||
|
|
||||||
|
std::vector<std::vector<unsigned>> get_all_combination_index(std::vector<unsigned>& vars,
|
||||||
|
const unsigned& n,
|
||||||
|
const unsigned& k);
|
||||||
|
|
||||||
|
std::vector<std::vector<unsigned>> get_all_permutation(const std::vector<unsigned>& vars);
|
||||||
|
|
||||||
|
template <typename T>
|
||||||
|
void show_array(const std::vector<T>& array)
|
||||||
|
{
|
||||||
|
std::cout << "Elements: ";
|
||||||
|
for (const auto& x : array)
|
||||||
|
{
|
||||||
|
std::cout << " " << x;
|
||||||
|
}
|
||||||
|
std::cout << std::endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
void print_sat_clause(solver_wrapper* solver, pabc::lit* begin, pabc::lit* end);
|
||||||
|
int add_print_clause(std::vector<std::vector<int>>& clauses, pabc::lit* begin, pabc::lit* end);
|
||||||
|
std::vector<std::string> split(const std::string& s, char delimiter);
|
||||||
|
|
||||||
|
std::vector<std::string> split(const std::string& str, const std::string& sep);
|
||||||
|
void to_dimacs(FILE* f, solver_wrapper* solver, std::vector<std::vector<int>>& clauses);
|
||||||
|
|
||||||
|
template<class Ntk>
|
||||||
|
void print_stats(const Ntk& ntk)
|
||||||
|
{
|
||||||
|
//auto copy = ntk;
|
||||||
|
//depth_view depth_ntk{ ntk };
|
||||||
|
using depth_ntk = depth_view<Ntk>;
|
||||||
|
std::cout << fmt::format("ntk i/o = {}/{} gates = {} level = {}\n", ntk.num_pis(), ntk.num_pos(), ntk.num_gates(), depth_ntk{ ntk }.depth());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
|
@ -3,95 +3,77 @@
|
||||||
|
|
||||||
#include "properties.hpp"
|
#include "properties.hpp"
|
||||||
|
|
||||||
|
namespace phyLS {
|
||||||
|
std::vector<uint32_t> split_xmg_critical_path(xmg_network const& xmg) {
|
||||||
|
uint32_t xor3{0}, xor2{0}, maj{0}, and_or{0};
|
||||||
|
depth_view dxmg{xmg};
|
||||||
|
|
||||||
namespace phyLS
|
node<xmg_network> cp_node;
|
||||||
{
|
|
||||||
std::vector<uint32_t> split_xmg_critical_path( xmg_network const& xmg )
|
|
||||||
{
|
|
||||||
uint32_t xor3{ 0 }, xor2{ 0 }, maj{ 0 }, and_or{ 0 };
|
|
||||||
depth_view dxmg{ xmg };
|
|
||||||
|
|
||||||
node<xmg_network> cp_node;
|
/* find the po on critical path */
|
||||||
|
xmg.foreach_po([&](auto const& f) {
|
||||||
|
auto level = dxmg.level(xmg.get_node(f));
|
||||||
|
|
||||||
/* find the po on critical path */
|
if (level == dxmg.depth()) {
|
||||||
xmg.foreach_po( [&]( auto const& f ) {
|
cp_node = xmg.get_node(f);
|
||||||
auto level = dxmg.level( xmg.get_node( f ) );
|
return false;
|
||||||
|
|
||||||
if( level == dxmg.depth() )
|
|
||||||
{
|
|
||||||
cp_node = xmg.get_node( f );
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
|
|
||||||
return true;
|
|
||||||
} );
|
|
||||||
|
|
||||||
/* recursive until reach the primary inputs */
|
|
||||||
while( !xmg.is_constant( cp_node ) && !xmg.is_pi( cp_node ) )
|
|
||||||
{
|
|
||||||
bool has_constant_fanin = false;
|
|
||||||
|
|
||||||
/* check if all the fanin nodes are not constant */
|
|
||||||
xmg.foreach_fanin( cp_node, [&]( auto const& f ) {
|
|
||||||
if( xmg.is_constant( xmg.get_node( f ) ) )
|
|
||||||
{
|
|
||||||
has_constant_fanin = true;
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
} );
|
|
||||||
|
|
||||||
if( xmg.is_maj( cp_node ) )
|
|
||||||
{
|
|
||||||
if( has_constant_fanin )
|
|
||||||
{
|
|
||||||
++and_or;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
++maj;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else if( xmg.is_xor3( cp_node ) )
|
|
||||||
{
|
|
||||||
if( has_constant_fanin )
|
|
||||||
{
|
|
||||||
++xor2;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
++xor3;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
assert( false && "UNKNOWN operator" );
|
|
||||||
}
|
|
||||||
|
|
||||||
/* continue process fanin node */
|
|
||||||
xmg.foreach_fanin( cp_node, [&]( auto const& f ) {
|
|
||||||
auto level = dxmg.level( xmg.get_node( f ) );
|
|
||||||
|
|
||||||
if( level + 1 == dxmg.level( cp_node ) )
|
|
||||||
{
|
|
||||||
cp_node = xmg.get_node( f );
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
} );
|
|
||||||
}
|
}
|
||||||
|
|
||||||
std::vector<uint32_t> v{ xor3, xor2, maj, and_or };
|
return true;
|
||||||
return v;
|
});
|
||||||
}
|
|
||||||
|
/* recursive until reach the primary inputs */
|
||||||
void xmg_critical_path_profile_gates( xmg_network const& xmg, xmg_critical_path_stats& stats )
|
while (!xmg.is_constant(cp_node) && !xmg.is_pi(cp_node)) {
|
||||||
{
|
bool has_constant_fanin = false;
|
||||||
auto v = split_xmg_critical_path( xmg );
|
|
||||||
stats.xor3 = v[0];
|
/* check if all the fanin nodes are not constant */
|
||||||
stats.xor2 = v[1];
|
xmg.foreach_fanin(cp_node, [&](auto const& f) {
|
||||||
stats.maj = v[2];
|
if (xmg.is_constant(xmg.get_node(f))) {
|
||||||
stats.and_or = v[3];
|
has_constant_fanin = true;
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
});
|
||||||
|
|
||||||
|
if (xmg.is_maj(cp_node)) {
|
||||||
|
if (has_constant_fanin) {
|
||||||
|
++and_or;
|
||||||
|
} else {
|
||||||
|
++maj;
|
||||||
|
}
|
||||||
|
} else if (xmg.is_xor3(cp_node)) {
|
||||||
|
if (has_constant_fanin) {
|
||||||
|
++xor2;
|
||||||
|
} else {
|
||||||
|
++xor3;
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
assert(false && "UNKNOWN operator");
|
||||||
|
}
|
||||||
|
|
||||||
|
/* continue process fanin node */
|
||||||
|
xmg.foreach_fanin(cp_node, [&](auto const& f) {
|
||||||
|
auto level = dxmg.level(xmg.get_node(f));
|
||||||
|
|
||||||
|
if (level + 1 == dxmg.level(cp_node)) {
|
||||||
|
cp_node = xmg.get_node(f);
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
std::vector<uint32_t> v{xor3, xor2, maj, and_or};
|
||||||
|
return v;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void xmg_critical_path_profile_gates(xmg_network const& xmg,
|
||||||
|
xmg_critical_path_stats& stats) {
|
||||||
|
auto v = split_xmg_critical_path(xmg);
|
||||||
|
stats.xor3 = v[0];
|
||||||
|
stats.xor2 = v[1];
|
||||||
|
stats.maj = v[2];
|
||||||
|
stats.and_or = v[3];
|
||||||
|
}
|
||||||
|
|
||||||
|
} // namespace phyLS
|
||||||
|
|
|
@ -13,30 +13,29 @@
|
||||||
#ifndef PROPERTIES_HPP
|
#ifndef PROPERTIES_HPP
|
||||||
#define PROPERTIES_HPP
|
#define PROPERTIES_HPP
|
||||||
|
|
||||||
|
#include <fmt/format.h>
|
||||||
|
|
||||||
#include <mockturtle/networks/xmg.hpp>
|
#include <mockturtle/networks/xmg.hpp>
|
||||||
#include <mockturtle/views/depth_view.hpp>
|
#include <mockturtle/views/depth_view.hpp>
|
||||||
#include <fmt/format.h>
|
|
||||||
|
|
||||||
using namespace mockturtle;
|
using namespace mockturtle;
|
||||||
|
|
||||||
namespace phyLS
|
namespace phyLS {
|
||||||
{
|
struct xmg_critical_path_stats {
|
||||||
struct xmg_critical_path_stats
|
uint32_t xor3{0};
|
||||||
{
|
uint32_t xor2{0};
|
||||||
uint32_t xor3{ 0 };
|
uint32_t maj{0};
|
||||||
uint32_t xor2{ 0 };
|
uint32_t and_or{0};
|
||||||
uint32_t maj{ 0 };
|
|
||||||
uint32_t and_or{ 0 };
|
|
||||||
|
|
||||||
void report() const
|
void report() const {
|
||||||
{
|
fmt::print("On critical path: XOR3: {}, XOR2: {}, MAJ: {}, AND/OR: {}\n",
|
||||||
fmt::print( "On critical path: XOR3: {}, XOR2: {}, MAJ: {}, AND/OR: {}\n",
|
xor3, xor2, maj, and_or);
|
||||||
xor3, xor2, maj, and_or );
|
}
|
||||||
}
|
};
|
||||||
};
|
|
||||||
|
|
||||||
void xmg_critical_path_profile_gates( xmg_network const& xmg, xmg_critical_path_stats& stats );
|
|
||||||
|
|
||||||
}
|
void xmg_critical_path_profile_gates(xmg_network const& xmg,
|
||||||
|
xmg_critical_path_stats& stats);
|
||||||
|
|
||||||
|
} // namespace phyLS
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
2957
src/core/stp_sat.hpp
2957
src/core/stp_sat.hpp
File diff suppressed because it is too large
Load Diff
|
@ -0,0 +1,26 @@
|
||||||
|
GATE _const0_ 0.00 z=CONST0;
|
||||||
|
GATE _const1_ 0.00 z=CONST1;
|
||||||
|
GATE inv1 1 O=!a; PIN * INV 1 999 0.9 0.3 0.9 0.3
|
||||||
|
GATE inv2 2 O=!a; PIN * INV 2 999 1.0 0.1 1.0 0.1
|
||||||
|
GATE inv3 3 O=!a; PIN * INV 3 999 1.1 0.09 1.1 0.09
|
||||||
|
GATE inv4 4 O=!a; PIN * INV 4 999 1.2 0.07 1.2 0.07
|
||||||
|
GATE nand2 2 O=!(a*b); PIN * INV 1 999 1.0 0.2 1.0 0.2
|
||||||
|
GATE nand3 3 O=!(a*b*c); PIN * INV 1 999 1.1 0.3 1.1 0.3
|
||||||
|
GATE nand4 4 O=!(a*b*c*d); PIN * INV 1 999 1.4 0.4 1.4 0.4
|
||||||
|
GATE nor2 2 O=!(a+b); PIN * INV 1 999 1.4 0.5 1.4 0.5
|
||||||
|
GATE nor3 3 O=!(a+b+c); PIN * INV 1 999 2.4 0.7 2.4 0.7
|
||||||
|
GATE nor4 4 O=!(a+b+c+d); PIN * INV 1 999 3.8 1.0 3.8 1.0
|
||||||
|
GATE and2 3 O=a*b; PIN * NONINV 1 999 1.9 0.3 1.9 0.3
|
||||||
|
GATE or2 3 O=a+b; PIN * NONINV 1 999 2.4 0.3 2.4 0.3
|
||||||
|
GATE xor2a 5 O=a*!b+!a*b; PIN * UNKNOWN 2 999 1.9 0.5 1.9 0.5
|
||||||
|
GATE xor2b 5 O=!(a*b+!a*!b); PIN * UNKNOWN 2 999 1.9 0.5 1.9 0.5
|
||||||
|
GATE xnor2a 5 O=a*b+!a*!b; PIN * UNKNOWN 2 999 2.1 0.5 2.1 0.5
|
||||||
|
GATE xnor2b 5 O=!(!a*b+a*!b); PIN * UNKNOWN 2 999 2.1 0.5 2.1 0.5
|
||||||
|
GATE mig3 3 O=(a*b+a*c+b*c); PIN * INV 1 999 2.0 0.2 2.0 0.2
|
||||||
|
GATE xor3 6 O=((a*!b+!a*b)*!c+!(a*!b+!a*b)*c); PIN * INV 1 999 2.0 0.2 2.0 0.2
|
||||||
|
GATE aoi21 3 O=!(a*b+c); PIN * INV 1 999 1.6 0.4 1.6 0.4
|
||||||
|
GATE aoi22 4 O=!(a*b+c*d); PIN * INV 1 999 2.0 0.4 2.0 0.4
|
||||||
|
GATE oai21 3 O=!((a+b)*c); PIN * INV 1 999 1.6 0.4 1.6 0.4
|
||||||
|
GATE oai22 4 O=!((a+b)*(c+d)); PIN * INV 1 999 2.0 0.4 2.0 0.4
|
||||||
|
GATE buf 1 O=a; PIN * NONINV 1 999 1.0 0.0 1.0 0.0
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
/* phyLS: powerful heightened yielded Logic Synthesis
|
/* phyLS: powerful heightened yielded Logic Synthesis
|
||||||
* Copyright (C) 2022
|
* Copyright (C) 2022
|
||||||
*
|
*
|
||||||
* Permission is hereby granted, free of charge, to any person
|
* Permission is hereby granted, free of charge, to any person
|
||||||
* obtaining a copy of this software and associated documentation
|
* obtaining a copy of this software and associated documentation
|
||||||
|
@ -24,13 +24,16 @@
|
||||||
*/
|
*/
|
||||||
|
|
||||||
#include "store.hpp"
|
#include "store.hpp"
|
||||||
#include "commands/load.hpp"
|
#include "commands/balance.hpp"
|
||||||
#include "commands/exprsim.hpp"
|
#include "commands/exprsim.hpp"
|
||||||
#include "commands/write_dot.hpp"
|
#include "commands/load.hpp"
|
||||||
#include "commands/techmap.hpp"
|
|
||||||
#include "commands/lut_mapping.hpp"
|
#include "commands/lut_mapping.hpp"
|
||||||
|
#include "commands/node_resynthesis.hpp"
|
||||||
|
#include "commands/resub.hpp"
|
||||||
#include "commands/sim.hpp"
|
#include "commands/sim.hpp"
|
||||||
#include "commands/stpsat.hpp"
|
#include "commands/stpsat.hpp"
|
||||||
|
#include "commands/techmap.hpp"
|
||||||
|
#include "commands/write_dot.hpp"
|
||||||
|
#include "commands/refactor.hpp"
|
||||||
|
|
||||||
|
ALICE_MAIN(phyLS)
|
||||||
ALICE_MAIN( phyLS )
|
|
Loading…
Reference in New Issue