Maciej Jerzy Ciesielski | EPFL Graph Search

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Computer Algebraic Approach to Verification and Debugging of Galois Field Multipliers

Maciej Jerzy Ciesielski, Cunxi Yu

The paper presents a novel method to verify and debug gate-level arithmetic circuits implemented in Galois Field arithmetic. The method is based on forward reduction of the specification polynomials of the circuit in GF(2(m)) using GF(2) models of its logic gates. We define a forward variable order "FO >" and the rules of forward reduction that enable verification, bug detection, and automatic bug correction in the circuit. By analyzing the remainder generated by forward reduction, the method can determine whether the circuit is buggy, and finds the location and the type of the bug. The experiments performed on Mastrovito and Montgomery multipliers show that our debugging method is independent of the location of the bug(s) and the debugging time is comparable to the time needed to verify the bug-free circuit.

IEEE2018

End-to-End Industrial Study of Retiming

Maciej Jerzy Ciesielski, Giovanni De Micheli, Cunxi Yu

Sequential circuits are combinational circuits that are separated by registers. Retiming is considered as the most promising technique for optimizing sequential circuits, that involves moving the edge-triggered registers across the combinational logic without changing the functionality. Despite significant efforts spent on sequential optimization since 1980's, there are few works discussed its performance in an end to-end design flow. The retiming algorithms were mostly evaluated at the logic level. However, it turns out that the retiming results at logic level could be significantly different than evaluating the physical level. This paper provides the findings of how retiming algorithms perform in an end-to-end industrial design flow, with seven industry designs taken from a recent 14nm microprocessor. Experiments are conducted with several complete industrial design flows. The evaluations are made at the end of the physical design flow. The experimental results show that the performance (design quality) of the retiming algorithms vary on the designs. Based these experimental results, we discover a feature that describes the retiming potentials of sequential designs. This model successfully forecast whether the given industrial designs could be significantly improved by retiming in an end-to-end design flow, regarding timing, area, and power.

IEEE2018

Exploiting Circuit Duality to Speed Up SAT

Luca Gaetano Amarù, Maciej Jerzy Ciesielski, Giovanni De Micheli, Pierre-Emmanuel Julien Marc Gaillardon

In this paper, we establish a non-trivial duality between tautology and contradiction check to speed up circuit SAT. Tautology check determines if a logic circuit is true in every possible interpretation. Analogously, contradiction check determines if a logic circuit is false in every possible interpretation. A trivial transformation of a (tautology, contradiction) check problem into a (contradiction, tautology) check problem is the inversion of all outputs in a logic circuit. In this work, we show that exact logic inversion is not necessary. We give operator switching rules that selectively exchange tautologies with contradictions, and vice versa. Our approach collapses into logic inversion just for tautology and contradiction extreme points but generates non-complementary logic circuits in the other cases. This property enables computing benefits when an alternative, but equisolvable, instance of a problem is easier to solve than the original one. As a case study, we investigate the impact on SAT. There, our methodology generates a dual SAT instance solvable in parallel with the original one. This concept can be used on top of any other SAT approach and does not impose much overhead, except having to run two solvers instead of one, which is typically not a problem because multi-cores are widespread and computing resources are inexpensive. Experimental results show a 25% speed-up of SAT in a concurrent execution scenario. Also, statistical experiments confirmed that our runtime reduction is not of the random variation type.

IEEE2015