Yin

Introduction

C Yin library, named after "寅虎", is one of the Synthesis and Verification Libraries of Zodiac Program.

Yin contains operation on truth table, it is separated from the graph based optimization library. Truth table, especially bit-level based technique will be extended here in this library. As for STP(Semi-tensor product) based example, please refer to Zilib.

Caution

Sanitize check is turned on, if mem error/leak exists, PR won't be accepted.

Build

Since some functionalities depend on Zilib, a recursive clone is needed.

git clone --recursive [email protected]:wjrforcyber/Yin.git
mkdir build
cd build
cmake ..
make
make test

Select Interface

• Check if a boolean function is positive/negative unate/binate etc. Use
  enum FUNC_TYPE isUnate(truthTable* tt, ziArray* res); For example, XOR is binate, by loading a two input truthtable $T$ which contains 0110, and an array $A$ for storing each property of a variable $v_i$ on index $i$ of $A$. The final result is the property $P$ of the whole Boolean function.

    ziArray record_xor;
    char tts_xor[] = "0110";
    truthTable *ttXOR = readTT(tts_xor, 1);
    enum FUNC_TYPE type_unate_xor = isUnate(ttXOR, &record_xor);
    assert(type_unate_xor == BINATE);
    clearEachEntryArray(&record_xor);