skip to main content
10.1145/2157136.2157268acmconferencesArticle/Chapter ViewAbstractPublication PagessigcseConference Proceedingsconference-collections
research-article

Integrating formal verification in an online judge for e-Learning logic circuit design

Published: 29 February 2012 Publication History

Abstract

This paper investigates the use of formal verification techniques to create online judges that can assist in teaching logic circuit design. Formal verification not only contributes to give an exact assessment about correctness, but also saves the instructor the tedious task of designing test cases. The paper explains how formal verification has been integrated in an online judge. It also describes the courseware created for a course on logic circuits and the successful experience of using it in a one-week summer course with students from secondary and high school.

References

[1]
NuSMV v2.5 User Manual. \myurlhttp://nusmv.fbk.eu.
[2]
J. Bhasker. Verilog HDL Synthesis: A Practical Primer. Star Galaxy Publishing, 1998.
[3]
J. Bhasker. A VHDL Primer. Prentice Hall, third edition, 1999.
[4]
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677--691, 1986.
[5]
B. Cheang, A. Kurnia, A. Lim, and W.-C. Oon. On automated grading of programming assignments in an academic institution. Computers & Education, 41(2):121--131, 2003.
[6]
A. Cimatti et al. NuSMV2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS. Springer, July 2002.
[7]
E. M. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press, 2001.
[8]
M. Damm, F. Bauer, and G. Zucker. Solving Digital Logic Assignments with Automatic Verification in SCORM Modules. In International Conference on Interactive Computer-Aided Learning (ICL), pages 359--363, 2009.
[9]
M. Damm, B. Klauer, and K. Waldschmidt. LogiFlash - A Flash-based Logic-Simulator for Educational Purposes. In World Conference on Educational Multimedia, Hypermedia and Telecommunications, pages 748--750, 2003.
[10]
O. Giménez, J. Petit, and S. Roura. Jutge.org: An educational programming judge. In Proc. of the 43rd ACM Technical Symposium on Computer Science Education (SIGCSE-2012), 2012.
[11]
E. I. Goldberg, M. R. Prasad, and R. K. Brayton. Using SAT for combinational equivalence checking. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE), pages 114--121, 2001.
[12]
D. Jansen. The Electronic Design Automation Handbook. Kluwer Academic Publishers, 2003.
[13]
M. Joy, N. Griffiths, and R. Boyatt. The BOSS online submission and assessment system. ACM Journal on Educational Resources in Computing, 5(3), 2005.
[14]
A. Kuehlmann and C. A. J. van Eijk. Combinational and sequential equivalence checking, pages 343--372. Kluwer Academic Publishers, 2002.
[15]
J. P. Mermet. Fundamentals and Standards in Hardware Description Languages. Kluwer Academic Publishers, Norwell, MA, USA, 1993.
[16]
A. Pnueli. The temporal logic of programs. In FOCS, pages 46--57. IEEE, 1977.
[17]
A. Sagahyroon and M. Massoumi. On the use of hardware description languages in teaching VLSI design courses. In Proceedings of the 26th Annual Frontiers in Education (FIE), volume 2, pages 713--716, 1996.
[18]
D. E. Thomas and P. Moorby. The Verilog hardware description language. Kluwer, third edition, 1996.
[19]
Z. Vranesic and S. Brown. Use of HDLs in teaching of computer hardware courses. In Workshop on Computer Architecture Education (WCAE), 2003.
[20]
S. Williams. Icarus Verilog. http://iverilog.icarus.com.

Cited By

View all
  • (2023)FLOD: Full-Lifecycle Online Judge For Accompanying Programming Teaching2023 IEEE International Conference on Teaching, Assessment and Learning for Engineering (TALE)10.1109/TALE56641.2023.10398364(1-8)Online publication date: 28-Nov-2023
  • (2020)Online Judge for FPGA-based Lab Projects in Computer Organization CourseProceedings of the ACM Turing Celebration Conference - China10.1145/3393527.3393531(15-20)Online publication date: 22-May-2020
  • (2018)Jutge.org: Characteristics and ExperiencesIEEE Transactions on Learning Technologies10.1109/TLT.2017.272338911:3(321-333)Online publication date: 1-Jul-2018
  • Show More Cited By

Index Terms

  1. Integrating formal verification in an online judge for e-Learning logic circuit design

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Conferences
      SIGCSE '12: Proceedings of the 43rd ACM technical symposium on Computer Science Education
      February 2012
      734 pages
      ISBN:9781450310987
      DOI:10.1145/2157136
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Sponsors

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 29 February 2012

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. formal verification
      2. logic circuit design
      3. online judge
      4. verilog

      Qualifiers

      • Research-article

      Conference

      SIGCSE '12
      Sponsor:
      SIGCSE '12: The 43rd ACM Technical Symposium on Computer Science Education
      February 29 - March 3, 2012
      North Carolina, Raleigh, USA

      Acceptance Rates

      SIGCSE '12 Paper Acceptance Rate 100 of 289 submissions, 35%;
      Overall Acceptance Rate 1,787 of 5,146 submissions, 35%

      Upcoming Conference

      SIGCSE TS 2025
      The 56th ACM Technical Symposium on Computer Science Education
      February 26 - March 1, 2025
      Pittsburgh , PA , USA

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)9
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 17 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2023)FLOD: Full-Lifecycle Online Judge For Accompanying Programming Teaching2023 IEEE International Conference on Teaching, Assessment and Learning for Engineering (TALE)10.1109/TALE56641.2023.10398364(1-8)Online publication date: 28-Nov-2023
      • (2020)Online Judge for FPGA-based Lab Projects in Computer Organization CourseProceedings of the ACM Turing Celebration Conference - China10.1145/3393527.3393531(15-20)Online publication date: 22-May-2020
      • (2018)Jutge.org: Characteristics and ExperiencesIEEE Transactions on Learning Technologies10.1109/TLT.2017.272338911:3(321-333)Online publication date: 1-Jul-2018
      • (2015)Aiding Teaching of Logic Design and Computer Organization through Dynamic Problem Generation and Automatic Checker Using COLDVL ToolProceedings of the 2015 IEEE Seventh International Conference on Technology for Education (T4E)10.1109/T4E.2015.4(15-22)Online publication date: 10-Dec-2015
      • (2015)Towards an Analytical Framework to Enhance Teaching Support in Digital Systems Design CourseProceedings of the 2015 Ninth International Conference on Complex, Intelligent, and Software Intensive Systems10.1109/CISIS.2015.20(148-155)Online publication date: 8-Jul-2015
      • (2012)Jutge.orgProceedings of the 43rd ACM technical symposium on Computer Science Education10.1145/2157136.2157267(445-450)Online publication date: 29-Feb-2012

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media