Publications
-
2024
- Jiteshri Dasari, Maciej Ciesielski,
Combining Formal Verification and Testing for Debugging of Arithmetic Circuits,
Design, Automation and Test in Europe Conference, DATE-2024, March 2024.
2023
- Jiteshri Dasari, Maciej Ciesielski,
Efficient Formal Verification and Debugging of Arithmetic Divider Circuits,
IEEE/ACM International Conference on Computer Aided Design (ICCAD), October 2023.
- Jiteshri Dasari, Maciej Ciesielski,
Formal Verification of Restoring Dividers made Fast and Simple,
60th ACM/IEEE Design Automation Conference (DAC), July 2023.
- Atif Yasin, Tiankai Su, Sebastien Pillement, Maciej Ciesielski,
Formal Verification of Divider Circuits by Hardware Reduction,
19th International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design (SMACD), July 2023.
2022
- Maciej Ciesielski, Atif Yasin, Jiteshri Dasari,
Functional Verification of Arithmetic Circuits: Survey of Formal Methods,
25th International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS), April 2022.
2020
- Tiankai Su, Atif Yasin, Sébastien Pillement, Maciej Ciesielski,
Formal verification of constrained arithmetic circuits using computer algebraic approach,
IEEE Computer Society Annual Symposium on VLSI (ISVLSI), July 2020.
- Dinesh D Narasimharaju, RS Suraj Rao, Akshaya Sandeep Waingade, Atif Yasin, Maciej Ciesielski,
Dual Approach to Solving SAT in Hardware,
15th Design & Technology of Integrated Systems in Nanoscale Era (DTIS), April 2020.
- Atif Yasin, Tiankai Su, Sebastien Pillement, Maciej Ciesielski,
SPEAR: Hardware-based Implicit Rewriting for Square-root Verification,
Design, Automation and Test in Europe Conference, DATE-2020, March 2020.
2019
- Atif Yasin, Tiankai Su, Sebastien Pillement, Maciej Ciesielski,
Functional Verification of Hardware Dividers using Algebraic Model,
2019 IFIP/IEEE 27th International Conference on Very Large Scale Integration (VLSI-SoC), Cusco, Peru, Oct. 2019.
- Atif Yasin, Tiankai Su, Sebastien Pillement, Maciej Ciesielski,
Formal Verification of Integer Dividers: Division by a Constant, Intl. Conf of VLSI, ISVLSI-2019, July 2019.
- M. Ciesielski, Tiankai Su, Tiankai Su, Atif Yasin, Cunxi Yu,
Understanding Algebraic Rewriting for Arithmetic Circuit Verification: a Bit-Flow Model, IEEE Trans. on Computer-Aided Design, March 2019.
- Cunxi Yu, Tiankai Su, Atif Yasin, Maciej Ciesielski,
Spectral Approach to Verifying Non-linear Arithmetic Circuits,
ASPDAC, Japan, Jan. 21-24, 2019.
2018
- Cunxi Yu, Atif Yasin, Tiankai Su, Alan Mishchenko, Maciej Ciesielski,
Rewriting Environment for Arithmetic Circuit Verification,
22nd International Conference on Logic Programming, Artificial Intelligence and Reasoning (LPAR-22), EPIC Series in Computing, Vol. 57, pp. 656-666, November 16-21, 2018.
- Cunxi Yu, Maciej Ciesielski, Alan Mishchenko,
Fast Algebraic Rewriting Based on And-Inverter Graphs ,
IEEE Trans. on CAD, (DOI 10.1109/TCAD.2017.2772854) Vol. 37, No. 9, pp. 1907-1911, September 2018.
- Cunxi Yu, Chau-Chin Huang, Gi-Joon Nam, Mihir Choudhury, Victor N. Kravets,
Andrew Sullivan, Maciej Ciesielski, Giovanni De Micheli,
End-to-End Industrial Study of Retiming,
ISVLSI-2018, pp. 203-208, Hong Kong, July 9-11, 2018.
- Tiankai Su, Atif Yasin, Cunxi Yu, Maciej Ciesielski,
Computer Algebraic Approach to Verification and Debugging of Galois Field Multipliers, IEEE Intl. Symposium on Circuits and Systems (ISCAS), May 27-30, pp. 1-6, 2018.
- Cunxi Yu and M. Ciesielski,
Formal Analysis of GF Arithmetic Circuits - Parallel Verification and Reverse Engineering, IEEE Trans. on Computer-Aided Design, arXiv:1802.06870v1, pp. 1-13, Feb. 2018.
2017
- Cunxi Yu, Xiangyu Zhang, Duo Liu, Maciej Ciesielski, Daniel Holcomb,
Incremental SAT-based Reverse Engineering of Camouflaged Logic Circuits, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), pp. 1647-1659, Oct. 2017.
- Cunxi Yu, Mihir Choudhury, David Geiger, Andrew Sullivan and Maciej Ciesielski,
Advanced Datapath Synthesis using Graph Isomorphism,
2017 International Conference On Computer Aided Design (ICCAD'17), Nov. 13-16, 2017, Irvine, CA, USA.
- Tiankai Su, Cunxi Yu, Atif Yasin, and Maciej Ciesielski,
Formal Verification of Truncated Multipliers using Algebraic Approach,
2017 IEEE Computer Society Annual Symposium on VLSI (ISVLSI'17), pp. 415-420,
July 3-5, 2017, Bochum, Germany.
- Cunxi Yu, Mihir Choudhury, David Geiger, Andrew Sullivan and Maciej Ciesielski,
``Advanced Logic synthesis of Datapaths using Graph Isomorphism'',
International Workshop on Logic Synthesis, IWLS 2017, June 2017, Austin, USA.
- Cunxi Yu, Maciej Ciesielski,
Reverse Engineering of Irreducible Polynomials in GF(2^m) Arithmetic,
DATE-2017, pp. 1558-1563, March 2017.
- Cunxi Yu, Maciej Ciesielski,
Efficient Parallel Verification of Galois Field Multipliers ,
ASP-DAC 2017, Japan, Jan. 2017.
2016
- Cunxi Yu, Walter Brown, Duo Liu, Andre Rossi, Maciej Ciesielski,
Formal Verification of Arithmetic Circuits by Function Extraction,
IEEE Transactions on CAD (TCAD), 35(12): pp. 2131-2142, Dec. 2016.
- Cunxi Yu, Maciej Ciesielski,
Analyzing Imprecise Adders using BDDs: A Case Study,
IEEE Computer Society Annual Symposium on VLSI (ISVLSI) 2016, July 2016.
- Cunxi Yu, Maciej Ciesielski,
Formal Verification using Don't-care and Vanishing Polynomials,
IEEE Computer Society Annual Symposium on VLSI (ISVLSI) 2016, July 2016.
- C. Yu, M. Choudhury, A. Sullivan, M. Ciesielski,
DAC-Aware Logic Synthesis of Datapaths,
Design Automation Conference (DAC), pp. 1 - 6, June 2016.
- C. Yu, M. Ciesielski,
Automatic Word-level Abstraction of Datapaths,
2016 IEEE International Symposium on Circuits and Systems (ISCAS), pp. 1 - 6, May 2016.
2015
- M. Ciesielski Functional Verification of Arithmetic Circuits , 2015 IEEE International Conference on Computer Design (ICCD), Tutorial.
- S. Ghandali, C. Yu, D. Liu, W. Brown, M. Ciesielski,
Logic Debugging of Arithmetic Circuits,
IEEE Computer Society Annual Symposium on VLSI (ISVLSI) 2015, pp. 113-118, July 2015.
- L. Amaru, P. Gaillardon, A. Mishchenko, M. Ciesielski, G. Micheli,
Exploiting Circuit Duality to Speed up SAT,
IEEE Computer Society Annual Symposium on VLSI (ISVLSI) 2015, pp. 101-106, July 2015.
- Cunxi Yu, Walter Brown, Maciej Ciesielski,
Verification of Arithmetic Datapath Designs using Word-level Approach - A Case Study, IEEE Intl. Symposium on Circuits and Systems (ISCAS), May 2015.
- M. Ciesielski, C. Yu, D. Liu, W. Brown, A. Rossi,
Verification of Gate-level Arithmetic Circuits by Function Extraction,
Design Automation Conference (DAC), June 2015.
2014
- M. Ciesielski, W. Brown, D. Liu, A. Rossi,
Function Extraction from Arithmetic Bit-level Circuits,
IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. 356-361, July 2014.
- T.B. Ahmad, M. Ciesielski,
Parallel Multi-core Verilog HDL Simulation using Domain Partitioning, IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. 619-624, July 2014.
- M. Ciesielski, W. Brown, D. Liu, A. Rossi,
Function Extraction using Network Flow Model,
interactive presentation/poster, Design Automation Conference, DAC-2014, June 2014.
- T.B. Ahmad, M. Ciesielski,
Fast Time-Parallel C-based Event-Driven RTL Simulation, Design and Diagnostics of Electronic Circuits and Systems, DDECS-14, pp. 71-76, April 2014.
- T.B. Ahmad and M. Ciesielski,
Fast STA Prediction-based Gate-Level Timing Simulation, DATE-2014, pp. 248.1--248.6, March 2014.
2013
- T.B. Ahmad, M. Ciesielski,
An Approach to Multi-core Functional Gate-level Simulation Minimizing Synchronization and Communication Overheadsl, 14th International Workshop on Microprocessor Test and Verification (MTVCON 2013), 6 pages, Dec. 2013.
- M. Ciesielski, W. Brown, A. Rossi,
Arithmetic Bit-level Verification using Network Flow Model,
Haifa Verification Conference, HVC-2013; in Bertacco and A. Legay (Eds.):
LNCS 8244, pp. 327--343, 2013.
- D. Kim, M. Ciesielski, S. Yang,
MULTES: MUlti-Level Temporal-parallel Event-driven Simulation, IEEE Transactions on Computer Aided Design, 32(6), pp. 845-857, June 2013.
- D. Gomez-Prado, M. Ciesielski, R. Tessier,
FPGA latency optimization using system-level transformations and DFG restructuring, DATE 2013, pp. 1553-1558, March 2013.
2012
- T.B. Ahmad, N. Kim, B. Min, A. Kalia, M. Ciesielski, and S. Yang,
Scalable Parallel Event-driven HDL Simulation for Multi-Cores ,
Intl. Conf. on Synthesis, Modeling, Analysis and Simulation Methods and
Applications to Circuit Design, SMACD-2012, pp. 217-220, Sept. 2012.
- T.B. Ahmad, M. Ciesielski, D. Kim, and S. Yang,
Application of Parallel Distributed Event Driven Simulation for Accelerating Hardware Verification, Advances in Distributed and Parallel Computing (ADPC 2012), pp. 54-59, Sept. 2012.
2011
- M.A. Basith, T. Ahmad, A. Rossi, M. Ciesielski,
Algebraic Approach to Arithmetic Design Verification, FMCAD-11, Oct/Nov 2011.
- D. Kim, M. Ciesielski, K. Shim, S.Yang,
Temporal Parallel Simulation: A Fast Gate-Level HDL Simulation using Higher Level Models , DATE'11, March 2011.
- D. Kim, M. Ciesielski, S.Yang,
A New Distributed Event-Driven Gate-Level HDL Timing Simulation by Accurate Prediction , DATE'11, March 2011.
2010
- D. Gomez-Prado, D. Kim, M. Ciesielski, E. Boutillon,
Retiming Arithmetic Datapaths using Timed Taylor Expansion Diagrams,
2010 IEEE International High Level Design Validation and Test Workshop (HLDVT), 10-12 June 2010, pp. 33-39.
- D. Kim, D. Gomez-Prado, M. Ciesielski,
Computing State Matching in Sequential Circuits in Application to Temporal Parallel Simulation, Intl. Workshop on Logic Synthesis, IWLS'10, June 2010, pp. 171-177.
- A. Mishchenko, N. Een, R. K. Brayton, S. Jang, M. Ciesielski, T. Daniel,
Magic: An Industrial-Strength Logic Optimization, Technology
Mapping, and Formal Verification Tool, Intl. Workshop on Logic Synthesis, IWLS'10, June 2010, pp. 124-127.
2009
- M. Ciesielski, D. Gomez-Prado, Q.Ren, J. Guillot, E. Boutillon,
Optimization of Data Flow Computations using Canonical TED Representation,
IEEE Transactions on Computer-Aided Design, Vol. 28, No. 9, Sept. 2009, pp. 1321 - 1333.
- M. Ciesielski, J. Guillot, D. Gomez-Prado, E. Boutillon,
High-Level Transformations of Data Flow Computations using Canonical TED Representation,
Design & Test of Computers, Special issue, July/Aug 2009, pp. 46-57.
- M. Ciesielski, A.M. Jabir, D. Pradhan,
Canonical Graph-based Representations for Verification of Arithmetic and Data Flow Designs; book chapter, in Practical Design Verification,
ed. D.K. Pradhan, I.G. Harris, Cambridge University Press, 2009, pp. 173-245.
- D. Gomez-Prado, Q. Ren, M. Ciesielski, J. Guillot, and E. Boutillon,
Optimizing Data Flow Graphs to Minimize Hardware Implementation
Design, Automation and Test in Europe Conference, DATE'09, April, 2009.
2008
- D. Kim, M. Ciesielski, K. Shim, S.Yang,
Temporal Parallel Gate-level Timing Simulation ,
IEEE Workshop on High Level Design Verification and Test, HLDVT-08,
pp. 111-116, Nov 2008.
- M. Ciesielski, Q. Ren, D. Gomez-Prado, J. Guillot, E. Boutillon,
TDS: Behavioral Transformation System based on Canonical Dataflow
Representation
(poster) , Design, Automation and Test in Europe Conference},
DATE'08, Workshop: New Wave of High-Level Synthesis, 2008.
2007 and earlier
- M. Ciesielski, S. Askar, D. Gomez-Prado, J. Guillot, and E. Boutillon,
Data-Flow Transformations using Taylor Expansion Diagrams
Design, Automation and Test in Europe Conference, DATE'07, April, 2007.
- M. Ciesielski, P. Kalla, S. Askar,
Taylor Expansion Diagrams: A Canonical Representation
for Verification of Data Flow Designs,
IEEE Transactions on Computers,
Vol. 55, No. 9, pp. 1188-1201, Sept. 2006.
- J. Guillot, E. Boutillon, D. Gomez-Prado, S. Askar, Q. Ren, and
M. Ciesielski,
Efficient Factorization of DSP Transforms using Taylor Expansion
Diagrams,
Design, Automation and Test Conference in Europe, DATE'06, March 2006.
- Z. Zeng, K.R. Talupuru, and M. Ciesielski,
Functional Test Generation based on Word-level SAT,
in Journal of Systems Architecture.
Vol.51, Issue 8, August 2005, pp. 488-511.
Elsevier Publishers, 2005.
- D. Gomez-Prado, Q. Ren, S. Askar, M. Ciesielski, E. Boutillon,
Variable Ordering for Taylor Expansions Diagrams,
IEEE Intl. High Level Design Validation and Test Workshop>, HLDVT-04,
pp. 55-59, Nov. 2004.
- Z. Zeng, Q. Zhang, I. Harris, M. Ciesielski,
Fast Compputation of Data Correlation using BDDs ,
Design Automation & Test in Europe, DATE-2003,
pp. 122-127, March 2003.
- D. Pradhan, S. Askar, M. Ciesielski,
Mathematical Framework for Representing Discrete Functions as Word-level
Polynomials,
IEEE Intl. High Level Design Validation and Test Workshop, HLDVT-03,
pp. 135-139, Nov. 2003.
-
C. Yang, M. Ciesielski,
BDS: BDD-based Logic Optimization System ,
IEEE Transactions on CAD, Vol. 21, pp. 866-876, July 2002.
- M. Ciesielski, P. Kalla, Z. Zeng, B. Rouzeyre,
Taylor Expansion Diagrams: A Compact, Canonical Representation with
Applications to Symbolic Verification ,
Design Automation & Test in Europe, DATE-2002, p. 285-289, March 2002.
- M. Ciesielski, S. Askar, S. Levitin,
Analytical Approach to Layout Generation of Datapath Cells ,
IEEE Transactions on CAD, Vol. 21, No. 12, pp. 1480-1488, Dec. 2002
-
P. Kalla, M. Ciesielski,
A Comprehensive Approach to Partial Scan Problem using Implicit State
Enumeration , IEEE Trans. on Computer-Aided Design, Vol. 21,
pp. 810-826, July 2002.
-
Z. Zeng, P. Kalla, M. Ciesielski,
LPSAT: A Unified Approach to RTL Satisfiability (PS file).
Design, Automation and Test in Europe Conference, DATE-2001,
pp. 398-402, March 2001.
-
M. Fujita, Y. Matsunaga, M. Ciesielski,
``Multi-Level Logic Optimization'', in Logic Synthesis and Verification,
Kluwer Academic Publishers, ed. by T. Sasao and S. Hassoun. Chapter 2,
pp. 29-67, Aug. 2001.
-
Z. Zeng, M. Ciesielski, B. Rouzeyre,
Functional Test Generation using Constraint Logic Programming ,
in Proc. IFIP VLSI-SOC Conference Dec. 2001.
- S. Askar, M. Ciesielski,
Transistor Placement for Custom Datapath Cells (PS file).
15th Design of Circuits and Integrated Systems Conference, DCIS-2000.
-
P. Kalla, M. Ciesielski,
A BDD-based Satisfiability Infrastructure using the Unate Recursive
Paradigm. (PS file).
Design, Automation and Test in Europe Conference, DATE-2000.
- C. Yang, V. Singhal, M. Ciesielski,
BDD Decomposition for Efficient Logic Synthesis (PS file).
Intl. Conference on Computer Design: VLSI in Computers and Processors,
ICCD'99 .
- S. Askar, M. Ciesielski,
Analytical Approach to Custom Datapath Design (PDF file).
Intl. Conference on Computer-Aided Design, ICCAD'99.
-
P. Kalla, M. Ciesielski,
Performance Driven Resynthesis by Exploiting Retiming-Induced State
Register Equivalence ,
Design & Test in Europe Conference, DATE'99.
- B. Iyer, M. Ciesielski,
Reencoding for Cycle-Time Minimization under Fixed Encoding
Length , (PDF file).
Intl. Conference on Computer-Aided Design, ICCAD'98.
-
P. Kalla, M. Ciesielski,
A Comprehensive Approach to Partial Scan Problem using Implicit State
Enumeration , International Test Conference, 1998.
- S. Bommu, M. Ciesielski, P. Kalla, N. O'Neill,
Sequential Logic Optimization with Implicit Retiming and Resynthesis,
Proceedings of International Conference on VLSI'97.
- B. Iyer, M. Ciesielski,
METAMORPHOSIS: State Assignment by Retiming and Re-encoding,
Intl. Conference on Computer-Aided Design, ICCAD'96, 1996.
- P. Kalla, M. Ciesielski,
Testability of Sequential Circuits with Multi-Cycle False Paths,
15th IEEE VLSI Test Symposium, 1997.
- W. Burleson, M. Ciesielski, F. Klass, W. Liu,
Wave-pipelining: A tutorial and Survey of Recent Research
(ps.gz file).
IEEE Transactions on VLSI, Vol.6, No.3, pp. 464-474, Sept. 1998.
- Z. Hasan, M. Ciesielski,
FSM Decomposition and Functional Verification of FSM Networks,
VLSI Design: An International Journal of Custom-Chip Design,
Simulation and Testing, 1995.
- S. Yang, M. Ciesielski, Optimum and Suboptimum Algorithms for Input Encoding and its Relationship to Logic Minimization , IEEE Trans. on CAD, Jan. 1991.