公开(公告)号：US12292946B1

公开(公告)日：2025-05-06

申请号：US18967676

申请日：2024-12-04

Applicant: SHANGHAITECH UNIVERSITY

Inventor： Rui Li ,  Lin Li ,  Yajun Ha

IPC: G06F17/16

Abstract: A method for implementing formal verification of an optimized multiplier via symbolic computer algebra (SCA)-satisfiability (SAT) synergy includes: systematically recovering, by a reverse engineering algorithm, an adder tree from an optimized multiplier; 2) generating, by a constraint satisfaction algorithm, a reference multiplier only by using an adder based on a constraint condition; and 3) combining, by an SCA-based and SAT-based verification method, complementary advantages of SCA and SAT. In the verification framework, the method introduces a reference multiplier generator for generating a correct reference multiplier. The correct reference multiplier has both a structure similar to a structure of the optimized multiplier and a clear adder boundary. The clear adder boundary allows proving correctness of the correct reference multiplier through SCA-based verification. With a structural similarity between the reference multiplier and the optimized multiplier, the reference multiplier is used as a known correct model for SAT-based verification of the optimized multiplier.

公开(公告)号：US11537774B2

公开(公告)日：2022-12-27

申请号：US17595194

申请日：2021-06-09

Applicant: SHANGHAITECH UNIVERSITY

Inventor： Rui Li ,  Yajun Ha

IPC: G06F30/34 ,  G06F30/337 ,  G06F30/3323

Abstract: An optimized reconfiguration algorithm based on dynamic voltage and frequency scaling (DVFS) is provided, which mainly has the following contributions. The optimized reconfiguration algorithm based on DVFS proposes a DVFS-based reconfiguration method, which schedules user tasks according to a degree of parallelism (DOP) of the user tasks so as to reconfigure more parallel user tasks, thereby achieving higher reliability. The optimized reconfiguration algorithm based on DVFS proposes a K-means-based heuristic approximation algorithm, which minimizes the delay of the DVFS-based reconfiguration scheduling algorithm. The optimized reconfiguration algorithm based on DVFS proposes a K-means-based method, which reduces memory overhead caused by DVFS-based reconfiguration scheduling. The optimized reconfiguration algorithm based on DVFS improves the reliability of a field programmable gate array (FPGA) system and minimizes the area overhead of a hardware circuit.