Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

FPGA programmable logic block evaluation using quantified Boolean satisfiability

FPGA programmable logic block evaluation using quantified Boolean satisfiability

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
IEE Proceedings - Computers and Digital Techniques — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

A novel field programmable gate array (FPGA) logic synthesis technique that determines if a logic function can be implemented in a given programmable circuit is presented, and how this problem can be formalised and solved using quantified Boolean satisfiability is described. This technique is general enough to be applied to any type of logic function and programmable circuit; thus, it has many applications to FPGAs. The application demonstrated is the FPGA programmable logic block evaluation and the results show that this tool allows radical new features of FPGA logic blocks to be evaluated in a rigorous scientific way.

References

    1. 1)
      • Cong, J., Wu, C., Ding, Y.: `Cut ranking and pruning enabling a general and efficient FPGA mapping solution', Proc. 1999 ACM/SIGDA Seventh Int. Symp. on Field Programmable Gate Arrays, 1999, ACM Press, p. 29–35.
    2. 2)
      • (2003) Spartan-iie 1.8v fpga family: function description.
    3. 3)
      • Tang, D., Yu, Y., Ranjan, D.P., Malik, S.: `Analysis of search based algorithms for satisfiability of quantified Boolean formulas arising from circuit state space diameter problems', SAT '04: The Seventh Int. Conf. on Theory and Applications of Satisfiability Testing, May 2004, p. 10–13.
    4. 4)
      • T. Larrabee . Test pattern generation using Boolean satisfiablity. IEEE Trans. Comput.-Aided Des. , 1 , 6 - 22
    5. 5)
      • Cong, J., Ding, Y.: `On area/depth trade-off in LUT-based FPGA technology mapping', Design Automation Conf., 1993, p. 213–218, available online: www.citeseer.ist.psu.edu/cong94areadepth.html.
    6. 6)
      • (2004) APEX 20K data sheet.
    7. 7)
      • Zhang, L., Malik, S.: `Conflict driven learning in a quantified Boolean satisfiability solver', ICCAD '02: Proc. 2002 IEEE/ACM Int. Conf. on Computer-Aided Design, 2002, ACM Press, p. 442–449.
    8. 8)
      • A. Kaviani , S. Brown . The hybrid field programmable architecture. IEEE Des. Test , 2 , 74 - 83
    9. 9)
      • Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: `Chaff: engineering an efficient SAT solver', Proc. 38th Design Automation Conf. (DAC'01), 2001, available online: www.citeseer.ist.psu.edu/moskewicz01chaff.html.
    10. 10)
      • Manohararajah, V., Brown, S.D., Vranesic, Z.G.: `Heuristics for area minimization in LUT-based FPGA technology mapping', Int. Workshop on Logic and Synthesis (IWLS'04), 2004.
    11. 11)
      • (2004) Virtex-ii complete data sheet ver 3.3.
    12. 12)
      • J. Cong , Y. Ding . An optimal technology mapping algorithm for delay optimization in lookup-table based FPGA designs. IEEE Trans. Comput.-Aided Des. , 1 , 1 - 13
    13. 13)
      • S. Yang . (1991) Logic synthesis and optimization benchmarks user guide version.
    14. 14)
      • J. Cong , Y.-Y. Hwang . Boolean matching for LUT-based logic blocks with applications to architecture evaluation and technology mapping. IEEE Trans. Comput.-Aided Des. , 9 , 1077 - 1090
    15. 15)
      • Arrows Electronics, available online: www.arrow.com.
    16. 16)
      • Levin, I., Pinter, R.Y.: `Realizing expression graphs using table-lookup FPGAs', Proc. Eur. Design Automation Conf., 1993, p. 306–311.
    17. 17)
      • E. Ahmed , J. Rose . (2000) The effect of LUT and cluster size on deep-submicron FPGA performance and density, ACM/SIGDA Int. Symp. on FPGAs.
    18. 18)
      • Biere, A.: `Resolve and expand', 7thInt. Conf. on Theory and Applications of Satisfiability Testing (SAT'04), 2004.
    19. 19)
      • V. Betz , J. Rose , A. Marquardt . (1999) Architecture and CAD for deep-submicron FPGAs.
    20. 20)
      • Lemieux, G.G., Lewis, D.M.: `Using sparse crossbars within LUT clusters', ACM/SIGDA Int. Symp. on FPGAs, 2001, p. 59–68, available online: www.citeseer.ist.psu.edu/lemieux01using.html.
    21. 21)
      • (2004) Component selector guide ver 14.0.
http://iet.metastore.ingenta.com/content/journals/10.1049/ip-cdt_20050164
Loading

Related content

content/journals/10.1049/ip-cdt_20050164
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address