diff --git a/src/commands/cec.hpp b/src/commands/cec.hpp new file mode 100644 index 0000000..71fd272 --- /dev/null +++ b/src/commands/cec.hpp @@ -0,0 +1,79 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file cec.hpp + * + * @brief performs combinational equivalence checking + * + * @author Homyoung + * @since 2022/12/14 + */ + +#ifndef CEC_HPP +#define CEC_HPP + +#include +#include +#include +#include +#include + +using namespace std; +using namespace mockturtle; + +namespace alice { + +class cec_command : public command { + public: + explicit cec_command(const environment::ptr& env) + : command(env, "combinational equivalence checking for AIG network") { + add_option("file_1, -a", filename_1, "the input file name"); + add_option("file_2, -b", filename_2, "the input file name"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + + begin = clock(); + aig_network aig1, aig2; + if ((lorina::read_aiger(filename_1, mockturtle::aiger_reader(aig1)) == + lorina::return_code::success) && + (lorina::read_aiger(filename_2, mockturtle::aiger_reader(aig2)) == + lorina::return_code::success)) { + if (aig1.num_pis() != aig2.num_pis()) + std::cerr << "Networks have different number of primary inputs." + << std::endl + << "Miter computation has failed." << std::endl; + else { + const auto miter_ntk = *miter(aig1, aig2); + equivalence_checking_stats st; + const auto result = equivalence_checking(miter_ntk, {}, &st); + if (result) + std::cout << "Networks are equivalent." << std::endl; + else + std::cout << "Networks are NOT EQUIVALENT." << std::endl; + } + } else { + std::cerr << "[w] parse error" << std::endl; + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } + + private: + string filename_1; + string filename_2; +}; + +ALICE_ADD_COMMAND(cec, "Verification") + +} // namespace alice + +#endif \ No newline at end of file diff --git a/src/commands/convert_graph.hpp b/src/commands/convert_graph.hpp new file mode 100644 index 0000000..114a731 --- /dev/null +++ b/src/commands/convert_graph.hpp @@ -0,0 +1,104 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file convert_graph.hpp + * + * @brief performs decomposable function for resynthesis graph + * + * @author Homyoung + * @since 2022/12/20 + */ + +#ifndef CONVERT_GRAPH_HPP +#define CONVERT_GRAPH_HPP + +#include +#include + +using namespace std; +using namespace mockturtle; + +namespace alice { + +class create_graph_command : public command { + public: + explicit create_graph_command(const environment::ptr& env) + : command(env, "functional reduction : using AIG as default") { + add_option("-e,--expression", expression, + "creates new graph from expression"); + add_flag("--mig, -m", "functional reduction for MIG"); + add_flag("--xag, -g", "functional reduction for XAG"); + add_flag("--xmg, -x", "functional reduction for XMG"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + + begin = clock(); + auto& opt_ntks = store(); + if (opt_ntks.empty()) opt_ntks.extend(); + + uint32_t num_vars{0u}; + for (auto c : expression) { + if (c >= 'a' && c <= 'p') + num_vars = std::max(num_vars, c - 'a' + 1u); + } + + kitty::dynamic_truth_table tt(num_vars); + kitty::create_from_expression(tt, expression); + + klut_network kLUT_ntk; + vector children; + for (auto i = 0; i < num_vars; i++) { + const auto x = kLUT_ntk.create_pi(); + children.push_back(x); + } + + auto fn = [&](kitty::dynamic_truth_table const& remainder, + std::vector const& children) { + return kLUT_ntk.create_node(children, remainder); + }; + + kLUT_ntk.create_po(dsd_decomposition(kLUT_ntk, tt, children, fn)); + + if (is_set("mig")) { + auto mig = convert_klut_to_graph(kLUT_ntk); + phyLS::print_stats(mig); + store().extend(); + store().current() = mig; + } else if (is_set("xmg")) { + auto xmg = convert_klut_to_graph(kLUT_ntk); + phyLS::print_stats(xmg); + store().extend(); + store().current() = xmg; + } else if (is_set("xag")) { + auto xag = convert_klut_to_graph(kLUT_ntk); + phyLS::print_stats(xag); + store().extend(); + store().current() = xag; + } else { + auto aig = convert_klut_to_graph(kLUT_ntk); + phyLS::print_stats(aig); + store().extend(); + store().current() = aig; + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } + + private: + string expression = ""; +}; + +ALICE_ADD_COMMAND(create_graph, "Logic synthesis") + +} // namespace alice + +#endif \ No newline at end of file diff --git a/src/commands/functional_reduction.hpp b/src/commands/functional_reduction.hpp new file mode 100644 index 0000000..cbcb98b --- /dev/null +++ b/src/commands/functional_reduction.hpp @@ -0,0 +1,89 @@ +/* phyLS: powerful heightened yielded Logic Synthesis + * Copyright (C) 2022 */ + +/** + * @file functional_reduction.hpp + * + * @brief performs functional reduction + * + * @author Homyoung + * @since 2022/12/20 + */ + +#ifndef FUCNTIONAL_REDUCTION_HPP +#define FUCNTIONAL_REDUCTION_HPP + +#include +#include +#include +#include +#include +#include +#include +#include + +using namespace std; +using namespace mockturtle; + +namespace alice { + +class reduction_command : public command { + public: + explicit reduction_command(const environment::ptr& env) + : command(env, "functional reduction : using AIG as default") { + add_flag("--mig, -m", "functional reduction for MIG"); + add_flag("--xag, -g", "functional reduction for XAG"); + add_flag("--xmg, -x", "functional reduction for XMG"); + add_flag("--verbose, -v", "print the information"); + } + + protected: + void execute() { + clock_t begin, end; + double totalTime; + + begin = clock(); + if (is_set("mig")) { + auto mig = store().current(); + functional_reduction(mig); + mig = cleanup_dangling(mig); + phyLS::print_stats(mig); + store().extend(); + store().current() = mig; + } else if (is_set("xmg")) { + auto xmg = store().current(); + functional_reduction(xmg); + xmg = cleanup_dangling(xmg); + phyLS::print_stats(xmg); + store().extend(); + store().current() = xmg; + } else if (is_set("xag")) { + auto xag = store().current(); + functional_reduction(xag); + xag = cleanup_dangling(xag); + phyLS::print_stats(xag); + store().extend(); + store().current() = xag; + } else { + auto aig = store().current(); + functional_reduction(aig); + aig = cleanup_dangling(aig); + phyLS::print_stats(aig); + store().extend(); + store().current() = aig; + } + end = clock(); + totalTime = (double)(end - begin) / CLOCKS_PER_SEC; + + cout.setf(ios::fixed); + cout << "[CPU time] " << setprecision(2) << totalTime << " s" << endl; + } + + private: +}; + +ALICE_ADD_COMMAND(reduction, "Logic synthesis") + +} // namespace alice + +#endif \ No newline at end of file diff --git a/src/phyLS.cpp b/src/phyLS.cpp index 8cae23f..ac5d128 100644 --- a/src/phyLS.cpp +++ b/src/phyLS.cpp @@ -36,5 +36,8 @@ #include "commands/write_dot.hpp" #include "commands/refactor.hpp" #include "commands/cut_rewriting.hpp" +#include "commands/cec.hpp" +#include "commands/functional_reduction.hpp" +#include "commands/convert_graph.hpp" ALICE_MAIN(phyLS) \ No newline at end of file