mirror of https://github.com/llvm/circt.git
[Support] Add NPN class for Boolean function canonicalization (#8747)
This commit introduces NPNClass and BinaryTruthTable classes to the CIRCT Support library for Boolean function equivalence checking and canonicalization. NPNClass computes Negation-Permutation-Negation canonical forms for Boolean functions, enabling efficient detection of functionally equivalent circuits under input/output transformations. BinaryTruthTable provides compact representation using APInt with support for multi-input, multi-output functions. This infrastructure is essential for technology mapping and Boolean function optimization in synthesis flows.
This commit is contained in:
parent
ab7a0a6c85
commit
754f72d04c
|
@ -0,0 +1,166 @@
|
|||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This header file defines NPN (Negation-Permutation-Negation) canonical forms
|
||||
// and binary truth tables for boolean function representation and equivalence
|
||||
// checking in combinational logic optimization.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#ifndef CIRCT_SUPPORT_NPNCLASS_H
|
||||
#define CIRCT_SUPPORT_NPNCLASS_H
|
||||
|
||||
#include "circt/Support/LLVM.h"
|
||||
#include "llvm/ADT/APInt.h"
|
||||
#include "llvm/ADT/ArrayRef.h"
|
||||
#include "llvm/ADT/SmallVector.h"
|
||||
#include "llvm/Support/raw_ostream.h"
|
||||
|
||||
namespace circt {
|
||||
|
||||
/// Represents a boolean function as a truth table.
|
||||
///
|
||||
/// A truth table stores the output values for all possible input combinations
|
||||
/// of a boolean function. For a function with n inputs and m outputs, the
|
||||
/// truth table contains 2^n entries, each with m output bits.
|
||||
///
|
||||
/// Example: For a 2-input AND gate:
|
||||
/// - Input 00 -> Output 0
|
||||
/// - Input 01 -> Output 0
|
||||
/// - Input 10 -> Output 0
|
||||
/// - Input 11 -> Output 1
|
||||
/// This would be stored as the bit pattern 0001 in the truth table.
|
||||
struct BinaryTruthTable {
|
||||
unsigned numInputs; ///< Number of inputs for this boolean function
|
||||
unsigned numOutputs; ///< Number of outputs for this boolean function
|
||||
llvm::APInt table; ///< Truth table data as a packed bit vector
|
||||
|
||||
/// Default constructor creates an empty truth table.
|
||||
BinaryTruthTable() : numInputs(0), numOutputs(0), table(1, 0) {}
|
||||
|
||||
/// Constructor for a truth table with given dimensions and evaluation data.
|
||||
BinaryTruthTable(unsigned numInputs, unsigned numOutputs,
|
||||
const llvm::APInt &table)
|
||||
: numInputs(numInputs), numOutputs(numOutputs), table(table) {
|
||||
assert(table.getBitWidth() == (1u << numInputs) * numOutputs &&
|
||||
"Truth table size mismatch");
|
||||
}
|
||||
|
||||
/// Constructor for a truth table with given dimensions, initialized to zero.
|
||||
BinaryTruthTable(unsigned numInputs, unsigned numOutputs)
|
||||
: numInputs(numInputs), numOutputs(numOutputs),
|
||||
table((1u << numInputs) * numOutputs, 0) {}
|
||||
|
||||
/// Get the output value for a given input combination.
|
||||
llvm::APInt getOutput(const llvm::APInt &input) const;
|
||||
|
||||
/// Set the output value for a given input combination.
|
||||
void setOutput(const llvm::APInt &input, const llvm::APInt &output);
|
||||
|
||||
/// Apply input permutation to create a new truth table.
|
||||
/// This reorders the input variables according to the given permutation.
|
||||
BinaryTruthTable applyPermutation(ArrayRef<unsigned> permutation) const;
|
||||
|
||||
/// Apply input negation to create a new truth table.
|
||||
/// This negates selected input variables based on the mask.
|
||||
BinaryTruthTable applyInputNegation(unsigned mask) const;
|
||||
|
||||
/// Apply output negation to create a new truth table.
|
||||
/// This negates selected output variables based on the mask.
|
||||
BinaryTruthTable applyOutputNegation(unsigned negation) const;
|
||||
|
||||
/// Check if this truth table is lexicographically smaller than another.
|
||||
/// Used for canonical ordering of truth tables.
|
||||
bool isLexicographicallySmaller(const BinaryTruthTable &other) const;
|
||||
|
||||
/// Equality comparison for truth tables.
|
||||
bool operator==(const BinaryTruthTable &other) const;
|
||||
|
||||
/// Debug dump method for truth tables.
|
||||
void dump(llvm::raw_ostream &os = llvm::errs()) const;
|
||||
};
|
||||
|
||||
/// Represents the canonical form of a boolean function under NPN equivalence.
|
||||
///
|
||||
/// NPN (Negation-Permutation-Negation) equivalence considers two boolean
|
||||
/// functions equivalent if one can be obtained from the other by:
|
||||
/// 1. Negating some inputs (pre-negation)
|
||||
/// 2. Permuting the inputs
|
||||
/// 3. Negating some outputs (post-negation)
|
||||
///
|
||||
/// Example: The function ab+c is NPN equivalent to !a + b(!c) since we can
|
||||
/// transform the first function into the second by negating inputs 'a' and 'c',
|
||||
/// then reordering the inputs appropriately.
|
||||
///
|
||||
/// This canonical form is used to efficiently match cuts against library
|
||||
/// patterns, as functions in the same NPN class can be implemented by the
|
||||
/// same circuit with appropriate input/output inversions.
|
||||
struct NPNClass {
|
||||
BinaryTruthTable truthTable; ///< Canonical truth table
|
||||
llvm::SmallVector<unsigned> inputPermutation; ///< Input permutation applied
|
||||
unsigned inputNegation = 0; ///< Input negation mask
|
||||
unsigned outputNegation = 0; ///< Output negation mask
|
||||
|
||||
/// Default constructor creates an empty NPN class.
|
||||
NPNClass() = default;
|
||||
|
||||
/// Constructor from a truth table.
|
||||
NPNClass(const BinaryTruthTable &tt) : truthTable(tt) {}
|
||||
|
||||
NPNClass(const BinaryTruthTable &tt, llvm::SmallVector<unsigned> inputPerm,
|
||||
unsigned inputNeg, unsigned outputNeg)
|
||||
: truthTable(tt), inputPermutation(std::move(inputPerm)),
|
||||
inputNegation(inputNeg), outputNegation(outputNeg) {}
|
||||
|
||||
/// Compute the canonical NPN form for a given truth table.
|
||||
///
|
||||
/// This method exhaustively tries all possible input permutations and
|
||||
/// negations to find the lexicographically smallest canonical form.
|
||||
///
|
||||
/// FIXME: Currently we are using exact canonicalization which doesn't scale
|
||||
/// well. For larger truth tables, semi-canonical forms should be used
|
||||
/// instead.
|
||||
static NPNClass computeNPNCanonicalForm(const BinaryTruthTable &tt);
|
||||
|
||||
/// Get input permutation from this NPN class to another equivalent NPN class.
|
||||
///
|
||||
/// When two NPN classes are equivalent, they may have different input
|
||||
/// permutations. This function computes a permutation that allows
|
||||
/// transforming input indices from the target NPN class to input indices of
|
||||
/// this NPN class.
|
||||
///
|
||||
/// Returns a permutation vector where result[i] gives the input index in this
|
||||
/// NPN class that corresponds to input i in the target NPN class.
|
||||
///
|
||||
/// Example: If this has permutation [2,0,1] and target has [1,2,0],
|
||||
/// the mapping allows connecting target inputs to this inputs correctly.
|
||||
void getInputPermutation(const NPNClass &targetNPN,
|
||||
llvm::SmallVectorImpl<unsigned> &permutation) const;
|
||||
|
||||
/// Equality comparison for NPN classes.
|
||||
bool equivalentOtherThanPermutation(const NPNClass &other) const {
|
||||
return truthTable == other.truthTable &&
|
||||
inputNegation == other.inputNegation &&
|
||||
outputNegation == other.outputNegation;
|
||||
}
|
||||
|
||||
bool isLexicographicallySmaller(const NPNClass &other) const {
|
||||
if (truthTable.table != other.truthTable.table)
|
||||
return truthTable.isLexicographicallySmaller(other.truthTable);
|
||||
if (inputNegation != other.inputNegation)
|
||||
return inputNegation < other.inputNegation;
|
||||
return outputNegation < other.outputNegation;
|
||||
}
|
||||
|
||||
/// Debug dump method for NPN classes.
|
||||
void dump(llvm::raw_ostream &os = llvm::errs()) const;
|
||||
};
|
||||
|
||||
} // namespace circt
|
||||
|
||||
#endif // CIRCT_SUPPORT_NPNCLASS_H
|
|
@ -16,6 +16,7 @@ add_circt_library(CIRCTSupport
|
|||
JSON.cpp
|
||||
LoweringOptions.cpp
|
||||
Naming.cpp
|
||||
NPNClass.cpp
|
||||
ParsingUtils.cpp
|
||||
Passes.cpp
|
||||
Path.cpp
|
||||
|
|
|
@ -0,0 +1,274 @@
|
|||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// This file implements NPN (Negation-Permutation-Negation) canonical forms
|
||||
// and binary truth tables for boolean function representation and equivalence
|
||||
// checking in combinational logic optimization.
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Support/NPNClass.h"
|
||||
|
||||
#include "llvm/ADT/STLExtras.h"
|
||||
#include <algorithm>
|
||||
#include <cassert>
|
||||
|
||||
using namespace circt;
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// BinaryTruthTable
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
llvm::APInt BinaryTruthTable::getOutput(const llvm::APInt &input) const {
|
||||
assert(input.getBitWidth() == numInputs && "Input width mismatch");
|
||||
return table.extractBits(numOutputs, input.getZExtValue() * numOutputs);
|
||||
}
|
||||
|
||||
void BinaryTruthTable::setOutput(const llvm::APInt &input,
|
||||
const llvm::APInt &output) {
|
||||
assert(input.getBitWidth() == numInputs && "Input width mismatch");
|
||||
assert(output.getBitWidth() == numOutputs && "Output width mismatch");
|
||||
assert(input.getBitWidth() < 32 && "Input width too large");
|
||||
unsigned offset = input.getZExtValue() * numOutputs;
|
||||
for (unsigned i = 0; i < numOutputs; ++i)
|
||||
table.setBitVal(offset + i, output[i]);
|
||||
}
|
||||
|
||||
BinaryTruthTable
|
||||
BinaryTruthTable::applyPermutation(ArrayRef<unsigned> permutation) const {
|
||||
assert(permutation.size() == numInputs && "Permutation size mismatch");
|
||||
BinaryTruthTable result(numInputs, numOutputs);
|
||||
|
||||
for (unsigned i = 0; i < (1u << numInputs); ++i) {
|
||||
llvm::APInt input(numInputs, i);
|
||||
llvm::APInt permutedInput = input;
|
||||
|
||||
// Apply permutation
|
||||
for (unsigned j = 0; j < numInputs; ++j) {
|
||||
if (permutation[j] != j)
|
||||
permutedInput.setBitVal(j, input[permutation[j]]);
|
||||
}
|
||||
|
||||
result.setOutput(permutedInput, getOutput(input));
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
BinaryTruthTable BinaryTruthTable::applyInputNegation(unsigned mask) const {
|
||||
BinaryTruthTable result(numInputs, numOutputs);
|
||||
|
||||
for (unsigned i = 0; i < (1u << numInputs); ++i) {
|
||||
llvm::APInt input(numInputs, i);
|
||||
|
||||
// Apply negation using bitwise XOR
|
||||
llvm::APInt negatedInput = input ^ llvm::APInt(numInputs, mask);
|
||||
|
||||
result.setOutput(negatedInput, getOutput(input));
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
BinaryTruthTable
|
||||
BinaryTruthTable::applyOutputNegation(unsigned negation) const {
|
||||
BinaryTruthTable result(numInputs, numOutputs);
|
||||
|
||||
for (unsigned i = 0; i < (1u << numInputs); ++i) {
|
||||
llvm::APInt input(numInputs, i);
|
||||
llvm::APInt output = getOutput(input);
|
||||
|
||||
// Apply negation using bitwise XOR
|
||||
llvm::APInt negatedOutput = output ^ llvm::APInt(numOutputs, negation);
|
||||
|
||||
result.setOutput(input, negatedOutput);
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
bool BinaryTruthTable::isLexicographicallySmaller(
|
||||
const BinaryTruthTable &other) const {
|
||||
assert(numInputs == other.numInputs && numOutputs == other.numOutputs);
|
||||
return table.ult(other.table);
|
||||
}
|
||||
|
||||
bool BinaryTruthTable::operator==(const BinaryTruthTable &other) const {
|
||||
return numInputs == other.numInputs && numOutputs == other.numOutputs &&
|
||||
table == other.table;
|
||||
}
|
||||
|
||||
void BinaryTruthTable::dump(llvm::raw_ostream &os) const {
|
||||
os << "TruthTable(" << numInputs << " inputs, " << numOutputs << " outputs, "
|
||||
<< "value=";
|
||||
os << table << ")\n";
|
||||
|
||||
// Print header
|
||||
for (unsigned i = 0; i < numInputs; ++i) {
|
||||
os << "i" << i << " ";
|
||||
}
|
||||
for (unsigned i = 0; i < numOutputs; ++i) {
|
||||
os << "o" << i << " ";
|
||||
}
|
||||
os << "\n";
|
||||
|
||||
// Print separator
|
||||
for (unsigned i = 0; i < numInputs + numOutputs; ++i) {
|
||||
os << "---";
|
||||
}
|
||||
os << "\n";
|
||||
|
||||
// Print truth table rows
|
||||
for (unsigned i = 0; i < (1u << numInputs); ++i) {
|
||||
// Print input values
|
||||
for (unsigned j = 0; j < numInputs; ++j) {
|
||||
os << ((i >> j) & 1) << " ";
|
||||
}
|
||||
|
||||
// Print output values
|
||||
llvm::APInt input(numInputs, i);
|
||||
llvm::APInt output = getOutput(input);
|
||||
os << "|";
|
||||
for (unsigned j = 0; j < numOutputs; ++j) {
|
||||
os << output[j] << " ";
|
||||
}
|
||||
os << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// NPNClass
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
namespace {
|
||||
// Helper functions for permutation manipulation - kept as implementation
|
||||
// details
|
||||
|
||||
/// Create an identity permutation of the given size.
|
||||
/// Result[i] = i for all i in [0, size).
|
||||
llvm::SmallVector<unsigned> identityPermutation(unsigned size) {
|
||||
llvm::SmallVector<unsigned> identity(size);
|
||||
for (unsigned i = 0; i < size; ++i)
|
||||
identity[i] = i;
|
||||
return identity;
|
||||
}
|
||||
|
||||
/// Apply a permutation to a negation mask.
|
||||
/// Given a negation mask and a permutation, returns a new mask where
|
||||
/// the negation bits are reordered according to the permutation.
|
||||
unsigned permuteNegationMask(unsigned negationMask,
|
||||
ArrayRef<unsigned> permutation) {
|
||||
unsigned result = 0;
|
||||
for (unsigned i = 0; i < permutation.size(); ++i) {
|
||||
if (negationMask & (1u << i)) {
|
||||
result |= (1u << permutation[i]);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
/// Create the inverse of a permutation.
|
||||
/// If permutation[i] = j, then inverse[j] = i.
|
||||
llvm::SmallVector<unsigned> invertPermutation(ArrayRef<unsigned> permutation) {
|
||||
llvm::SmallVector<unsigned> inverse(permutation.size());
|
||||
for (unsigned i = 0; i < permutation.size(); ++i) {
|
||||
inverse[permutation[i]] = i;
|
||||
}
|
||||
return inverse;
|
||||
}
|
||||
|
||||
} // anonymous namespace
|
||||
|
||||
void NPNClass::getInputPermutation(
|
||||
const NPNClass &targetNPN,
|
||||
llvm::SmallVectorImpl<unsigned> &permutation) const {
|
||||
assert(inputPermutation.size() == targetNPN.inputPermutation.size() &&
|
||||
"NPN classes must have the same number of inputs");
|
||||
assert(equivalentOtherThanPermutation(targetNPN) &&
|
||||
"NPN classes must be equivalent for input mapping");
|
||||
|
||||
// Create inverse permutation for this NPN class
|
||||
auto thisInverse = invertPermutation(inputPermutation);
|
||||
|
||||
// For each input position in the target NPN class, find the corresponding
|
||||
// input position in this NPN class
|
||||
permutation.reserve(targetNPN.inputPermutation.size());
|
||||
for (unsigned i = 0; i < targetNPN.inputPermutation.size(); ++i) {
|
||||
// Target input i maps to canonical position targetNPN.inputPermutation[i]
|
||||
// We need the input in this NPN class that maps to the same canonical
|
||||
// position
|
||||
unsigned canonicalPos = targetNPN.inputPermutation[i];
|
||||
permutation.push_back(thisInverse[canonicalPos]);
|
||||
}
|
||||
}
|
||||
|
||||
NPNClass NPNClass::computeNPNCanonicalForm(const BinaryTruthTable &tt) {
|
||||
NPNClass canonical(tt);
|
||||
// Initialize permutation with identity
|
||||
canonical.inputPermutation = identityPermutation(tt.numInputs);
|
||||
assert(tt.numInputs <= 8 && "Inputs are too large");
|
||||
// Try all possible tables and pick the lexicographically smallest.
|
||||
// FIXME: The time complexity is O(n! * 2^(n + m)) where n is the number
|
||||
// of inputs and m is the number of outputs. This is not scalable so
|
||||
// semi-canonical forms should be used instead.
|
||||
for (uint32_t negMask = 0; negMask < (1u << tt.numInputs); ++negMask) {
|
||||
BinaryTruthTable negatedTT = tt.applyInputNegation(negMask);
|
||||
|
||||
// Try all possible permutations
|
||||
auto permutation = identityPermutation(tt.numInputs);
|
||||
|
||||
do {
|
||||
BinaryTruthTable permutedTT = negatedTT.applyPermutation(permutation);
|
||||
|
||||
// Permute the negation mask according to the permutation
|
||||
unsigned currentNegMask = permuteNegationMask(negMask, permutation);
|
||||
|
||||
// Try all negation masks for the output
|
||||
for (unsigned outputNegMask = 0; outputNegMask < (1u << tt.numOutputs);
|
||||
++outputNegMask) {
|
||||
// Apply output negation
|
||||
BinaryTruthTable candidateTT =
|
||||
permutedTT.applyOutputNegation(outputNegMask);
|
||||
|
||||
// Create a new NPN class for the candidate
|
||||
NPNClass candidate(candidateTT, permutation, currentNegMask,
|
||||
outputNegMask);
|
||||
|
||||
// Check if this candidate is lexicographically smaller than the
|
||||
// current canonical form
|
||||
if (candidate.isLexicographicallySmaller(canonical))
|
||||
canonical = std::move(candidate);
|
||||
}
|
||||
} while (std::next_permutation(permutation.begin(), permutation.end()));
|
||||
}
|
||||
|
||||
return canonical;
|
||||
}
|
||||
|
||||
void NPNClass::dump(llvm::raw_ostream &os) const {
|
||||
os << "NPNClass:\n";
|
||||
os << " Input permutation: [";
|
||||
for (unsigned i = 0; i < inputPermutation.size(); ++i) {
|
||||
if (i > 0)
|
||||
os << ", ";
|
||||
os << inputPermutation[i];
|
||||
}
|
||||
os << "]\n";
|
||||
os << " Input negation: 0b";
|
||||
for (int i = truthTable.numInputs - 1; i >= 0; --i) {
|
||||
os << ((inputNegation >> i) & 1);
|
||||
}
|
||||
os << "\n";
|
||||
os << " Output negation: 0b";
|
||||
for (int i = truthTable.numOutputs - 1; i >= 0; --i) {
|
||||
os << ((outputNegation >> i) & 1);
|
||||
}
|
||||
os << "\n";
|
||||
os << " Canonical truth table:\n";
|
||||
truthTable.dump(os);
|
||||
}
|
|
@ -1,6 +1,7 @@
|
|||
add_circt_unittest(CIRCTSupportTests
|
||||
FVIntTest.cpp
|
||||
JSONTest.cpp
|
||||
NPNClassTest.cpp
|
||||
PrettyPrinterTest.cpp
|
||||
)
|
||||
|
||||
|
|
|
@ -0,0 +1,414 @@
|
|||
//===----------------------------------------------------------------------===//
|
||||
//
|
||||
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
||||
// See https://llvm.org/LICENSE.txt for license information.
|
||||
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
||||
//
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
#include "circt/Support/NPNClass.h"
|
||||
#include "llvm/ADT/APInt.h"
|
||||
#include "gtest/gtest.h"
|
||||
|
||||
using namespace circt;
|
||||
using namespace llvm;
|
||||
|
||||
TEST(BinaryTruthTableTest, BasicConstruction) {
|
||||
// Test default constructor
|
||||
BinaryTruthTable defaultTT;
|
||||
EXPECT_EQ(defaultTT.numInputs, 0u);
|
||||
EXPECT_EQ(defaultTT.numOutputs, 0u);
|
||||
|
||||
// Test parameterized constructor with zero initialization
|
||||
BinaryTruthTable zeroTT(2, 1);
|
||||
EXPECT_EQ(zeroTT.numInputs, 2u);
|
||||
EXPECT_EQ(zeroTT.numOutputs, 1u);
|
||||
EXPECT_EQ(zeroTT.table.getBitWidth(), 4u); // 2^2 * 1
|
||||
EXPECT_EQ(zeroTT.table.getZExtValue(), 0u);
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, GetSetOutput) {
|
||||
BinaryTruthTable tt(2, 1);
|
||||
|
||||
// Test setting and getting output for different inputs
|
||||
APInt input00(2, 0); // 00
|
||||
APInt input01(2, 1); // 01
|
||||
APInt input10(2, 2); // 10
|
||||
APInt input11(2, 3); // 11
|
||||
APInt output0(1, 0);
|
||||
APInt output1(1, 1);
|
||||
|
||||
// Set outputs for AND gate truth table
|
||||
tt.setOutput(input00, output0);
|
||||
tt.setOutput(input01, output0);
|
||||
tt.setOutput(input10, output0);
|
||||
tt.setOutput(input11, output1);
|
||||
|
||||
// Verify outputs
|
||||
EXPECT_EQ(tt.getOutput(input00), output0);
|
||||
EXPECT_EQ(tt.getOutput(input01), output0);
|
||||
EXPECT_EQ(tt.getOutput(input10), output0);
|
||||
EXPECT_EQ(tt.getOutput(input11), output1);
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, Permutation) {
|
||||
// Create a truth table for a 2-input function: f(a,b) = a & !b
|
||||
BinaryTruthTable original(2, 1);
|
||||
APInt output0(1, 0);
|
||||
APInt output1(1, 1);
|
||||
|
||||
// Set truth table: f(0,0)=0, f(0,1)=0, f(1,0)=1, f(1,1)=0
|
||||
original.setOutput(APInt(2, 0), output0); // f(0,0) = 0
|
||||
original.setOutput(APInt(2, 1), output0); // f(0,1) = 0
|
||||
original.setOutput(APInt(2, 2), output1); // f(1,0) = 1
|
||||
original.setOutput(APInt(2, 3), output0); // f(1,1) = 0
|
||||
|
||||
// Apply permutation [1, 0] (swap inputs)
|
||||
SmallVector<unsigned> permutation = {1, 0};
|
||||
BinaryTruthTable permuted = original.applyPermutation(permutation);
|
||||
|
||||
// After permutation, the function becomes f(b,a) = b & !a
|
||||
// So: f(0,0)=0, f(0,1)=1, f(1,0)=0, f(1,1)=0
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 0)), output0); // f(0,0) = 0
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 1)), output1); // f(0,1) = 1
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 2)), output0); // f(1,0) = 0
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 3)), output0); // f(1,1) = 0
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, InputNegation) {
|
||||
// Create a truth table for AND gate: f(a,b) = a & b
|
||||
BinaryTruthTable original(2, 1);
|
||||
APInt output0(1, 0);
|
||||
APInt output1(1, 1);
|
||||
|
||||
// Set AND truth table
|
||||
original.setOutput(APInt(2, 0), output0); // f(0,0) = 0
|
||||
original.setOutput(APInt(2, 1), output0); // f(0,1) = 0
|
||||
original.setOutput(APInt(2, 2), output0); // f(1,0) = 0
|
||||
original.setOutput(APInt(2, 3), output1); // f(1,1) = 1
|
||||
|
||||
// Apply input negation mask 1 (negate the second)
|
||||
BinaryTruthTable negated = original.applyInputNegation(1);
|
||||
|
||||
APInt result00 = negated.getOutput(APInt(2, 0));
|
||||
APInt result01 = negated.getOutput(APInt(2, 1));
|
||||
APInt result10 = negated.getOutput(APInt(2, 2));
|
||||
APInt result11 = negated.getOutput(APInt(2, 3));
|
||||
|
||||
// For input negation mask 1 (negates the last input), the mapping is:
|
||||
// clang-format off
|
||||
// g(0,0) gets the output from f(0,!0) = f(0,1) = 0
|
||||
// g(0,1) gets the output from f(0,!1) = f(0,0) = 0
|
||||
// g(1,0) gets the output from f(1,!0) = f(1,1) = 1
|
||||
// g(1,1) gets the output from f(1,!1) = f(1,0) = 0
|
||||
// clang-format on
|
||||
EXPECT_EQ(result00, output0); // g(0,0) = 0
|
||||
EXPECT_EQ(result01, output0); // g(0,1) = 0
|
||||
EXPECT_EQ(result10, output1); // g(1,0) = 1
|
||||
EXPECT_EQ(result11, output0); // g(1,1) = 0
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, OutputNegation) {
|
||||
// Create a truth table for AND gate
|
||||
BinaryTruthTable original(2, 1);
|
||||
APInt output0(1, 0);
|
||||
APInt output1(1, 1);
|
||||
|
||||
original.setOutput(APInt(2, 0), output0);
|
||||
original.setOutput(APInt(2, 1), output0);
|
||||
original.setOutput(APInt(2, 2), output0);
|
||||
original.setOutput(APInt(2, 3), output1);
|
||||
|
||||
// Apply output negation (creates NAND gate)
|
||||
BinaryTruthTable negated = original.applyOutputNegation(1);
|
||||
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 0)), output1);
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 1)), output1);
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 2)), output1);
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 3)), output0);
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, Equality) {
|
||||
BinaryTruthTable tt1(2, 1);
|
||||
BinaryTruthTable tt2(2, 1);
|
||||
BinaryTruthTable tt3(3, 1); // Different size
|
||||
|
||||
// Both empty truth tables should be equal
|
||||
EXPECT_TRUE(tt1 == tt2);
|
||||
EXPECT_FALSE(tt1 == tt3);
|
||||
|
||||
// Set same values
|
||||
tt1.setOutput(APInt(2, 3), APInt(1, 1));
|
||||
tt2.setOutput(APInt(2, 3), APInt(1, 1));
|
||||
EXPECT_TRUE(tt1 == tt2);
|
||||
|
||||
// Set different values
|
||||
tt2.setOutput(APInt(2, 2), APInt(1, 1));
|
||||
EXPECT_FALSE(tt1 == tt2);
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, BasicConstruction) {
|
||||
// Test default constructor
|
||||
NPNClass defaultNPN;
|
||||
EXPECT_EQ(defaultNPN.inputNegation, 0u);
|
||||
EXPECT_EQ(defaultNPN.outputNegation, 0u);
|
||||
EXPECT_TRUE(defaultNPN.inputPermutation.empty());
|
||||
|
||||
// Test constructor from truth table
|
||||
BinaryTruthTable tt(2, 1);
|
||||
NPNClass npn(tt);
|
||||
EXPECT_EQ(npn.truthTable, tt);
|
||||
EXPECT_EQ(npn.inputNegation, 0u);
|
||||
EXPECT_EQ(npn.outputNegation, 0u);
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, CanonicalFormSimple) {
|
||||
// Create truth table for XOR: f(a,b) = a ^ b
|
||||
BinaryTruthTable xorTT(2, 1);
|
||||
xorTT.setOutput(APInt(2, 0), APInt(1, 0)); // 0 ^ 0 = 0
|
||||
xorTT.setOutput(APInt(2, 1), APInt(1, 1)); // 0 ^ 1 = 1
|
||||
xorTT.setOutput(APInt(2, 2), APInt(1, 1)); // 1 ^ 0 = 1
|
||||
xorTT.setOutput(APInt(2, 3), APInt(1, 0)); // 1 ^ 1 = 0
|
||||
|
||||
NPNClass canonical = NPNClass::computeNPNCanonicalForm(xorTT);
|
||||
|
||||
// XOR is symmetric, so canonical form should be predictable
|
||||
EXPECT_EQ(canonical.truthTable.numInputs, 2u);
|
||||
EXPECT_EQ(canonical.truthTable.numOutputs, 1u);
|
||||
EXPECT_EQ(canonical.inputPermutation.size(), 2u);
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, EquivalenceOtherThanPermutation) {
|
||||
BinaryTruthTable tt1(2, 1);
|
||||
BinaryTruthTable tt2(2, 1);
|
||||
|
||||
NPNClass npn1(tt1, {0, 1}, 0, 0);
|
||||
NPNClass npn2(tt2, {1, 0}, 0, 0); // Different permutation
|
||||
NPNClass npn3(tt1, {0, 1}, 1, 0); // Different input negation
|
||||
|
||||
EXPECT_TRUE(npn1.equivalentOtherThanPermutation(npn2));
|
||||
EXPECT_FALSE(npn1.equivalentOtherThanPermutation(npn3));
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, InputMapping) {
|
||||
BinaryTruthTable tt(3, 1);
|
||||
NPNClass npn1(tt, {2, 0, 1}, 0, 0); // Permutation [2,0,1]
|
||||
NPNClass npn2(tt, {1, 2, 0}, 0, 0); // Permutation [1,2,0]
|
||||
|
||||
SmallVector<unsigned> permutation;
|
||||
npn1.getInputPermutation(npn2, permutation);
|
||||
// Verify the mapping is correct
|
||||
EXPECT_EQ(permutation.size(), 3u);
|
||||
|
||||
// For each target input position i, mapping[i] should give us the input
|
||||
// position in npn1 that corresponds to the same canonical position
|
||||
for (unsigned i = 0; i < 3; ++i) {
|
||||
// Target input i maps to canonical position npn2.inputPermutation[i]
|
||||
unsigned targetCanonicalPos = npn2.inputPermutation[i];
|
||||
// npn1's input mapping[i] should map to the same canonical position
|
||||
unsigned npn1CanonicalPos = npn1.inputPermutation[permutation[i]];
|
||||
EXPECT_EQ(targetCanonicalPos, npn1CanonicalPos);
|
||||
}
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, LexicographicalOrdering) {
|
||||
BinaryTruthTable tt1(2, 1, APInt(4, 0x5)); // 0101
|
||||
BinaryTruthTable tt2(2, 1, APInt(4, 0x6)); // 0110
|
||||
|
||||
NPNClass npn1(tt1);
|
||||
NPNClass npn2(tt2);
|
||||
|
||||
// 0x5 < 0x6, so npn1 should be lexicographically smaller
|
||||
EXPECT_TRUE(npn1.isLexicographicallySmaller(npn2));
|
||||
EXPECT_FALSE(npn2.isLexicographicallySmaller(npn1));
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, Commutativity) {
|
||||
// Create truth table for AND gate
|
||||
BinaryTruthTable andTT(2, 1);
|
||||
andTT.setOutput(APInt(2, 0), APInt(1, 0));
|
||||
andTT.setOutput(APInt(2, 1), APInt(1, 0));
|
||||
andTT.setOutput(APInt(2, 2), APInt(1, 0));
|
||||
andTT.setOutput(APInt(2, 3), APInt(1, 1));
|
||||
|
||||
// Create swapped version (should be same canonical form since AND is
|
||||
// commutative)
|
||||
BinaryTruthTable andTTSwapped(2, 1);
|
||||
andTTSwapped.setOutput(APInt(2, 0), APInt(1, 0)); // f(0,0) = 0
|
||||
andTTSwapped.setOutput(APInt(2, 1), APInt(1, 0)); // f(0,1) = 0
|
||||
andTTSwapped.setOutput(APInt(2, 2), APInt(1, 0)); // f(1,0) = 0
|
||||
andTTSwapped.setOutput(APInt(2, 3), APInt(1, 1)); // f(1,1) = 1
|
||||
|
||||
NPNClass canonical1 = NPNClass::computeNPNCanonicalForm(andTT);
|
||||
NPNClass canonical2 = NPNClass::computeNPNCanonicalForm(andTTSwapped);
|
||||
|
||||
// Should have same canonical form
|
||||
EXPECT_TRUE(canonical1.equivalentOtherThanPermutation(canonical2));
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, MultiBitOutput) {
|
||||
// Test 2-input, 2-output function: f(a,b) = (a&b, a|b)
|
||||
BinaryTruthTable tt(2, 2);
|
||||
|
||||
// Set outputs for each input combination
|
||||
// f(0,0) = (0,0)
|
||||
tt.setOutput(APInt(2, 0), APInt(2, 0));
|
||||
// f(0,1) = (0,1)
|
||||
tt.setOutput(APInt(2, 1), APInt(2, 1));
|
||||
// f(1,0) = (0,1)
|
||||
tt.setOutput(APInt(2, 2), APInt(2, 1));
|
||||
// f(1,1) = (1,1)
|
||||
tt.setOutput(APInt(2, 3), APInt(2, 3));
|
||||
|
||||
// Verify outputs
|
||||
EXPECT_EQ(tt.getOutput(APInt(2, 0)), APInt(2, 0));
|
||||
EXPECT_EQ(tt.getOutput(APInt(2, 1)), APInt(2, 1));
|
||||
EXPECT_EQ(tt.getOutput(APInt(2, 2)), APInt(2, 1));
|
||||
EXPECT_EQ(tt.getOutput(APInt(2, 3)), APInt(2, 3));
|
||||
|
||||
// Test table bit width
|
||||
EXPECT_EQ(tt.table.getBitWidth(), 8u); // 2^2 * 2 = 8 bits
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, MultiBitOutputPermutation) {
|
||||
// Create 2-input, 2-output function: f(a,b) = (a&b, a^b)
|
||||
BinaryTruthTable original(2, 2);
|
||||
|
||||
// f(0,0) = (0,0)
|
||||
original.setOutput(APInt(2, 0), APInt(2, 0));
|
||||
// f(0,1) = (0,1)
|
||||
original.setOutput(APInt(2, 1), APInt(2, 1));
|
||||
// f(1,0) = (0,1)
|
||||
original.setOutput(APInt(2, 2), APInt(2, 1));
|
||||
// f(1,1) = (1,0)
|
||||
original.setOutput(APInt(2, 3), APInt(2, 2));
|
||||
|
||||
// Apply permutation [1,0] (swap inputs)
|
||||
SmallVector<unsigned> permutation = {1, 0};
|
||||
BinaryTruthTable permuted = original.applyPermutation(permutation);
|
||||
|
||||
// After swapping inputs, f(b,a) = (b&a, b^a)
|
||||
// f(0,0) = (0,0)
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 0)), APInt(2, 0));
|
||||
// f(0,1) = (0,1)
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 1)), APInt(2, 1));
|
||||
// f(1,0) = (0,1)
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 2)), APInt(2, 1));
|
||||
// f(1,1) = (1,0)
|
||||
EXPECT_EQ(permuted.getOutput(APInt(2, 3)), APInt(2, 2));
|
||||
}
|
||||
|
||||
TEST(BinaryTruthTableTest, MultiBitOutputNegation) {
|
||||
// Create 2-input, 2-output function
|
||||
BinaryTruthTable original(2, 2);
|
||||
|
||||
// Set some non-trivial outputs
|
||||
original.setOutput(APInt(2, 0), APInt(2, 0)); // 00
|
||||
original.setOutput(APInt(2, 1), APInt(2, 1)); // 01
|
||||
original.setOutput(APInt(2, 2), APInt(2, 2)); // 10
|
||||
original.setOutput(APInt(2, 3), APInt(2, 3)); // 11
|
||||
|
||||
// Apply output negation mask 1 (negate first output bit)
|
||||
BinaryTruthTable negated = original.applyOutputNegation(1);
|
||||
|
||||
// Check that only the first bit of each output is negated
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 0)), APInt(2, 1)); // 00 -> 01
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 1)), APInt(2, 0)); // 01 -> 00
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 2)), APInt(2, 3)); // 10 -> 11
|
||||
EXPECT_EQ(negated.getOutput(APInt(2, 3)), APInt(2, 2)); // 11 -> 10
|
||||
|
||||
// Apply output negation mask 2 (negate second output bit)
|
||||
BinaryTruthTable negated2 = original.applyOutputNegation(2);
|
||||
|
||||
EXPECT_EQ(negated2.getOutput(APInt(2, 0)), APInt(2, 2)); // 00 -> 10
|
||||
EXPECT_EQ(negated2.getOutput(APInt(2, 1)), APInt(2, 3)); // 01 -> 11
|
||||
EXPECT_EQ(negated2.getOutput(APInt(2, 2)), APInt(2, 0)); // 10 -> 00
|
||||
EXPECT_EQ(negated2.getOutput(APInt(2, 3)), APInt(2, 1)); // 11 -> 01
|
||||
|
||||
// Apply output negation mask 3 (negate both output bits)
|
||||
BinaryTruthTable negated3 = original.applyOutputNegation(3);
|
||||
|
||||
EXPECT_EQ(negated3.getOutput(APInt(2, 0)), APInt(2, 3)); // 00 -> 11
|
||||
EXPECT_EQ(negated3.getOutput(APInt(2, 1)), APInt(2, 2)); // 01 -> 10
|
||||
EXPECT_EQ(negated3.getOutput(APInt(2, 2)), APInt(2, 1)); // 10 -> 01
|
||||
EXPECT_EQ(negated3.getOutput(APInt(2, 3)), APInt(2, 0)); // 11 -> 00
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, MultiBitOutputCanonical) {
|
||||
// Create a 2-input, 2-output function: f(a,b) = (a&b, a|b)
|
||||
BinaryTruthTable tt(2, 2);
|
||||
|
||||
tt.setOutput(APInt(2, 0), APInt(2, 0)); // f(0,0) = (0,0)
|
||||
tt.setOutput(APInt(2, 1), APInt(2, 1)); // f(0,1) = (0,1)
|
||||
tt.setOutput(APInt(2, 2), APInt(2, 1)); // f(1,0) = (0,1)
|
||||
tt.setOutput(APInt(2, 3), APInt(2, 3)); // f(1,1) = (1,1)
|
||||
|
||||
NPNClass canonical = NPNClass::computeNPNCanonicalForm(tt);
|
||||
|
||||
// Should have correct dimensions
|
||||
EXPECT_EQ(canonical.truthTable.numInputs, 2u);
|
||||
EXPECT_EQ(canonical.truthTable.numOutputs, 2u);
|
||||
EXPECT_EQ(canonical.inputPermutation.size(), 2u);
|
||||
|
||||
// The canonical form should be well-defined and reproducible
|
||||
NPNClass canonical2 = NPNClass::computeNPNCanonicalForm(tt);
|
||||
EXPECT_TRUE(canonical.equivalentOtherThanPermutation(canonical2));
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, MultiBitOutputEquivalence) {
|
||||
// Create two equivalent 2-input, 2-output functions with different input
|
||||
// orderings
|
||||
BinaryTruthTable tt1(2, 2);
|
||||
BinaryTruthTable tt2(2, 2);
|
||||
|
||||
// tt1: f(a,b) = (a&b, a^b)
|
||||
tt1.setOutput(APInt(2, 0), APInt(2, 0)); // f(0,0) = (0,0)
|
||||
tt1.setOutput(APInt(2, 1), APInt(2, 1)); // f(0,1) = (0,1)
|
||||
tt1.setOutput(APInt(2, 2), APInt(2, 1)); // f(1,0) = (0,1)
|
||||
tt1.setOutput(APInt(2, 3), APInt(2, 2)); // f(1,1) = (1,0)
|
||||
|
||||
// tt2: g(a,b) = f(b,a) = (b&a, b^a) - same function with swapped inputs
|
||||
tt2.setOutput(APInt(2, 0), APInt(2, 0)); // g(0,0) = (0,0)
|
||||
tt2.setOutput(APInt(2, 1), APInt(2, 1)); // g(0,1) = (0,1)
|
||||
tt2.setOutput(APInt(2, 2), APInt(2, 1)); // g(1,0) = (0,1)
|
||||
tt2.setOutput(APInt(2, 3), APInt(2, 2)); // g(1,1) = (1,0)
|
||||
|
||||
NPNClass canonical1 = NPNClass::computeNPNCanonicalForm(tt1);
|
||||
NPNClass canonical2 = NPNClass::computeNPNCanonicalForm(tt2);
|
||||
|
||||
// Since the functions are equivalent under permutation, their canonical forms
|
||||
// should be equivalent (though permutations might differ)
|
||||
EXPECT_TRUE(canonical1.equivalentOtherThanPermutation(canonical2));
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, MultiBitOutputMapping) {
|
||||
// Test input mapping with multi-bit outputs
|
||||
BinaryTruthTable tt(2, 3); // 2 inputs, 3 outputs
|
||||
|
||||
NPNClass npn1(tt, {0, 1}, 0, 0); // Identity permutation
|
||||
NPNClass npn2(tt, {1, 0}, 0, 0); // Swapped permutation
|
||||
|
||||
SmallVector<unsigned> permutation;
|
||||
npn1.getInputPermutation(npn2, permutation);
|
||||
EXPECT_EQ(permutation.size(), 2u);
|
||||
|
||||
// Verify the mapping relationship
|
||||
for (unsigned i = 0; i < 2; ++i) {
|
||||
unsigned targetCanonicalPos = npn2.inputPermutation[i];
|
||||
unsigned npn1CanonicalPos = npn1.inputPermutation[permutation[i]];
|
||||
EXPECT_EQ(targetCanonicalPos, npn1CanonicalPos);
|
||||
}
|
||||
}
|
||||
|
||||
TEST(NPNClassTest, MultiBitOutputLexicographical) {
|
||||
// Test lexicographical ordering with multi-bit outputs
|
||||
BinaryTruthTable tt1(2, 2, APInt(8, 0x12)); // 00010010
|
||||
BinaryTruthTable tt2(2, 2, APInt(8, 0x34)); // 00110100
|
||||
|
||||
NPNClass npn1(tt1);
|
||||
NPNClass npn2(tt2);
|
||||
|
||||
// 0x12 < 0x34, so npn1 should be lexicographically smaller
|
||||
EXPECT_TRUE(npn1.isLexicographicallySmaller(npn2));
|
||||
EXPECT_FALSE(npn2.isLexicographicallySmaller(npn1));
|
||||
}
|
Loading…
Reference in New Issue