Skip to content

Commit

Permalink
✨ Simulate node truth tables (#49)
Browse files Browse the repository at this point in the history
* ✨ Exposed further truth table operators and functions

* ✨ Exposed node simulation

* 👷 Added Python 3.13 to the `noxfile.py` configuration

* 📝 Mention the new functions in the README
  • Loading branch information
marcelwa authored Dec 12, 2024
1 parent 97c67fe commit d3e8d1a
Show file tree
Hide file tree
Showing 10 changed files with 311 additions and 52 deletions.
9 changes: 8 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -226,14 +226,21 @@ print(tt.is_const0())
#### Symbolic Simulation of AIGs

```python
from aigverse import simulate
from aigverse import simulate, simulate_nodes

# Obtain the truth table of each AIG output
tts = simulate(aig)

# Print the truth tables
for i, tt in enumerate(tts):
print(f"PO{i}: {tt.to_binary()}")

# Obtain the truth tables of each node in the AIG
n_to_tt = simulate_nodes(aig)

# Print the truth tables of each node
for node, tt in n_to_tt.items():
print(f"Node {node}: {tt.to_binary()}")
```

#### Exporting as Lists of Lists
Expand Down
8 changes: 8 additions & 0 deletions bindings/aigverse/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,15 @@
TruthTable,
aig_cut_rewriting,
aig_resubstitution,
cofactor0,
cofactor1,
equivalence_checking,
read_aiger_into_aig,
read_ascii_aiger_into_aig,
simulate,
simulate_nodes,
sop_refactoring,
ternary_majority,
to_edge_list,
write_aiger,
)
Expand All @@ -31,11 +35,15 @@
"__version__",
"aig_cut_rewriting",
"aig_resubstitution",
"cofactor0",
"cofactor1",
"equivalence_checking",
"read_aiger_into_aig",
"read_ascii_aiger_into_aig",
"simulate",
"simulate_nodes",
"sop_refactoring",
"ternary_majority",
"to_edge_list",
"write_aiger",
]
2 changes: 2 additions & 0 deletions bindings/aigverse/aigverse.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
#include "aigverse/io/read_aiger.hpp"
#include "aigverse/io/write_aiger.hpp"
#include "aigverse/networks/logic_networks.hpp"
#include "aigverse/truth_tables/operations.hpp"
#include "aigverse/truth_tables/truth_table.hpp"

#include <pybind11/pybind11.h>
Expand All @@ -31,6 +32,7 @@ PYBIND11_MODULE(pyaigverse, m, pybind11::mod_gil_not_used())
* Truth tables.
*/
aigverse::truth_tables(m);
aigverse::truth_table_operations(m);

