---
_id: '66185'
author:
- first_name: Kuan-Hsun
  full_name: Chen, Kuan-Hsun
  last_name: Chen
- first_name: Yung-Chia
  full_name: Lin, Yung-Chia
  last_name: Lin
- first_name: Jenq-Kuen
  full_name: Lee, Jenq-Kuen
  last_name: Lee
citation:
  ama: 'Chen K-H, Lin Y-C, Lee J-K. Guest Editorial: Special Issue on Systems Optimizations
    for DSP and AI Applications. <i>Journal of Signal Processing Systems</i>. 2023;95(5):569-570.
    doi:<a href="https://doi.org/10.1007/s11265-023-01854-y">10.1007/s11265-023-01854-y</a>'
  apa: 'Chen, K.-H., Lin, Y.-C., &#38; Lee, J.-K. (2023). Guest Editorial: Special
    Issue on Systems Optimizations for DSP and AI Applications. <i>Journal of Signal
    Processing Systems</i>, <i>95</i>(5), 569–570. <a href="https://doi.org/10.1007/s11265-023-01854-y">https://doi.org/10.1007/s11265-023-01854-y</a>'
  bibtex: '@article{Chen_Lin_Lee_2023, title={Guest Editorial: Special Issue on Systems
    Optimizations for DSP and AI Applications}, volume={95}, DOI={<a href="https://doi.org/10.1007/s11265-023-01854-y">10.1007/s11265-023-01854-y</a>},
    number={5}, journal={Journal of Signal Processing Systems}, publisher={Springer
    Science and Business Media LLC}, author={Chen, Kuan-Hsun and Lin, Yung-Chia and
    Lee, Jenq-Kuen}, year={2023}, pages={569–570} }'
  chicago: 'Chen, Kuan-Hsun, Yung-Chia Lin, and Jenq-Kuen Lee. “Guest Editorial: Special
    Issue on Systems Optimizations for DSP and AI Applications.” <i>Journal of Signal
    Processing Systems</i> 95, no. 5 (2023): 569–70. <a href="https://doi.org/10.1007/s11265-023-01854-y">https://doi.org/10.1007/s11265-023-01854-y</a>.'
  ieee: 'K.-H. Chen, Y.-C. Lin, and J.-K. Lee, “Guest Editorial: Special Issue on
    Systems Optimizations for DSP and AI Applications,” <i>Journal of Signal Processing
    Systems</i>, vol. 95, no. 5, pp. 569–570, 2023, doi: <a href="https://doi.org/10.1007/s11265-023-01854-y">10.1007/s11265-023-01854-y</a>.'
  mla: 'Chen, Kuan-Hsun, et al. “Guest Editorial: Special Issue on Systems Optimizations
    for DSP and AI Applications.” <i>Journal of Signal Processing Systems</i>, vol.
    95, no. 5, Springer Science and Business Media LLC, 2023, pp. 569–70, doi:<a href="https://doi.org/10.1007/s11265-023-01854-y">10.1007/s11265-023-01854-y</a>.'
  short: K.-H. Chen, Y.-C. Lin, J.-K. Lee, Journal of Signal Processing Systems 95
    (2023) 569–570.
date_created: 2026-07-03T21:14:35Z
date_updated: 2026-07-05T14:47:03Z
doi: 10.1007/s11265-023-01854-y
intvolume: '        95'
issue: '5'
language:
- iso: eng
page: 569-570
publication: Journal of Signal Processing Systems
publication_identifier:
  issn:
  - 1939-8018
  - 1939-8115
publication_status: published
publisher: Springer Science and Business Media LLC
status: public
title: 'Guest Editorial: Special Issue on Systems Optimizations for DSP and AI Applications'
type: journal_article
user_id: '128464'
volume: 95
year: '2023'
...
---
_id: '12967'
abstract:
- lang: eng
  text: Modern Boolean satisfiability solvers can emit proofs of unsatisfiability.
    There is substantial interest in being able to verify such proofs and also in
    using them for further computations. In this paper, we present an FPGA accelerator
    for checking resolution proofs, a popular proof format. Our accelerator exploits
    parallelism at the low level by implementing the basic resolution step in hardware,
    and at the high level by instantiating a number of parallel modules for proof
    checking. Since proof checking involves highly irregular memory accesses, we employ
    Hybrid Memory Cube technology for accelerator memory. The results show that while
    the accelerator is scalable and achieves speedups for all benchmark proofs, performance
    improvements are currently limited by the overhead of transitioning the proof
    into the accelerator memory.
