2008 | ||
---|---|---|
113 | EE | Paul T. Darga, Karem A. Sakallah, Igor L. Markov: Faster symmetry discovery using sparsity of symmetries. DAC 2008: 149-154 |
112 | EE | Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah: Reveal: A Formal Verification Tool for Verilog Designs. LPAR 2008: 343-352 |
111 | EE | Mark H. Liffiton, Karem A. Sakallah: Searching for Autarkies to Trim Unsatisfiable Clause Sets. SAT 2008: 182-195 |
110 | EE | Mark H. Liffiton, Karem A. Sakallah: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. J. Autom. Reasoning 40(1): 1-33 (2008) |
2007 | ||
109 | João Marques-Silva, Karem A. Sakallah: Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings Springer 2007 | |
108 | EE | Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah: Improved Design Debugging Using Maximum Satisfiability. FMCAD 2007: 13-19 |
107 | EE | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah: Symmetry breaking for pseudo-Boolean formulas. ACM Journal of Experimental Algorithmics 12: (2007) |
106 | EE | Fadi A. Aloul, Arathi Ramani, Karem A. Sakallah, Igor L. Markov: Solution and Optimization of Systems of Pseudo-Boolean Constraints. IEEE Trans. Computers 56(10): 1415-1424 (2007) |
2006 | ||
105 | EE | Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah: Refinement strategies for verification methods based on datapath abstraction. ASP-DAC 2006: 19-24 |
104 | EE | Hossein M. Sheini, Karem A. Sakallah: Ario: A Linear Integer Arithmetic Logic Solver. FMCAD 2006: 47-48 |
103 | EE | Hossein M. Sheini, Karem A. Sakallah: SMT(CLU): a step toward scalability in system verification. ICCAD 2006: 844-851 |
102 | EE | Hossein M. Sheini, Karem A. Sakallah: From Propositional Satisfiability to Satisfiability Modulo Theories. SAT 2006: 1-9 |
101 | EE | Hossein M. Sheini, Karem A. Sakallah: A Progressive Simplifier for Satisfiability Modulo Theories. SAT 2006: 184-197 |
100 | EE | Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov: Efficient Symmetry Breaking for Boolean Satisfiability. IEEE Trans. Computers 55(5): 549-558 (2006) |
99 | EE | Arathi Ramani, Igor L. Markov, Karem A. Sakallah, Fadi A. Aloul: Breaking Instance-Independent Symmetries In Exact Graph Coloring. J. Artif. Intell. Res. (JAIR) 26: 289-322 (2006) |
98 | EE | Hossein M. Sheini, Karem A. Sakallah: Pueblo: A Hybrid Pseudo-Boolean SAT Solver. JSAT 2(1-4): 165-189 (2006) |
2005 | ||
97 | EE | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah: Dynamic symmetry-breaking for improved Boolean optimization. ASP-DAC 2005: 445-450 |
96 | EE | Hossein M. Sheini, Bart Peintner, Karem A. Sakallah, Martha E. Pollack: On Solving Soft Temporal Constraints Using SAT Techniques. CP 2005: 607-621 |
95 | EE | Hossein M. Sheini, Karem A. Sakallah: A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems. CPAIOR 2005: 320-335 |
94 | EE | Hossein M. Sheini, Karem A. Sakallah: Pueblo: A Modern Pseudo-Boolean SAT Solver. DATE 2005: 684-685 |
93 | EE | Mark H. Liffiton, Michael D. Moffitt, Martha E. Pollack, Karem A. Sakallah: Identifying Conflicts in Overconstrained Temporal Problems. IJCAI 2005: 205-211 |
92 | EE | Mark H. Liffiton, Karem A. Sakallah: On Finding All Minimally Unsatisfiable Subformulas. SAT 2005: 173-186 |
91 | EE | Hossein M. Sheini, Karem A. Sakallah: A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. SAT 2005: 241-256 |
90 | EE | Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João P. Marques Silva, Karem A. Sakallah: A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. SAT 2005: 467-474 |
89 | EE | Maher N. Mneimneh, Karem A. Sakallah: Principles of Sequential-Equivalence Verification. IEEE Design & Test of Computers 22(3): 248-257 (2005) |
2004 | ||
88 | EE | Maher N. Mneimneh, Karem A. Sakallah, John Moondanos: Preserving synchronizing sequences of sequential circuits after retiming. ASP-DAC 2004: 579-584 |
87 | EE | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah: ShatterPB: symmetry-breaking for pseudo-Boolean formulas. ASP-DAC 2004: 883-886 |
86 | EE | Zaher S. Andraus, Karem A. Sakallah: Automatic abstraction and verification of verilog models. DAC 2004: 218-223 |
85 | EE | Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, Igor L. Markov: AMUSE: a minimally-unsatisfiable subformula extractor. DAC 2004: 518-523 |
84 | EE | Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov: Exploiting structure in symmetry detection for CNF. DAC 2004: 530-534 |
83 | EE | Arathi Ramani, Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: Breaking Instance-Independent Symmetries in Exact Graph Coloring. DATE 2004: 324-331 |
82 | EE | Gi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar: A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints. IEEE Trans. Computers 53(6): 688-696 (2004) |
81 | EE | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: MINCE: A Static Global Variable-Ordering Heuristic for SAT Search and BDD Manipulation. J. UCS 10(12): 1562-1596 (2004) |
2003 | ||
80 | EE | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: FORCE: a fast and easy-to-implement variable-ordering heuristic. ACM Great Lakes Symposium on VLSI 2003: 116-119 |
79 | EE | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: Shatter: efficient symmetry-breaking for boolean satisfiability. DAC 2003: 836-839 |
78 | Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov: Efficient Symmetry Breaking for Boolean Satisfiability. IJCAI 2003: 271-276 | |
77 | EE | Maher N. Mneimneh, Karem A. Sakallah: Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. SAT 2003: 411-425 |
76 | EE | Michael A. Riepe, Karem A. Sakallah: Transistor placement for noncomplementary digital VLSI cell synthesis. ACM Trans. Design Autom. Electr. Syst. 8(1): 81-107 (2003) |
75 | EE | Hui Xu, Rob A. Rutenbar, Karem A. Sakallah: sub-SAT: a formulation for relaxed Boolean satisfiability with applications in routing. IEEE Trans. on CAD of Integrated Circuits and Systems 22(6): 814-820 (2003) |
74 | EE | Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah: Satometer: how much have we searched? IEEE Trans. on CAD of Integrated Circuits and Systems 22(8): 995-1004 (2003) |
73 | EE | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah: Solving difficult instances of Boolean satisfiability in the presence of symmetry. IEEE Trans. on CAD of Integrated Circuits and Systems 22(9): 1117-1137 (2003) |
2002 | ||
72 | EE | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah: Solving difficult SAT instances in the presence of symmetry. DAC 2002: 731-736 |
71 | EE | Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah: Satometer: how much have we searched? DAC 2002: 737-742 |
70 | EE | Fadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah: Search-Based SAT Using Zero-Suppressed BDDs. DATE 2002: 1082 |
69 | EE | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar: Hybrid Routing for FPGAs by Integrating Boolean Satisfiability with Geometric Search. FPL 2002: 360-369 |
68 | EE | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah: Generic ILP versus specialized 0-1 ILP: an update. ICCAD 2002: 450-457 |
67 | EE | Victor N. Kravets, Karem A. Sakallah: Resynthesis of multi-level circuits under tight constraints using symbolic optimization. ICCAD 2002: 687-693 |
66 | EE | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: Improving the Efficiency of Circuit-to-BDD Conversion by Gate and Input Ordering. ICCD 2002: 64-69 |
65 | EE | Hui Xu, Rob A. Rutenbar, Karem A. Sakallah: sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing. ISPD 2002: 182-187 |
64 | Fadi A. Aloul, Maher N. Mneimneh, Karem A. Sakallah: ZBDD-Based Backtrack Search SAT Solver. IWLS 2002: 131-136 | |
63 | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: Efficient Gate and Input Ordering for Circuit-to-BDD Conversion. IWLS 2002: 137-142 | |
62 | Leyla Nazhandali, Karem A. Sakallah: Majority-Based Decomposition of Carry Logic in Binary Adders. IWLS 2002: 179-184 | |
61 | EE | Fadi A. Aloul, Soha Hassoun, Karem A. Sakallah, David Blaauw: Robust SAT-Based Search Algorithm for Leakage Power Reduction. PATMOS 2002: 167-177 |
60 | EE | Luís Guerra e Silva, João P. Marques Silva, Luis Miguel Silveira, Karem A. Sakallah: Satisfiability models and algorithms for circuit delay computation. ACM Trans. Design Autom. Electr. Syst. 7(1): 137-158 (2002) |
59 | EE | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar: A new FPGA detailed routing approach via search-based Booleansatisfiability. IEEE Trans. on CAD of Integrated Circuits and Systems 21(6): 674-684 (2002) |
2001 | ||
58 | EE | Maher N. Mneimneh, Fadi A. Aloul, Christopher T. Weaver, Saugata Chatterjee, Karem A. Sakallah, Todd M. Austin: Scalable Hybrid Verification of Complex Microprocessors. DAC 2001: 41-46 |
57 | EE | Jesse Whittemore, Joonyoung Kim, Karem A. Sakallah: SATIRE: A New Incremental Satisfiability Engine. DAC 2001: 542-545 |
56 | EE | Hakan Yalcin, Robert Palermo, Mohammad Mortazavi, Cyrus Bamji, Karem A. Sakallah, John P. Hayes: An Advanced Timing Characterization Method Using Mode Dependency. DAC 2001: 657-660 |
55 | EE | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar: A boolean satisfiability-based incremental rerouting approach with application to FPGAs. DATE 2001: 560-565 |
54 | EE | Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah: Faster SAT and Smaller BDDs via Common Function Structure. ICCAD 2001: 443-448 |
53 | EE | Gi-Joon Nam, Fadi A. Aloul, Karem A. Sakallah, Rob A. Rutenbar: A comparative study of two Boolean formulations of FPGA detailed routing constraints. ISPD 2001: 222-227 |
52 | EE | Hakan Yalcin, Mohammad Mortazavi, Robert Palermo, Cyrus Bamji, Karem A. Sakallah, John P. Hayes: Fast and accurate timing characterization using functionalinformation. IEEE Trans. on CAD of Integrated Circuits and Systems 20(2): 315-331 (2001) |
2000 | ||
51 | João P. Marques Silva, Karem A. Sakallah: Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. CAV 2000: 3 | |
50 | EE | João P. Marques Silva, Karem A. Sakallah: Boolean satisfiability in electronic design automation. DAC 2000: 675-680 |
49 | EE | Victor N. Kravets, Karem A. Sakallah: Constructive Library-Aware Synthesis Using Symmetries. DATE 2000: 208- |
48 | EE | Joonyoung Kim, Jesse Whittemore, Karem A. Sakallah, João P. Marques Silva: On Applying Incremental Satisfiability to Delay Fault Testing. DATE 2000: 380-384 |
47 | EE | Karem A. Sakallah, Fadi A. Aloul, João P. Marques Silva: An Experimental Study of Satisfiability Search Heuristics. DATE 2000: 745 |
46 | Victor N. Kravets, Karem A. Sakallah: Generalized Symmetries in Boolean Functions. ICCAD 2000: 526-532 | |
45 | EE | Joonyoung Kim, Jesse Whittemore, Karem A. Sakallah: On Solving Stack-Based Incremental Satisfiability Problems. ICCD 2000: 379-382 |
1999 | ||
44 | EE | Hakan Yalcin, Mohammad Mortazavi, Robert Palermo, Cyrus Bamji, Karem A. Sakallah: Functional Timing Analysis for IP Characterization. DAC 1999: 731-736 |
43 | EE | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar: Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs vis Search-Based Boolean SAT. FPGA 1999: 167-175 |
42 | EE | Michael A. Riepe, Karem A. Sakallah: Transistor level micro-placement and routing for two-dimensional digital VLSI cell synthesis. ISPD 1999: 74-81 |
41 | Joonyoung Kim, João P. Marques Silva, Karem A. Sakallah: Satisfiability-Based Functional Delay Fault Testing. VLSI 1999: 362-372 | |
40 | EE | Gi-Joon Nam, Karem A. Sakallah, Rob A. Rutenbar: Satisfiability-Based Detailed FPGA Routing. VLSI Design 1999: 574-577 |
39 | João P. Marques Silva, Karem A. Sakallah: GRAPS: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers 48(5): 506-521 (1999) | |
38 | EE | David Van Campenhout, Trevor N. Mudge, Karem A. Sakallah: Timing verification of sequential dynamic circuits. IEEE Trans. on CAD of Integrated Circuits and Systems 18(5): 645-658 (1999) |
1998 | ||
37 | EE | Phiroze N. Parakh, Richard B. Brown, Karem A. Sakallah: Congestion Driven Quadratic Placement. DAC 1998: 275-278 |
36 | EE | Victor N. Kravets, Karem A. Sakallah: M32: A Constructive multilevel Logic Synthesis System. DAC 1998: 336-341 |
35 | EE | V. Chandramouli, Jesse Whittemore, Karem A. Sakallah: AFTA: A Formal Delay Model for Functional Timing Analysis. DATE 1998: 350-355 |
34 | EE | Michael A. Riepe, Karem A. Sakallah: The edge-based design rule model revisited. ACM Trans. Design Autom. Electr. Syst. 3(3): 463-486 (1998) |
33 | EE | Richard B. Brown, Bruce Bernhardt, M. LaMacchia, J. Abrokwah, Phiroze N. Parakh, Todd D. Basso, Spencer M. Gold, S. Stetson, Claude R. Gauthier, D. Foster, B. Crawforth, T. McQuire, Karem A. Sakallah, Ronald J. Lomax, Trevor N. Mudge: Overview of complementary GaAs technology for high-speed VLSI circuits. IEEE Trans. VLSI Syst. 6(1): 47-51 (1998) |
1997 | ||
32 | EE | V. Chandramouli, Karem A. Sakallah, Ayman I. Kayssi: Signal Delay in Coupled, Distributed RC Lines in the Presence of Temporal Proximity. ARVLSI 1997: 32-46 |
31 | João P. Marques Silva, Karem A. Sakallah: Robust Search Algorithms for Test Pattern Generation. FTCS 1997: 152-161 | |
1996 | ||
30 | EE | V. Chandramouli, Karem A. Sakallah: Modeling the Effects of Temporal Proximity of Input Transitions on Gate Propagation Delay and Transition Time. DAC 1996: 617-622 |
29 | EE | Hakan Yalcin, John P. Hayes, Karem A. Sakallah: An approximate timing analysis method for datapath circuits. ICCAD 1996: 114-118 |
28 | EE | David Van Campenhout, Trevor N. Mudge, Karem A. Sakallah: Timing verification of sequential domino circuits. ICCAD 1996: 127-132 |
27 | EE | João P. Marques Silva, Karem A. Sakallah: GRASP - a new search algorithm for satisfiability. ICCAD 1996: 220-227 |
26 | João P. Marques Silva, Karem A. Sakallah: Conflict Analysis in Search Algorithms for Satisfiability. ICTAI 1996: 467-469 | |
25 | EE | Michael A. Riepe, João P. Marques Silva, Karem A. Sakallah, Richard B. Brown: Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulation. IEEE Trans. VLSI Syst. 4(1): 113-129 (1996) |
1995 | ||
24 | EE | Ajay Chandna, C. David Kibler, Richard B. Brown, Mark Roberts, Karem A. Sakallah: The Aurora RAM Compiler. DAC 1995: 261-266 |
23 | EE | Timothy M. Burks, Karem A. Sakallah, Trevor N. Mudge: Critical paths in circuits with level-sensitive latches. IEEE Trans. VLSI Syst. 3(2): 273-291 (1995) |
22 | EE | Chuan-Hua Chang, Edward S. Davidson, Karem A. Sakallah: Maximum rate single-phase clocking of a closed pipeline including wave pipelining, stoppability, and startability. IEEE Trans. on CAD of Integrated Circuits and Systems 14(12): 1526-1545 (1995) |
21 | EE | Ayman I. Kayssi, Karem A. Sakallah: Timing models for gallium arsenide direct-coupled FET logic circuits. IEEE Trans. on CAD of Integrated Circuits and Systems 14(3): 384-393 (1995) |
1994 | ||
20 | EE | João P. Marques Silva, Karem A. Sakallah: Dynamic Search-Space Pruning Techniques in Path Sensitization. DAC 1994: 705-711 |
19 | EE | Timothy M. Burks, Karem A. Sakallah: Optimization of critical paths in circuits with level-sensitive latches. ICCAD 1994: 468-473 |
18 | João P. Marques Silva, Karem A. Sakallah: Efficient and Robust Test Generation-Based Timing Analysis. ISCAS 1994: 303-306 | |
17 | Ayman I. Kayssi, Karem A. Sakallah: Macromodel Simplification Using Dimensional Analysis. ISCAS 1994: 335-338 | |
1993 | ||
16 | EE | Timothy M. Burks, Karem A. Sakallah: Min-max linear programming and the timing analysis of digital circuits. ICCAD 1993: 152-155 |
15 | Michael A. Riepe, João P. Marques Silva, Karem A. Sakallah, Richard B. Brown: Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation. ICCD 1993: 361-364 | |
14 | João P. Marques Silva, Karem A. Sakallah: An Analysis of Path Sensitization Criteria. ICCD 1993: 68-72 | |
13 | EE | Karem A. Sakallah, Trevor N. Mudge, Timothy M. Burks, Edward S. Davidson: Synchronization of pipelines. IEEE Trans. on CAD of Integrated Circuits and Systems 12(8): 1132-1146 (1993) |
1992 | ||
12 | EE | Timothy M. Burks, Karem A. Sakallah, Trevor N. Mudge: Identification of critical paths in circuits with level-sensitive latches. ICCAD 1992: 137-141 |
11 | EE | Chuan-Hua Chang, Edward S. Davidson, Karem A. Sakallah: Using constraint geometry to determine maximum rate pipeline clocking. ICCAD 1992: 142-148 |
10 | EE | Emily J. Shriver, Karem A. Sakallah: Ravel: assigned-delay compiled-code logic simulation. ICCAD 1992: 364-368 |
9 | EE | Karem A. Sakallah, Trevor N. Mudge, Oyekunle A. Olukotun: Analysis and design of latch-controlled synchronous digital circuits. IEEE Trans. on CAD of Integrated Circuits and Systems 11(3): 322-333 (1992) |
1991 | ||
8 | João P. Marques Silva, Karem A. Sakallah, Luís M. Vidigal: FPD - An Environment for Exact Timing Analysis. ICCAD 1991: 212-215 | |
7 | Karem A. Sakallah, Trevor N. Mudge, Timothy M. Burks, Edward S. Davidson: Optimal Clocking of Circular Pipelines. ICCD 1991: 642-650 | |
6 | Trevor N. Mudge, Richard B. Brown, William P. Bimingham, Jeffrey A. Dykstra, Ayman I. Kayssi, Ronald J. Lomax, Kunle Olukotun, Karem A. Sakallah, Raymond A. Milano: The Design of a Microsupercomputer. IEEE Computer 24(1): 57-64 (1991) | |
1990 | ||
5 | EE | Karem A. Sakallah, Trevor N. Mudge, Kunle Olukotun: Analysis and Design of Latch-Controlled Synchronous Digital Circuits. DAC 1990: 111-117 |
4 | Karem A. Sakallah, Trevor N. Mudge, Kunle Olukotun: check Tc and min Tc: Timing Verification and Optimal Clocking of Synchronous Digtal Circuits. ICCAD 1990: 552-555 | |
3 | Somanathan C. Menon, Karem A. Sakallah: Clock Qualification Algorithm for Timing Analysis of Custom CMOS VLSI Circuits with Overlapped Clocking Disciplines and On-section Clock Derivation. ICSI 1990: 550-558 | |
2 | EE | Karem A. Sakallah, Yao-Tsung Yen, Steve S. Greenberg: A first-order charge conserving MOS capacitance model. IEEE Trans. on CAD of Integrated Circuits and Systems 9(1): 99-108 (1990) |
1985 | ||
1 | EE | Karem A. Sakallah, Stephen W. Director: SAMSON2: An Event Driven VLSI Circuit Simulator. IEEE Trans. on CAD of Integrated Circuits and Systems 4(4): 668-684 (1985) |