/**
* Algorithms
Expand Down
35 changes: 33 additions & 2 deletions bindings/aigverse/include/aigverse/algorithms/simulation.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,14 @@

#include "aigverse/types.hpp"

#include <kitty/dynamic_truth_table.hpp>
#include <mockturtle/algorithms/simulation.hpp>
#include <pybind11/pybind11.h>
#include <pybind11/stl.h>

#include <iostream>
#include <new>
#include <unordered_map>
#include <vector>

namespace aigverse
Expand Down Expand Up @@ -50,9 +52,38 @@ void simulation(pybind11::module& m)
throw;
}
},
"network"_a)
"network"_a);

;
m.def(
"simulate_nodes",
[](const Ntk& ntk) -> std::unordered_map<uint64_t, kitty::dynamic_truth_table>
{
if (ntk.num_pis() > 16)
{
std::cout << "[w] trying to simulate a network with more than 16 inputs; this might take while and "
"potentially cause memory issues\n";
}

try
{
const auto n_map = mockturtle::simulate_nodes<kitty::dynamic_truth_table>(
ntk,
// NOLINTNEXTLINE
mockturtle::default_simulator<kitty::dynamic_truth_table>{static_cast<unsigned>(ntk.num_pis())});

std::unordered_map<mockturtle::node<Ntk>, kitty::dynamic_truth_table> node_to_tt{};

// convert vector implementation to unordered_map
ntk.foreach_node([&n_map, &node_to_tt](const auto& n) { node_to_tt[n] = n_map[n]; });
return node_to_tt;
}
catch (const std::bad_alloc&)
{
std::cout << "[e] network has too many inputs to store its truth table; out of memory!\n";
throw;
}
},
"network"_a);
}

} // namespace detail
Expand Down
49 changes: 49 additions & 0 deletions bindings/aigverse/include/aigverse/truth_tables/operations.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
//
// Created by marcel on 12.12.24.
//

#ifndef AIGVERSE_OPERATIONS_HPP
#define AIGVERSE_OPERATIONS_HPP

#include "aigverse/types.hpp"

#include <kitty/dynamic_truth_table.hpp>
#include <kitty/operations.hpp>
#include <pybind11/pybind11.h>

namespace aigverse
{

namespace detail
{

inline void truth_table_operations(pybind11::module& m)
{
using namespace pybind11::literals;

m.def(
"ternary_majority",
[](const aigverse::truth_table& a, const aigverse::truth_table& b,
const aigverse::truth_table& c) -> aigverse::truth_table { return kitty::ternary_majority(a, b, c); },
"a"_a, "b"_a, "c"_a, "Compute the ternary majority of three truth tables.");

m.def(
"cofactor0", [](const aigverse::truth_table& tt, const uint8_t var_index) -> aigverse::truth_table
{ return kitty::cofactor0(tt, var_index); },
"Returns the cofactor with respect to 0 of the variable at index `var_index` in the given truth table.");
m.def(
"cofactor1", [](const aigverse::truth_table& tt, const uint8_t var_index) -> aigverse::truth_table
{ return kitty::cofactor1(tt, var_index); },
"Returns the cofactor with respect to 1 of the variable at index `var_index` in the given truth table.");
}

} // namespace detail

inline void truth_table_operations(pybind11::module& m)
{
detail::truth_table_operations(m);
}

} // namespace aigverse

#endif // AIGVERSE_OPERATIONS_HPP
76 changes: 41 additions & 35 deletions bindings/aigverse/include/aigverse/truth_tables/truth_table.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,7 @@ inline void truth_tables(pybind11::module& m)
namespace py = pybind11;
using namespace pybind11::literals;

using dyn_tt = kitty::dynamic_truth_table;

py::class_<dyn_tt>(m, "TruthTable")
py::class_<aigverse::truth_table>(m, "TruthTable")
.def(py::init<>(), "Create an empty TruthTable with 0 variables.")
.def(py::init<uint32_t>(), "num_vars"_a,
"Create a TruthTable with 'num_vars' variables with all bits set to 0.")
Expand All @@ -40,47 +38,52 @@ inline void truth_tables(pybind11::module& m)
.def(py::self == py::self, "other"_a)
.def(py::self != py::self, "other"_a)
.def(py::self < py::self, "other"_a)
.def(py::self & py::self, "other"_a)
.def(py::self | py::self, "other"_a)
.def(py::self ^ py::self, "other"_a)
.def(~py::self)

// Method bindings
.def("num_vars", &dyn_tt::num_vars, "Returns the number of variables.")
.def("num_blocks", &dyn_tt::num_blocks, "Returns the number of blocks.")
.def("num_bits", &dyn_tt::num_bits, "Returns the number of bits.")
.def("num_vars", &aigverse::truth_table::num_vars, "Returns the number of variables.")
.def("num_blocks", &aigverse::truth_table::num_blocks, "Returns the number of blocks.")
.def("num_bits", &aigverse::truth_table::num_bits, "Returns the number of bits.")

// Operator= for assigning other truth tables
.def(
"__copy__", [](const dyn_tt& self) -> dyn_tt { return self; }, "Returns a shallow copy of the truth table.")
"__copy__", [](const aigverse::truth_table& self) -> aigverse::truth_table { return self; },
"Returns a shallow copy of the truth table.")
.def(
"__deepcopy__", [](const dyn_tt& self, [[maybe_unused]] py::dict&) -> dyn_tt { return self; },
"Returns a deep copy of the truth table.")
"__deepcopy__", [](const aigverse::truth_table& self, [[maybe_unused]] py::dict&) -> aigverse::truth_table
{ return self; }, "Returns a deep copy of the truth table.")
.def(
"__assign__", [](dyn_tt& self, const dyn_tt& other) -> dyn_tt { return self = other; }, "other"_a,
"Assigns the truth table from another compatible truth table.")
"__assign__", [](aigverse::truth_table& self, const aigverse::truth_table& other) -> aigverse::truth_table
{ return self = other; }, "other"_a, "Assigns the truth table from another compatible truth table.")

// Hashing
.def(
"__hash__", [](const dyn_tt& self) { return kitty::hash<dyn_tt>{}(self); },
"__hash__", [](const aigverse::truth_table& self) { return kitty::hash<aigverse::truth_table>{}(self); },
"Returns the hash of the truth table.")

// Free functions added to the class for convenience
.def(
"set_bit", [](dyn_tt& self, const uint64_t index) -> void { kitty::set_bit(self, index); }, "index"_a,
"Sets the bit at the given index.")
"set_bit", [](aigverse::truth_table& self, const uint64_t index) -> void { kitty::set_bit(self, index); },
"index"_a, "Sets the bit at the given index.")
.def(
"get_bit", [](const dyn_tt& self, const uint64_t index) -> bool { return kitty::get_bit(self, index); },
"index"_a, "Returns the bit at the given index.")
"get_bit", [](const aigverse::truth_table& self, const uint64_t index) -> bool
{ return kitty::get_bit(self, index); }, "index"_a, "Returns the bit at the given index.")
.def(
"clear_bit", [](dyn_tt& self, const uint64_t index) -> void { kitty::clear_bit(self, index); }, "index"_a,
"Clears the bit at the given index.")
"clear_bit", [](aigverse::truth_table& self, const uint64_t index) -> void
{ kitty::clear_bit(self, index); }, "index"_a, "Clears the bit at the given index.")
.def(
"flip_bit", [](dyn_tt& self, const uint64_t index) -> void { kitty::flip_bit(self, index); }, "index"_a,
"Flips the bit at the given index.")
"flip_bit", [](aigverse::truth_table& self, const uint64_t index) -> void { kitty::flip_bit(self, index); },
"index"_a, "Flips the bit at the given index.")
.def(
"get_block", [](const dyn_tt& self, const uint64_t block_index) -> uint64_t
"get_block", [](const aigverse::truth_table& self, const uint64_t block_index) -> uint64_t
{ return kitty::get_block(self, block_index); }, "block_index"_a, "Returns a block of bits vector.")

.def(
"create_nth_var",
[](dyn_tt& self, const uint8_t var_index, const bool complement = false) -> void
[](aigverse::truth_table& self, const uint8_t var_index, const bool complement = false) -> void
{
if (var_index >= self.num_vars())
{
Expand All @@ -95,7 +98,7 @@ inline void truth_tables(pybind11::module& m)
"than the truth table's number of variables.")
.def(
"create_from_binary_string",
[](dyn_tt& self, const std::string& binary) -> void
[](aigverse::truth_table& self, const std::string& binary) -> void
{
if (binary.size() != self.num_bits())
{
Expand All @@ -113,7 +116,7 @@ inline void truth_tables(pybind11::module& m)

.def(
"create_from_hex_string",
[](dyn_tt& self, const std::string& hexadecimal) -> void
[](aigverse::truth_table& self, const std::string& hexadecimal) -> void
{
if (self.num_vars() < 2)
{
Expand All @@ -139,29 +142,32 @@ inline void truth_tables(pybind11::module& m)
"function is represented by the binary string 'E8' or 'e8'. The number of characters in 'hex' "
"must be one fourth the number of bits in the truth table.")
.def(
"create_random", [](dyn_tt& self) -> void { kitty::create_random(self); },
"create_random", [](aigverse::truth_table& self) -> void { kitty::create_random(self); },
"Constructs a random truth table.")
.def(
"create_majority", [](aigverse::truth_table& self) -> void { kitty::create_majority(self); },
"Constructs a MAJ truth table.")

.def("clear", &kitty::clear<dyn_tt>, "Clears all bits.")
.def("clear", &kitty::clear<aigverse::truth_table>, "Clears all bits.")

.def("count_ones", &kitty::count_ones<dyn_tt>, "Counts ones in truth table.")
.def("count_zeroes", &kitty::count_zeros<dyn_tt>, "Counts zeroes in truth table.")
.def("count_ones", &kitty::count_ones<aigverse::truth_table>, "Counts ones in truth table.")
.def("count_zeroes", &kitty::count_zeros<aigverse::truth_table>, "Counts zeroes in truth table.")

.def(
"is_const0", [](const dyn_tt& self) -> bool { return kitty::is_const0(self); },
"is_const0", [](const aigverse::truth_table& self) -> bool { return kitty::is_const0(self); },
"Checks if the truth table is constant 0.")
.def(
"is_const1", [](const dyn_tt& self) -> bool { return kitty::is_const0(kitty::unary_not(self)); },
"Checks if the truth table is constant 1.")
"is_const1", [](const aigverse::truth_table& self) -> bool
{ return kitty::is_const0(kitty::unary_not(self)); }, "Checks if the truth table is constant 1.")

// Representations
.def(
"__repr__",
[](const dyn_tt& self) -> std::string { return fmt::format("TruthTable <vars={}>", self.num_vars()); },
"__repr__", [](const aigverse::truth_table& self) -> std::string
{ return fmt::format("TruthTable <vars={}>", self.num_vars()); },
"Returns an abstract string representation of the truth table.")
.def(
"to_binary",
[](const dyn_tt& self) -> std::string
[](const aigverse::truth_table& self) -> std::string
{
std::stringstream stream{};
kitty::print_binary(self, stream);
Expand All @@ -171,7 +177,7 @@ inline void truth_tables(pybind11::module& m)
"Returns the truth table as a string in binary representation.")
.def(
"to_hex",
[](const dyn_tt& self) -> std::string
[](const aigverse::truth_table& self) -> std::string
{
std::stringstream stream{};
kitty::print_hex(self, stream);
Expand Down
9 changes: 9 additions & 0 deletions bindings/aigverse/pyaigverse.pyi
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,10 @@ class TruthTable:
def __eq__(self, other: object) -> bool: ...
def __ne__(self, other: object) -> bool: ...
def __lt__(self, other: TruthTable) -> bool: ...
def __and__(self, other: TruthTable) -> TruthTable: ...
def __or__(self, other: TruthTable) -> TruthTable: ...
def __xor__(self, other: TruthTable) -> TruthTable: ...
def __invert__(self) -> TruthTable: ...
def num_vars(self) -> int: ...
def num_blocks(self) -> int: ...
def num_bits(self) -> int: ...
Expand All @@ -147,6 +151,7 @@ class TruthTable:
def create_from_binary_string(self, binary: str) -> None: ...
def create_from_hex_string(self, hexadecimal: str) -> None: ...
def create_random(self) -> None: ...
def create_majority(self) -> None: ...
def clear(self) -> None: ...
def count_ones(self) -> int: ...
def count_zeroes(self) -> int: ...
Expand All @@ -155,6 +160,9 @@ class TruthTable:
def to_binary(self) -> str: ...
def to_hex(self) -> str: ...

def ternary_majority(a: TruthTable, b: TruthTable, c: TruthTable) -> TruthTable: ...
def cofactor0(tt: TruthTable, var_index: int) -> TruthTable: ...
def cofactor1(tt: TruthTable, var_index: int) -> TruthTable: ...
def equivalence_checking(
spec: Aig,
impl: Aig,
Expand Down Expand Up @@ -196,3 +204,4 @@ def aig_cut_rewriting(
very_verbose: bool = False,
) -> None: ...
def simulate(ntk: Aig) -> list[TruthTable]: ...
def simulate_nodes(ntk: Aig) -> dict[int, TruthTable]: ...
Loading

0 comments on commit d3e8d1a

Please sign in to comment.