Page MenuHomePhorge
Files F27033068

convert_bdd.cpp
No OneTemporary
Actions

Authored By
Unknown
Size
4 KB
Referenced Files
None
Subscribers
None

convert_bdd.cpp
View Options

// Copyright 2025 Oliver Theimer
#include <algorithm>
#include <cstdlib>
#include <filesystem>
#include <iostream>
#include <string>
#include <vector>
#include <cstdio>
#include <lorina/diagnostics.hpp>
#include <lorina/lorina.hpp>
#include <mockturtle/algorithms/cover_to_graph.hpp>
#include <mockturtle/mockturtle.hpp>
#include "bdd.h"
#include "mockturtle/io/write_blif.hpp"
#include "mockturtle/networks/cover.hpp"
#include "util/cover_to_bdd.hpp"
int write_blif_recursive(std::ofstream &blif_file, cover_network cover,
const BDD &node, int next_index, bool output) {
if (node < 2) {
return node;
}
int low_out =
write_blif_recursive(blif_file, cover, bdd_low(node), next_index, false);
int high_out = write_blif_recursive(blif_file, cover, bdd_high(node),
next_index++, false);
blif_file << ".names " << cover.signal_map[bdd_var(node)] << " ";
if (IS_TERM(low_out)) {
if (low_out == 0) {
blif_file << "$false ";
} else {
blif_file << "$true ";
}
} else {
blif_file << std::to_string(low_out);
}
blif_file << " ";
if (IS_TERM(high_out)) {
if (high_out == 0) {
blif_file << "$false ";
} else {
blif_file << "$true ";
}
} else {
blif_file << std::to_string(high_out) << " ";
}
/*blif_file << std::format(
".names {} {} {} {}", cover.signal_map[bdd_var(node)],
IS_TERM(low_out) ? (low_out == 0 ? "$false" : "$true")
: std::to_string(low_out),
IS_TERM(high_out) ? (high_out == 0 ? "$false" : "$true")
: std::to_string(high_out),
!output ? std::to_string(node) : "");*/
if (!output) {
blif_file << std::to_string(node);
blif_file << "\n0-1 1\n11- 1\n";
}
return node;
}
void write_blif(std::string filename, mockturtle::cover_network cover,
std::vector<std::pair<bdd, std::string>> output_map) {
std::ofstream blif_file(filename);
blif_file << ".model " + cover.get_module_name() + "\n";
blif_file << ".inputs";
for (unsigned int i = 0; i < cover.signal_map.size(); i++) {
blif_file << " " << cover.signal_map[i];
if (i + 1 == cover._storage->inputs.size()) {
blif_file << "\n.outputs";
}
}
blif_file << "\n.names $true\n1\n";
blif_file << ".names $false\n";
int next_index = cover._storage->inputs.size() + 1;
for (std::pair<bdd, std::string> out_map : output_map) {
if (out_map.first == bdd_true()) {
blif_file << ".names " << out_map.second << "\n1\n";
} else if (out_map.first == bdd_false()) {
blif_file << ".names " << out_map.second << "\n0\n";
} else {
write_blif_recursive(blif_file, cover, out_map.first.id(), next_index,
true);
blif_file << out_map.second << "\n0-1 1\n11- 1\n";
}
}
blif_file << ".end\n";
}
int get_bdd_height(BDD node) {
if (node < 2) {
return 0;
}
int low_height = get_bdd_height(bdd_low(node));
int high_height = get_bdd_height(bdd_high(node));
return std::max(low_height, high_height) + 1;
}
int get_total_height(std::vector<std::pair<bdd, std::string>> output_map) {
int max_height = -1;
for (std::pair<bdd, std::string> out_map : output_map) {
int current_height = get_bdd_height(out_map.first.id());
if (current_height > max_height) {
max_height = current_height;
}
}
return max_height;
}
int main(int argc, char *argv[]) {
if (optind >= argc) {
std::cout << "[ERROR] input file in blif format is missing\n";
std::cerr << "[INFO] Usage: " << argv[0] << " <blif-file>" << std::endl;
return EXIT_FAILURE;
}
std::string benchmark(argv[optind]);
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;
// lorina::diagnostic_engine diag;
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::vector<std::pair<bdd, std::string>> output_map;
bdd_init(300000, 10000);
bdd_setvarnum(cover._storage->inputs.size());
bdd_autoreorder(BDD_REORDER_SIFT);
printf("[INFO] init with %zu variables\n", cover._storage->inputs.size());
cover_to_bdd(cover, output_map);
// bdd_reorder_siftite is the same but repeats until no more progress is done
bdd_reorder(BDD_REORDER_SIFT);
printf("height after: %d\n", get_total_height(output_map));
write_blif("temp/" + base_name + "_bdd.blif", cover, output_map);
bdd_done();
return EXIT_SUCCESS;
}

File Metadata

Mime Type
text/x-c
Expires
Tue, Oct 27, 3:40 PM (23 h, 58 m)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
405749
Default Alt Text
convert_bdd.cpp (4 KB)

Event Timeline