-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
✨ Add SyReC synthesis with Additional Lines (#65)
This PR implements the original SyReC synthesis approach using additional lines. The `syrec-editor` GUI is updated accordingly. Signed-off-by: Lukas Burgholzer <lukas.burgholzer@jku.at> Co-authored-by: Lukas Burgholzer <lukas.burgholzer@jku.at>
- Loading branch information
1 parent
f898102
commit f1e591a
Showing
30 changed files
with
1,374 additions
and
906 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
34 changes: 34 additions & 0 deletions
34
include/algorithms/synthesis/syrec_synthesis_additional_lines.hpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
#pragma once | ||
|
||
#include "algorithms/synthesis/syrec_synthesis.hpp" | ||
|
||
namespace syrec { | ||
class SyrecSynthesisAdditionalLines: public SyrecSynthesis { | ||
public: | ||
using SyrecSynthesis::SyrecSynthesis; | ||
|
||
static bool synthesize(circuit& circ, const program& program, const properties::ptr& settings = std::make_shared<properties>(), const properties::ptr& statistics = std::make_shared<properties>()); | ||
|
||
protected: | ||
bool process_statement(const statement::ptr& statement) override { | ||
return !SyrecSynthesis::on_statement(statement); | ||
} | ||
|
||
void assign_add(bool& status, std::vector<unsigned>& lhs, std::vector<unsigned>& rhs, [[maybe_unused]] const unsigned& op) override { | ||
status = SyrecSynthesis::increase(lhs, rhs); | ||
} | ||
|
||
void assign_subtract(bool& status, std::vector<unsigned>& lhs, std::vector<unsigned>& rhs, [[maybe_unused]] const unsigned& op) override { | ||
status = SyrecSynthesis::decrease(lhs, rhs); | ||
} | ||
|
||
void assign_exor(bool& status, std::vector<unsigned>& lhs, std::vector<unsigned>& rhs, [[maybe_unused]] const unsigned& op) override { | ||
status = SyrecSynthesis::bitwise_cnot(lhs, rhs); | ||
} | ||
|
||
void exp_add(const unsigned& bitwidth, std::vector<unsigned>& lines, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs) override; | ||
void exp_subtract(const unsigned& bitwidth, std::vector<unsigned>& lines, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs) override; | ||
|
||
void exp_exor(const unsigned& bitwidth, std::vector<unsigned>& lines, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs) override; | ||
}; | ||
} // namespace syrec |
65 changes: 65 additions & 0 deletions
65
include/algorithms/synthesis/syrec_synthesis_no_additional_lines.hpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,65 @@ | ||
#pragma once | ||
|
||
#include "algorithms/synthesis/syrec_synthesis.hpp" | ||
|
||
namespace syrec { | ||
class SyrecSynthesisNoAdditionalLines: public SyrecSynthesis { | ||
public: | ||
using SyrecSynthesis::SyrecSynthesis; | ||
|
||
static bool synthesize(circuit& circ, const program& program, const properties::ptr& settings = std::make_shared<properties>(), const properties::ptr& statistics = std::make_shared<properties>()); | ||
|
||
protected: | ||
bool process_statement(const statement::ptr& statement) override { | ||
return !full_statement(statement) && !SyrecSynthesis::on_statement(statement); | ||
} | ||
|
||
bool full_statement(const statement::ptr& statement); | ||
bool full_statement(const assign_statement& statement); | ||
|
||
bool op_rhs_lhs_expression(const expression::ptr& expression, std::vector<unsigned>& v) override; | ||
|
||
bool op_rhs_lhs_expression(const variable_expression& expression, std::vector<unsigned>& v) override; | ||
|
||
bool op_rhs_lhs_expression(const binary_expression& expression, std::vector<unsigned>& v) override; | ||
|
||
void pop_exp(); | ||
|
||
void inverse(); | ||
|
||
void assign_add(bool& status, std::vector<unsigned>& lhs, std::vector<unsigned>& rhs, const unsigned& op) override; | ||
|
||
void assign_subtract(bool& status, std::vector<unsigned>& lhs, std::vector<unsigned>& rhs, const unsigned& op) override; | ||
|
||
void assign_exor(bool& status, std::vector<unsigned>& lhs, std::vector<unsigned>& rhs, const unsigned& op) override; | ||
|
||
bool solver(const std::vector<unsigned>& stat_lhs, unsigned stat_op, const std::vector<unsigned>& exp_lhs, unsigned exp_op, const std::vector<unsigned>& exp_rhs); | ||
|
||
bool flow(const expression::ptr& expression, std::vector<unsigned>& v); | ||
bool flow(const variable_expression& expression, std::vector<unsigned>& v); | ||
bool flow(const binary_expression& expression, const std::vector<unsigned>& v); | ||
|
||
void exp_add([[maybe_unused]] const unsigned& bitwidth, std::vector<unsigned>& lines, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs) override { | ||
SyrecSynthesis::increase(rhs, lhs); | ||
lines = rhs; | ||
} | ||
|
||
void exp_subtract([[maybe_unused]] const unsigned& bitwidth, std::vector<unsigned>& lines, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs) override { | ||
decrease_new_assign(rhs, lhs); | ||
lines = rhs; | ||
} | ||
|
||
void exp_exor([[maybe_unused]] const unsigned& bitwidth, std::vector<unsigned>& lines, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs) override { | ||
bitwise_cnot(rhs, lhs); // duplicate lhs | ||
lines = rhs; | ||
} | ||
|
||
bool exp_evaluate(std::vector<unsigned>& lines, unsigned op, const std::vector<unsigned>& lhs, const std::vector<unsigned>& rhs); | ||
|
||
bool expression_single_op(unsigned op, const std::vector<unsigned>& exp_lhs, const std::vector<unsigned>& exp_rhs); | ||
|
||
bool decrease_new_assign(const std::vector<unsigned>& rhs, const std::vector<unsigned>& lhs); | ||
|
||
bool expression_op_inverse(unsigned op, const std::vector<unsigned>& exp_lhs, const std::vector<unsigned>& exp_rhs) override; | ||
}; | ||
} // namespace syrec |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.