diff --git a/src/convert_muxig_opt.cpp b/src/convert_muxig_opt.cpp index a740992..80657ee 100644 --- a/src/convert_muxig_opt.cpp +++ b/src/convert_muxig_opt.cpp @@ -1,258 +1,260 @@ #include #include #include #include #include #include #include #include #include "lorina/blif.hpp" #include "mockturtle/algorithms/cover_to_graph.hpp" #include "mockturtle/networks/cover.hpp" #include "mockturtle/networks/muxig.hpp" #include "mockturtle/algorithms/sim_resub.hpp" #include "mockturtle/io/blif_reader.hpp" #include "mockturtle/io/write_blif.hpp" #define SEL_INDEX 0 #define IN0_INDEX 2 #define IN1_INDEX 1 #define SEL(ntk, node) ntk._storage->nodes[node].children[SEL_INDEX] #define IN0(ntk, node) ntk._storage->nodes[node].children[IN0_INDEX] #define IN1(ntk, node) ntk._storage->nodes[node].children[IN1_INDEX] int main(int argc, char *argv[]) { // Default values int max_pis = 10; // 8; int max_divisors = 150; int max_inserts = 20; // 2; bool output_path_given = false; std::string output_dir; int opt; while ((opt = getopt(argc, argv, "o:p:d:i:")) != -1) { switch (opt) { case 'o': output_path_given = true; output_dir = optarg; break; case 'p': max_pis = std::atoi(optarg); break; case 'd': max_divisors = std::atoi(optarg); break; case 'i': max_inserts = std::atoi(optarg); break; default: std::cerr << "Usage: " << argv[0] << " [-p max_pi] [-d max_divisors] [-i max_inserts] [-o " "output_file for performance statistics]" "\n"; return 1; } } std::string benchmark; if (optind < argc) { benchmark = argv[optind]; } else { std::cerr << "Error: Missing required positional argument.\n"; std::cerr << "Usage: " << argv[0] << " [-p max_pi] [-d max_divisors] [-i max_inserts] \n"; return 1; } if (!std::filesystem::exists(benchmark)) { std::cout << "[ERROR] File does not exist\n"; return EXIT_FAILURE; } std::filesystem::path path(benchmark); std::string base_name = path.stem().string(); mockturtle::cover_network cover; if (lorina::read_blif(benchmark, mockturtle::blif_reader(cover)) != lorina::return_code::success) { std::cout << "[ERROR] While Lorina tried to read in file\n"; return EXIT_FAILURE; } std::filesystem::path order_output_dir_path; std::filesystem::path base_name_path; std::filesystem::path order_file_path; std::ofstream order_file; mockturtle::muxig_network muxig_original = mockturtle::convert_cover_to_graph(cover); mockturtle::resubstitution_params ps; mockturtle::resubstitution_stats st; ps.max_inserts = max_inserts; ps.max_pis = max_pis; ps.max_divisors = max_divisors; ps.progress = false; ps.verbose = false; int size_before = muxig_original.num_gates(); mockturtle::sim_resubstitution(muxig_original, ps, &st); muxig_original = mockturtle::cleanup_dangling(muxig_original); int size_after = muxig_original.num_gates(); /*mockturtle::muxig_network muxig_sel = muxig_original.clone(); mockturtle::muxig_network muxig_and = muxig_original.clone(); mockturtle::muxig_network muxig_or = muxig_original.clone(); mockturtle::muxig_network muxig_all = muxig_original.clone();*/ mockturtle::muxig_network muxig = muxig_original.clone(); // jaspers /*printf("before: %d, after: %d, sel: %d, and: %d, or: %d, all: %d\n", size_before, muxig_original.num_gates(), muxig_sel.num_gates(), muxig_and.num_gates(), muxig_or.num_gates(), muxig_all.num_gates());*/ // Info from mockturtle library /* mux(a b c) = a b + a' c */ muxig.foreach_node([&](auto node) { if (muxig.is_mux(node) && (muxig.fanin_size(node) == 3)) { // if a and b are inverted push inverter to output if (muxig.is_complemented(IN0(muxig, node)) && muxig.is_complemented(IN1(muxig, node))) { muxig.substitute_node( node, muxig.create_not(muxig.create_gate( SEL(muxig, node), muxig.create_not(IN1(muxig, node)), muxig.create_not(IN0(muxig, node))))); } if (IN0(muxig, node).index == IN1(muxig, node).index){ assert(muxig.is_complemented(IN0(muxig, node)) || muxig.is_complemented(IN1(muxig, node))); printf("xor possibly\n"); } } }); mockturtle::fanout_view fnntk(muxig); muxig.foreach_node([&](auto node) { if (muxig.is_mux(node) && (muxig.fanin_size(node) == 3)) { uint32_t inv = muxig.fanout_size(node); std::vector> fanout_stack; fnntk.foreach_fanout(node, [&](auto fan_out) { int i = 0; muxig.foreach_fanin(fan_out, [&](auto signal) { if (muxig.get_node(signal) == node) { if (signal.complement) { inv--; } fanout_stack.emplace_back(fan_out, i); } i++; }); }); int output_count = 0; muxig.foreach_po([&](auto po) { if (muxig.get_node(po) == node && muxig.is_complemented(po)) { inv--; fanout_stack.emplace_back(output_count, -1); } output_count++; }); // if all fanouts are inverted if (inv == 0 && muxig.fanout_size(node) != 0) { if (IN1(muxig, node) == 0 && IN0(muxig, node) != 0 && !muxig.is_complemented(IN1(muxig, node))) { // 0 is represented as 0 and 1 as !0 // switching not(not a and b) to (a or not b) // this gets rid of all inverters at the output std::swap(SEL(muxig, node), IN0(muxig, node)); std::swap(IN1(muxig, node), IN0(muxig, node)); IN0(muxig, node) = muxig.get_constant(true); for (const auto &[node, child] : fanout_stack) { if (child >= 0) { muxig._storage->nodes[node].children[child] = muxig.create_not(muxig._storage->nodes[node].children[child]); } else { muxig._storage->outputs[node] = muxig.create_not(muxig._storage->outputs[node]); } } } else if (IN0(muxig, node) == 0 && IN1(muxig, node) != 0 && muxig.is_complemented(IN0(muxig, node))) { // switching not(not a or b) to (a and not b) std::swap(SEL(muxig, node), IN1(muxig, node)); std::swap(IN1(muxig, node), IN0(muxig, node)); IN1(muxig, node) = muxig.get_constant(false); for (const auto &[node, child] : fanout_stack) { if (child >= 0) { muxig._storage->nodes[node].children[child] = muxig.create_not(muxig._storage->nodes[node].children[child]); } else { muxig._storage->outputs[node] = muxig.create_not(muxig._storage->outputs[node]); } } } } } }); muxig.foreach_node([&](auto node) { if (muxig.is_mux(node) && (muxig.fanin_size(node) == 3)) { if (muxig.is_complemented(SEL(muxig, node))) { std::swap(IN0(muxig, node), IN1(muxig, node)); SEL(muxig, node) = muxig.create_not(SEL(muxig, node)); assert(!muxig.is_complemented(SEL(muxig, node))); } // and not if (IN0(muxig, node) == 0 && !muxig.is_complemented(IN0(muxig, node))) { if (muxig.is_complemented(IN1(muxig, node))) { // (sel, IN1, IN0) std::swap(IN1(muxig, node), SEL(muxig, node)); std::swap(IN0(muxig, node), IN1(muxig, node)); SEL(muxig, node) = muxig.create_not(SEL(muxig, node)); } } // or not if (IN1(muxig, node) == 1) { if (muxig.is_complemented(IN0(muxig, node))) { std::swap(IN0(muxig, node), SEL(muxig, node)); std::swap(IN0(muxig, node), IN1(muxig, node)); SEL(muxig, node) = muxig.create_not(SEL(muxig, node)); } } } }); if (output_path_given) { order_output_dir_path = output_dir; base_name_path = base_name; base_name_path.replace_extension(".csv"); order_file_path = order_output_dir_path / base_name_path; printf("Writing stats to %s\n", order_file_path.c_str()); order_file.open(order_file_path); order_file << "before;after;inv_before;inv_all\n"; order_file << size_before << ";" << size_after << ";" << mockturtle::num_inverters(muxig_original) << ";" << mockturtle::num_inverters(muxig) << "\n"; } printf("inverter before: %d after: %d\n", mockturtle::num_inverters(muxig_original), mockturtle::num_inverters(muxig)); /*printf("removed by sel: %d\n", mockturtle::num_inverters(muxig_original) - mockturtle::num_inverters(muxig_sel)); printf("removed by and not: %d\n", mockturtle::num_inverters(muxig_original) - mockturtle::num_inverters(muxig_and)); printf("removed by or not: %d\n", mockturtle::num_inverters(muxig_original) - mockturtle::num_inverters(muxig_or));*/ - mockturtle::write_blif(muxig, "temp/" + base_name + "_muxig_temp.blif"); + std::string const netlist_dir = output_path_given ? output_dir : "temp"; + mockturtle::write_blif(muxig, + netlist_dir + "/" + base_name + "_muxig_temp.blif"); return EXIT_SUCCESS; } diff --git a/synth.sh b/synth.sh index 7f4a020..451df66 100755 --- a/synth.sh +++ b/synth.sh @@ -1,203 +1,208 @@ #!/bin/bash BBDD_SCRIPT="yosys/bbdd_synth_muxxor.ys" BDD_SCRIPT="yosys/bdd_synth.ys" MUXIG_SCRIPT="yosys/muxig_synth.ys" TEMP_DIR="temp" LIBERTY_FILE="liberty/nem_thesis.lib" TIMEOUT="2m" #1 minute timeout for now TECHMAP_BBDD="yosys/techmap_bbdd.v" TABLE_SIZE="300000" MAX_INPUTS=0 # 0 disables partitioning, i.e. one diagram over all inputs print_options(){ echo "(1) Synthesis Verilog file with bbdd optimization" echo "(2) Synthesis Verilog file with bdd optimization" echo "(3) Synthesis Verilog file with muxig optimization" echo "(e) Exit" } safe_path() { local unsafe_path="$1" echo "$(printf '%s\n' "$unsafe_path" | sed 's/[&/\]/\\&/g')" } process_input() { file_name=$(basename "$file_path") # with extension file_base="${file_name%.*}" # without # get top module name read -p "top module [default=${file_base}] " top_module top_module=${top_module:-${file_base}} #safe_file_path=$(printf '%s\n' "$file_path" | sed 's/[&/\]/\\&/g') safe_file_path=$(safe_path "$file_path") #safe_techmap_path=$(printf '%s\n' "$TECHMAP_BBDD" | sed 's/[&/\]/\\&/g') } run_yosys() { # Run yosys if $nosat; then sat_replacement="#" # comment out {{SAT}} else sat_replacement="" # replace {{SAT}} with nothing fi - # options handed to the converter; the bbdd template picks them up through - # {{CONV_FLAGS}}. convert_bdd takes no options, and its template has no - # placeholder, so the substitution is a no-op there. - conv_flags="-t $TABLE_SIZE" - if [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then - conv_flags="$conv_flags -n $MAX_INPUTS" + # converter options, substituted into {{CONV_FLAGS}} + if [ "$opt_name" = "muxig" ]; then + converter="./build/src/convert_muxig_opt" + conv_flags="-o $TEMP_DIR" + else + converter="./build/src/convert_$opt_name" + conv_flags="-t $TABLE_SIZE -o $TEMP_DIR" + if [ "$MAX_INPUTS" -gt 0 ] 2>/dev/null; then + conv_flags="$conv_flags -n $MAX_INPUTS" + fi fi echo "Synthesising $file_base" sed -e "s/{{VERILOG_FILE}}/$safe_file_path/g" \ -e "s/{{TEMP_DIR}}/$TEMP_DIR/g" \ -e "s/{{TOP_MODULE}}/$top_module/g" \ -e "s/{{BASE_NAME}}/$file_base/g" \ -e "s/{{TECHMAP_BBDD}}/$safe_techmap_path/g" \ -e "s/{{LIBERTY_FILE}}/$safe_liberty_path/g" \ - -e "s/{{OUT_DIR}}/$safe_out_path/g" \ + -e "s/{{CASE_DIR}}/$(safe_path "${out_dir}${file_base}")/g" \ + -e "s|{{CONVERTER}}|$converter|g" \ -e "s/{{TIMEOUT}}/$TIMEOUT/g" \ -e "s/{{SAT}}/$sat_replacement/g" \ -e "s/{{CONV_FLAGS}}/$(safe_path "$conv_flags")/g" \ "$yosys_script" > "$TEMP_DIR/${file_base}_synth.ys" if $STRIP_NOSCOPEINFO; then sed -i 's/flatten -noscopeinfo/flatten/' "$TEMP_DIR/${file_base}_synth.ys" fi mkdir -p ${out_dir}/${file_base}/ /usr/bin/time -f "Time: %E\nCPU: %P\nMemory: %M KB" -o ${out_dir}/${file_base}/yosys_${opt_name}_time.txt yosys${yosys_flags} ${TEMP_DIR}/${file_base}_synth.ys if [ -e ${out_dir}/${file_base} ]; then # the summary is optional; don't report its failure as a synthesis failure if [ -n "$PYTHON" ]; then "$PYTHON" ./yosys/print_summary.py ${out_dir}/${file_base} \ || echo "[WARN] print_summary.py failed; results are still in ${out_dir}/${file_base}" else echo "[WARN] no python interpreter found; skipping print_summary.py" fi else echo "${file_base} did not finish in time" fi } synth_verilog() { local yosys_script="$1" local opt_name="$2" if ! $verbose; then yosys_flags=" -q" # is quite mode else yosys_flags="" fi safe_techmap_path=$(safe_path "$TECHMAP_BBDD") safe_liberty_path=$(safe_path "$LIBERTY_FILE") echo "Using script: $yosys_script" read -e -p 'Input file path: ' file_path # Get Output Dir read -e -p 'Output directory: ' out_dir safe_out_path=$(safe_path "$out_dir") out_dir="${out_dir%/}/" if [ -f "$file_path" ]; then process_input run_yosys if ! $nocleanup; then rm ${TEMP_DIR}/${file_base}_synth.ys rm ${TEMP_DIR}/${file_base}.blif rm -f ${TEMP_DIR}/${file_base}_bbdd.blif rm -f ${TEMP_DIR}/${file_base}_bdd.blif fi exit elif [ -d "$file_path" ]; then # extend / if not present file_path="${file_path%/}/" for file in "$file_path"*.v; do if [ -e "$file" ]; then safe_file_path=$(safe_path "$file") file_name=$(basename "$file") # with extension file_base="${file_name%.*}" # without top_module="$file_base" yosys_flags=" -q" run_yosys if ! $nocleanup; then rm ${TEMP_DIR}/${file_base}_synth.ys rm ${TEMP_DIR}/${file_base}.blif rm -f ${TEMP_DIR}/${file_base}_bbdd.blif rm -f ${TEMP_DIR}/${file_base}_bdd.blif fi fi done exit else echo "[ERROR] File ${file_path} does not exist" fi } handle_selection() { case "$1" in 1) synth_verilog $BBDD_SCRIPT "bbdd";; 2) synth_verilog $BDD_SCRIPT "bdd";; 3) synth_verilog $MUXIG_SCRIPT "muxig";; e) echo "Exiting..."; exit 0 ;; *) echo "Invalid option. Please try again." ;; esac } # Initialize booleans as false nocleanup=false nosat=false verbose=false # Parse flags while [[ $# -gt 0 ]]; do case "$1" in -nocleanup) nocleanup=true shift ;; -nosat) nosat=true shift ;; -v) verbose=true shift ;; -n) MAX_INPUTS="$2" shift 2 ;; *) echo "Unknown option: $1" echo "Usage: $0 [-nocleanup] [-nosat] [-v] [-n MAX_INPUTS]" exit 1 ;; esac done # some distros ship only python3 PYTHON="" for candidate in python3 python; do if command -v "$candidate" >/dev/null 2>&1; then PYTHON="$candidate" break fi done # yosys < 0.40 has no `flatten -noscopeinfo` (and no $scopeinfo cells to # drop), so strip the flag there. No -q: it would silence `help` too. STRIP_NOSCOPEINFO=false -if ! yosys -qp "help flatten" 2>/dev/null | grep -q -- "-noscopeinfo"; then +if ! yosys -p "help flatten" 2>/dev/null | grep -q -- "-noscopeinfo"; then STRIP_NOSCOPEINFO=true echo "[INFO] yosys $(yosys -V 2>/dev/null | awk '{print $2}') has no 'flatten -noscopeinfo'; stripping the flag" fi # get input file mkdir -p $TEMP_DIR while true; do if [ "$nosat" = false ]; then echo "Satisfiability check is enabled" fi print_options read -p "Enter your choice [1-3]: " choice handle_selection "$choice" echo "" done diff --git a/yosys/bbdd_synth_muxxor.ys b/yosys/bbdd_synth_muxxor.ys index ef5cbf0..8c44d05 100644 --- a/yosys/bbdd_synth_muxxor.ys +++ b/yosys/bbdd_synth_muxxor.ys @@ -1,71 +1,89 @@ ######################### preprocessing ########################################################################### read_verilog {{VERILOG_FILE}} hierarchy -top {{TOP_MODULE}} proc;; opt;;; flatten -noscopeinfo;; opt;;; techmap;; opt;;; splitnets -ports;; opt;;; ########################## write design to a blif file and delete empty line because mockturtle cannot handle that # write_blif {{TEMP_DIR}}/{{BASE_NAME}}.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_golden exec -- sed -i '/^$/d' {{TEMP_DIR}}/{{BASE_NAME}}.blif ########################## execute bbdd pass map the result back to yosys names and rename the module ############# -exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_time.txt ./build/src/convert_bbdd {{CONV_FLAGS}} {{TEMP_DIR}}/{{BASE_NAME}}.blif +exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{CASE_DIR}}/{{BASE_NAME}}_bbdd_time.txt {{CONVERTER}} {{CONV_FLAGS}} {{TEMP_DIR}}/{{BASE_NAME}}.blif read_blif {{TEMP_DIR}}/{{BASE_NAME}}_bbdd.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_bbdd stat {{TOP_MODULE}}_bbdd techmap -map {{TECHMAP_BBDD}} copy {{TOP_MODULE}}_bbdd {{TOP_MODULE}}_sat techmap -map yosys/muxxor_inv_map.v {{TOP_MODULE}}_bbdd techmap -map yosys/muxxor_inv_sat.v {{TOP_MODULE}}_sat opt -full {{TOP_MODULE}}_bbdd opt -full {{TOP_MODULE}}_golden ########################### check equality of the optimization ###################################################### {{SAT}}miter -equiv -make_assert {{TOP_MODULE}}_golden {{TOP_MODULE}}_sat equal {{SAT}}flatten equal {{SAT}}clean equal {{SAT}}opt -full equal;; {{SAT}}techmap equal {{SAT}}sat -prove-asserts -set-init-zero -tempinduct -verify -show-regs -show-inputs -show-outputs -dump_vcd trace.vcd equal ########################### write data without abc pass ############################################################# -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.json stat -json {{TOP_MODULE}}_bbdd -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_ltp.txt ltp {{TOP_MODULE}}_sat -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bbdd.json stat -json {{TOP_MODULE}}_bbdd +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bbdd_ltp.txt ltp {{TOP_MODULE}}_sat +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden + +########################### make the liberty cells known ############################################################ +# blackbox the liberty cells so ltp knows their ports (else length=0) +read_liberty -lib {{LIBERTY_FILE}} ########################### abc pass for the golden solution ######################################################## copy {{TOP_MODULE}}_golden {{TOP_MODULE}}_golden_abc abc -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_golden_abc ########################### abc pass for the optimization solution ################################################# copy {{TOP_MODULE}}_bbdd {{TOP_MODULE}}_bbdd_abc abc -D 100 -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_bbdd_abc #print stats to file -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.json stat -json {{TOP_MODULE}}_bbdd -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_abc.json stat -json {{TOP_MODULE}}_bbdd_abc -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bbdd.json stat -json {{TOP_MODULE}}_bbdd +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bbdd_abc.json stat -json {{TOP_MODULE}}_bbdd_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_abc_ltp.txt ltp {{TOP_MODULE}}_golden_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc -########################### write abc blif and verilog ############################################################# -write_blif -top {{TOP_MODULE}}_bbdd_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_abc.blif -write_blif -top {{TOP_MODULE}}_bbdd {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.blif -write_blif -top {{TOP_MODULE}}_golden_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.blif -write_blif -top {{TOP_MODULE}}_golden {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.blif -select {{TOP_MODULE}}_bbdd_abc -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd_abc.v -select {{TOP_MODULE}}_bbdd -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bbdd.v -select {{TOP_MODULE}}_golden_abc -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.v +########################### write one netlist per file ############################################################# +# write_blif has no -selected: isolate each module on a copy. `equal` exists +# only with SAT. + +design -push-copy +delete {{TOP_MODULE}}_golden_abc {{TOP_MODULE}}_bbdd {{TOP_MODULE}}_bbdd_abc {{TOP_MODULE}}_sat +{{SAT}}delete equal +write_blif -top {{TOP_MODULE}}_golden {{CASE_DIR}}/{{BASE_NAME}}_golden.blif select {{TOP_MODULE}}_golden -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.v +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_golden.v +design -pop +design -push-copy +delete {{TOP_MODULE}}_golden {{TOP_MODULE}}_bbdd {{TOP_MODULE}}_bbdd_abc {{TOP_MODULE}}_sat +{{SAT}}delete equal +write_blif -top {{TOP_MODULE}}_golden_abc {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.blif +select {{TOP_MODULE}}_golden_abc +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.v +design -pop + +design -push-copy +delete {{TOP_MODULE}}_golden {{TOP_MODULE}}_golden_abc {{TOP_MODULE}}_bbdd_abc {{TOP_MODULE}}_sat +{{SAT}}delete equal +write_blif -top {{TOP_MODULE}}_bbdd {{CASE_DIR}}/{{BASE_NAME}}_bbdd.blif +select {{TOP_MODULE}}_bbdd +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_bbdd.v +design -pop diff --git a/yosys/bdd_synth.ys b/yosys/bdd_synth.ys index e263356..ce67694 100644 --- a/yosys/bdd_synth.ys +++ b/yosys/bdd_synth.ys @@ -1,66 +1,81 @@ ######################### preprocessing ########################################################################### read_verilog {{VERILOG_FILE}} hierarchy -top {{TOP_MODULE}} proc;; opt;;; flatten -noscopeinfo;; opt;;; techmap;; opt;;; splitnets -ports;; opt;;; ########################## write design to a blif file and delete empty line because mockturtle cannot handle that # write_blif {{TEMP_DIR}}/{{BASE_NAME}}.blif exec -- sed -i '/^$/d' {{TEMP_DIR}}/{{BASE_NAME}}.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_golden -########################## execute bdd pass map the result back to yosys names and rename the module ############# -exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd_time.txt ./build/src/convert_bdd {{TEMP_DIR}}/{{BASE_NAME}}.blif +########################## execute bdd pass, map the result back and rename the module ############################ +exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{CASE_DIR}}/{{BASE_NAME}}_bdd_time.txt {{CONVERTER}} {{CONV_FLAGS}} {{TEMP_DIR}}/{{BASE_NAME}}.blif read_blif {{TEMP_DIR}}/{{BASE_NAME}}_bdd.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_bdd -techmap -map {{TECHMAP_BBDD}} {{BASE_NAME}}_bdd -stat {{BASE_NAME}}_bdd +techmap -map {{TECHMAP_BBDD}} {{TOP_MODULE}}_bdd opt {{TOP_MODULE}}_bdd -stat {{BASE_NAME}}_bdd opt -full {{TOP_MODULE}}_golden ########################### check equality of the optimization ###################################################### {{SAT}}miter -equiv -make_assert {{TOP_MODULE}}_golden {{TOP_MODULE}}_bdd equal {{SAT}}flatten equal {{SAT}}clean equal {{SAT}}opt -full equal;; {{SAT}}techmap equal {{SAT}}sat -prove-asserts -set-init-zero -tempinduct -verify -show-regs -show-inputs -show-outputs -dump_vcd trace.vcd equal -########################### write stats without abc pass ############################################################# -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd.json stat -json {{TOP_MODULE}}_bdd -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd_ltp.txt ltp {{TOP_MODULE}}_bdd -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden +########################### stats without abc pass ################################################################## +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bdd.json stat -json {{TOP_MODULE}}_bdd +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bdd_ltp.txt ltp {{TOP_MODULE}}_bdd +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden -########################### write netlists without abc pass ############################################################# -write_blif -top {{TOP_MODULE}}_bdd {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd.blif -write_blif -top {{TOP_MODULE}}_golden {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.blif -select {{TOP_MODULE}}_bdd -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd.v -select {{TOP_MODULE}}_golden -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.v +########################### make the liberty cells known ############################################################ +# blackbox the liberty cells so ltp knows their ports (else length=0) +read_liberty -lib {{LIBERTY_FILE}} ########################### abc pass for the golden solution ######################################################## copy {{TOP_MODULE}}_golden {{TOP_MODULE}}_golden_abc abc -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_golden_abc -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_abc_ltp.txt ltp {{TOP_MODULE}}_golden_abc ########################### abc pass for the optimization solution ################################################# copy {{TOP_MODULE}}_bdd {{TOP_MODULE}}_bdd_abc -abc -liberty {{LIBERTY_FILE}} -script "+attach" -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd_abc.json stat -json {{TOP_MODULE}}_bdd_abc +abc -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_bdd_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_bdd_abc.json stat -json {{TOP_MODULE}}_bdd_abc -########################### write abc blif and verilog ############################################################# -write_blif -top {{TOP_MODULE}}_bdd_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd_abc.blif -write_blif -top {{TOP_MODULE}}_golden_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.blif -select {{TOP_MODULE}}_bdd_abc -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_bdd_abc.v +########################### write one netlist per file ############################################################# +# write_blif has no -selected: isolate each module on a copy. `equal` exists +# only with SAT. + +design -push-copy +delete {{TOP_MODULE}}_golden_abc {{TOP_MODULE}}_bdd {{TOP_MODULE}}_bdd_abc +{{SAT}}delete equal +write_blif -top {{TOP_MODULE}}_golden {{CASE_DIR}}/{{BASE_NAME}}_golden.blif +select {{TOP_MODULE}}_golden +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_golden.v +design -pop + +design -push-copy +delete {{TOP_MODULE}}_golden {{TOP_MODULE}}_bdd {{TOP_MODULE}}_bdd_abc +{{SAT}}delete equal +write_blif -top {{TOP_MODULE}}_golden_abc {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.blif select {{TOP_MODULE}}_golden_abc -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.v +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.v +design -pop + +design -push-copy +delete {{TOP_MODULE}}_golden {{TOP_MODULE}}_golden_abc {{TOP_MODULE}}_bdd_abc +{{SAT}}delete equal +write_blif -top {{TOP_MODULE}}_bdd {{CASE_DIR}}/{{BASE_NAME}}_bdd.blif +select {{TOP_MODULE}}_bdd +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_bdd.v +design -pop diff --git a/yosys/muxig_synth.ys b/yosys/muxig_synth.ys index 89236f6..41c8793 100644 --- a/yosys/muxig_synth.ys +++ b/yosys/muxig_synth.ys @@ -1,65 +1,65 @@ ######################### preprocessing ########################################################################### read_verilog {{VERILOG_FILE}} hierarchy -top {{TOP_MODULE}} proc;; opt;;; flatten -noscopeinfo;; opt;;; techmap;; opt;;; splitnets -ports;; opt;;; ########################## write design to a blif file and delete empty line because mockturtle cannot handle that # write_blif {{TEMP_DIR}}/{{BASE_NAME}}.blif exec -- sed -i '/^$/d' {{TEMP_DIR}}/{{BASE_NAME}}.blif rename {{TOP_MODULE}} {{TOP_MODULE}}_golden ########################## execute muxig pass map the result back to yosys names and rename the module ############# -exec -- time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig_time.txt ./build/src/convert_muxig_opt -o {{OUT_DIR}}/{{BASE_NAME}} {{TEMP_DIR}}/{{BASE_NAME}}.blif -exec -- python ./yosys/map_ports.py {{TEMP_DIR}}/{{BASE_NAME}}.blif {{TEMP_DIR}}/{{BASE_NAME}}_muxig_temp.blif +exec -- timeout {{TIMEOUT}} time -f "\nTime: %E\nCPU: %P\nMemory: %M KB" -o {{CASE_DIR}}/{{BASE_NAME}}_muxig_time.txt {{CONVERTER}} {{CONV_FLAGS}} {{TEMP_DIR}}/{{BASE_NAME}}.blif +exec -- python3 ./yosys/map_ports.py {{TEMP_DIR}}/{{BASE_NAME}}.blif {{TEMP_DIR}}/{{BASE_NAME}}_muxig_temp.blif read_blif {{TEMP_DIR}}/{{BASE_NAME}}_muxig.blif rename top {{TOP_MODULE}}_muxig copy {{TOP_MODULE}}_muxig {{TOP_MODULE}}_muxig_sat ########################## read back the optimization and map it back to yosys internal gates ####################### techmap -map yosys/mockturtle_map.v {{TOP_MODULE}}_muxig techmap {{TOP_MODULE}}_muxig opt {{TOP_MODULE}}_muxig ########################### check equality of the optimization ###################################################### -{{SAT}}techmap -map yosys/mockturtle_map.v {{BASE_NAME}}_muxig_sat -{{SAT}}techmap {{BASE_NAME}}_muxig_sat +{{SAT}}techmap -map yosys/mockturtle_map.v {{TOP_MODULE}}_muxig_sat +{{SAT}}techmap {{TOP_MODULE}}_muxig_sat {{SAT}}miter -equiv -make_assert {{TOP_MODULE}}_golden {{TOP_MODULE}}_muxig_sat equal {{SAT}}flatten equal {{SAT}}clean equal {{SAT}}opt -full equal {{SAT}}techmap equal {{SAT}}sat -prove-asserts -set-init-zero -tempinduct -verify -show-regs -show-inputs -show-outputs -dump_vcd trace.vcd equal ########################### write data without abc pass ############################################################# -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig.json stat -json {{TOP_MODULE}}_muxig -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig_ltp.txt ltp {{TOP_MODULE}}_muxig -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden +tee -o {{CASE_DIR}}/{{BASE_NAME}}_muxig.json stat -json {{TOP_MODULE}}_muxig +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden.json stat -json {{TOP_MODULE}}_golden +tee -o {{CASE_DIR}}/{{BASE_NAME}}_muxig_ltp.txt ltp {{TOP_MODULE}}_muxig +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_ltp.txt ltp {{TOP_MODULE}}_golden ########################### abc pass for the golden solution ######################################################## copy {{TOP_MODULE}}_golden {{TOP_MODULE}}_golden_abc abc -liberty {{LIBERTY_FILE}} {{TOP_MODULE}}_golden_abc -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.json stat -json {{TOP_MODULE}}_golden_abc ########################### abc pass for the optimization solution ################################################# copy {{TOP_MODULE}}_muxig {{TOP_MODULE}}_muxig_abc -abc -liberty {{LIBERTY_FILE}} -script "+attach" -tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig_abc.json stat -json {{TOP_MODULE}}_muxig_abc +abc -liberty {{LIBERTY_FILE}} -script "+attach" {{TOP_MODULE}}_muxig_abc +tee -o {{CASE_DIR}}/{{BASE_NAME}}_muxig_abc.json stat -json {{TOP_MODULE}}_muxig_abc ########################### write abc blif and verilog ############################################################# -write_blif -top {{TOP_MODULE}}_muxig_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig_abc.blif -write_blif -top {{TOP_MODULE}}_golden_abc {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.blif +write_blif -top {{TOP_MODULE}}_muxig_abc {{CASE_DIR}}/{{BASE_NAME}}_muxig_abc.blif +write_blif -top {{TOP_MODULE}}_golden_abc {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.blif select {{TOP_MODULE}}_muxig_abc -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig_abc.v +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_muxig_abc.v select {{TOP_MODULE}}_golden_abc -write_verilog -selected {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_golden_abc.v +write_verilog -selected {{CASE_DIR}}/{{BASE_NAME}}_golden_abc.v ### this does not work for now so it is not considered -#tee -o {{OUT_DIR}}/{{BASE_NAME}}/{{BASE_NAME}}_muxig_abc_ltp.txt ltp {{TOP_MODULE}}_muxig_abc +#tee -o {{CASE_DIR}}/{{BASE_NAME}}_muxig_abc_ltp.txt ltp {{TOP_MODULE}}_muxig_abc