author:
- first_name: Tim
  full_name: Hansmeier, Tim
  id: '49992'
  last_name: Hansmeier
  orcid: 0000-0003-1377-3339
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
- first_name: Md Jubaer Hossain
  full_name: Pantho, Md Jubaer Hossain
  last_name: Pantho
- first_name: David
  full_name: Andrews, David
  last_name: Andrews
citation:
  ama: Hansmeier T, Platzner M, Pantho MJH, Andrews D. An Accelerator for Resolution
    Proof Checking based on FPGA and Hybrid Memory Cube Technology. <i>Journal of
    Signal Processing Systems</i>. 2019;91(11):1259-1272. doi:<a href="https://doi.org/10.1007/s11265-018-1435-y">10.1007/s11265-018-1435-y</a>
  apa: Hansmeier, T., Platzner, M., Pantho, M. J. H., &#38; Andrews, D. (2019). An
    Accelerator for Resolution Proof Checking based on FPGA and Hybrid Memory Cube
    Technology. <i>Journal of Signal Processing Systems</i>, <i>91</i>(11), 1259–1272.
    <a href="https://doi.org/10.1007/s11265-018-1435-y">https://doi.org/10.1007/s11265-018-1435-y</a>
  bibtex: '@article{Hansmeier_Platzner_Pantho_Andrews_2019, title={An Accelerator
    for Resolution Proof Checking based on FPGA and Hybrid Memory Cube Technology},
    volume={91}, DOI={<a href="https://doi.org/10.1007/s11265-018-1435-y">10.1007/s11265-018-1435-y</a>},
    number={11}, journal={Journal of Signal Processing Systems}, author={Hansmeier,
    Tim and Platzner, Marco and Pantho, Md Jubaer Hossain and Andrews, David}, year={2019},
    pages={1259–1272} }'
  chicago: 'Hansmeier, Tim, Marco Platzner, Md Jubaer Hossain Pantho, and David Andrews.
    “An Accelerator for Resolution Proof Checking Based on FPGA and Hybrid Memory
    Cube Technology.” <i>Journal of Signal Processing Systems</i> 91, no. 11 (2019):
    1259–72. <a href="https://doi.org/10.1007/s11265-018-1435-y">https://doi.org/10.1007/s11265-018-1435-y</a>.'
  ieee: T. Hansmeier, M. Platzner, M. J. H. Pantho, and D. Andrews, “An Accelerator
    for Resolution Proof Checking based on FPGA and Hybrid Memory Cube Technology,”
    <i>Journal of Signal Processing Systems</i>, vol. 91, no. 11, pp. 1259–1272, 2019.
  mla: Hansmeier, Tim, et al. “An Accelerator for Resolution Proof Checking Based
    on FPGA and Hybrid Memory Cube Technology.” <i>Journal of Signal Processing Systems</i>,
    vol. 91, no. 11, 2019, pp. 1259–72, doi:<a href="https://doi.org/10.1007/s11265-018-1435-y">10.1007/s11265-018-1435-y</a>.
  short: T. Hansmeier, M. Platzner, M.J.H. Pantho, D. Andrews, Journal of Signal Processing
    Systems 91 (2019) 1259–1272.
date_created: 2019-08-26T13:41:57Z
date_updated: 2022-01-06T06:51:27Z
department:
- _id: '78'
doi: 10.1007/s11265-018-1435-y
intvolume: '        91'
issue: '11'
language:
- iso: eng
page: 1259 - 1272
publication: Journal of Signal Processing Systems
publication_identifier:
  issn:
  - 1939-8018
  - 1939-8115
publication_status: published
status: public
title: An Accelerator for Resolution Proof Checking based on FPGA and Hybrid Memory
  Cube Technology
type: journal_article
user_id: '49992'
volume: 91
year: '2019'
...