Upscale

Scaling Up Formal Tools for

POSH Open Source Hardware















The goal of the POSH Upscale Project is to develop tools and techniques for verifying and evaluating open-source hardware. Modern Systems-on-Chip (SoCs) pose two distinct challenges to this endeavor. The first is increasing heterogeneity. SoCs comprise a range of programmable processors (CPUs, GPUs, other domain specific processors), dedicated hardware function blocks (accelerators, memory controllers, on-chip networks and buses), and analog/mixed-signal (AMS) components. The second is differing levels of abstraction used across these components in verification tools—instruction-level hardware-software interfaces for processors, register-transfer level finite state machine models for other digital modules, and circuit-level models for AMS components.




FORMAL METHODS


Open-source model checkers to provide an alternative to commercial tools for performing formal verification queries.




INSTRUCTION-LEVEL ABSTRACTIONS


Provide a layer of abstraction similar to that provided by instruction set architectures, but for arbitrary hardware modules.




MIXED-SIGNAL MODELS


Mixed-signal models needed to allow formal techniques to be applied to designs with analog components.




QUICK ERROR DETECTION


Fully automatic methodology for verifying processor cores or SoC’s that does not require property specification

PEOPLE
person

Clark Barrett

Professor of Computer Science, Stanford University

person

Aarti Gupta

Professor of Computer Science, Princeton University

person

Mark Horowitz

Professor of Computer Science and Electrical Engineering, Stanford University

person

Sharad Malik

Professor of Electrical Engineering, Princeton University

person

Subhasish Mitra

Professor of Computer Science and Electrical Engineering, Stanford University


RESEARCH SCIENTISTS AND POSTDOCTORAL RESEARCHERS
person

Florian Lonsing

Research Scientist, Stanford University

Satisfiability solving, model checking, and formal verification


GRADUATE STUDENTS
person

Makai Mann

PH.D. Candidate, Stanford University

Formal verification

person

Steven Herbst

PH.D. Candidate, Stanford University

Analog functional modeling and emulation

person

Sung-Jin Kim

PH.D. Candidate, Stanford University

Open-source high-speed phy

person

Zach Myers

PH.D. Candidate, Stanford University

Analog functional modeling and open-source high-speed phy

person

Saranyu Chattopadhyay

Graduate Student, Stanford University

person

Bo-Yuan Huang

PH.D. Candidate, Princeton University

person

Hongce Zhang

PH.D. Candidate, Princeton University

person

Yue Xing

PH.D. Candidate, Princeton University

person

Huaixi Lu

PH.D. Candidate, Princeton University

person

Yu Zeng

PH.D. Candidate, Princeton University

person

Qinhan Tan

PH.D. Candidate, Princeton University


TOOLS
tool

cvc5

Cooperating Validity Checker

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. cvc5 is the successor of CVC4.

View cvc5 on GitHub

tool

CVC4

Cooperating Validity Checker

CVC4 is an award-winning automatic theorem prover for satisfiability modulo theories (SMT) problems

View CVC4 on GitHub

tool

Boolector

Bitvector solver

Boolector is an award-winning SMT solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions

View Boolector on GitHub

tool

Pono

SMT-based model checker

Pono is a flexible and extensible SMT-based model checker that leverages word-level reasoning (“pono” is the Hawaiian word for proper, correct, or goodness).

Pono is the successor of our previous model checkers CoSA and CoSA2

View Pono on GitHub

tool

Smt-Switch

A solver-agnostic C++ API for SMT solving

Smt-Switch provides abstract C++ classes which can be implemented by different SMT solvers. Our model checker Pono is built using Smt-Switch.

View Smt-Switch on GitHub

tool

CoSA and CoSA2

CoreIR Symbolic Analyzer

CoSA/CoSA2 is an SMT-based symbolic model checker for hardware designs

Please consider our latest SMT-based model checker Pono

View CoSA on GitHub

View CoSA2 on GitHub

tool

ILAng

Instruction Level Abstraction

ILAng is a modeling and verification platform for system-on-chips (SoCs) using instruction level abstractions (ILAs)

View ILAng on GitHub

tool

DaVE

Methodologies and tools for analog function modeling

Today it is difficult to validate a System-on-Chip which contains analog components (is mixed signal). The problem is that the analog and digital subsystems are usually strongly intertwined so they must be validated as a system, but the validation approaches for analog and digital blocks are completely different. We address this problem by creating high-level functional models of analog components, which is compatible with top-level digital system validation, and then provide a method of formal checking to ensure that these functional models match the operation of the transistor level implementations of these blocks. We provide a set of methodologies and tools for this analog functional modeling, the core part for enabling our Digital Analog Design. Our modeling methodology consists of three core technologies: mLingua, a modeling language in SystemVerilog, mProbo, a model checker, and mGenero, a model generator.

View DaVE on GitHub


CASE STUDIES, DEMOS, AND TUTORIALS
tool

Upscale

A repository containing case studies using our tools. The case studies are presented in the following.

tool

AXI Protocol Checker

An easy-to-use AXI protocol checker using CoSA for model checking. This case study uses the OH! implementation of the AXI protocol.

tool

SQED Demo using RIDECORE

A tutorial for setting up Symbolic Quick Error Detection (SQED) using the open-source, SMT-based model checker CoSA. This tutorial shows how a bug was discovered in the multiply decoder of the RIDECORE Out of Order RISC-V Processor using SQED.

tool

Generic SQED Demo

This demo shows how to apply symbolic QED to RIDECORE, a RISC-V core, using a generic QED module. The generic QED module reduces the amount of manual work to be done by the verification engineer.

tool

Single instruction checking for RIDECORE

An implementation of single instruction checking for the RIDECORE Out of Order RISC-V Processor. Single instruction checking is complementary to SQED.

tool

Accelerator Quick Error Detection

Artifact demonstrating accelerator quick error detection (A-QED) on several designs

tool

ILAng Demo

This example demonstrates the use of Instruction-level Abstraction (ILA) for formally specifying hardware designs and checking the equivalence between implementation and specification. The demo artifact contains (i) the ILA model of an AES accelerator, (ii) the RTL implementation, and (iii) the refinement relation. From the above inputs, ILAng generates the verification targets and properties, which are then checked by CoSA.

tool

Asynchronous FIFO

This case study is based on a generic asynchronous FIFO developed by Andreas Olofsson. The FIFO has parameterized length and width of the data. It is asynchronous since it has two separate clocks for pushing (write) and popping (read) data. This case study is representative for the verification of safety properties using CoSA and SQED.

tool

HSLINK_PHY

Verilog functional model for PHY

tool

HSLINK_EMU

Event-driven FPGA emulation model of a high-speed link

tool

AES-ILASIM

Co-simulation model generation demo

SELECTED PUBLICATIONS AND AWARDS
Awards
  • 2021 DATE Best Paper Award
    • Recipients: Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik
    • Article: Leveraging Processor Modeling and Verification for General Hardware Modules
    • Publication: Design, Automation and Test in Europe Conference and Exhibition (DATE)
    • Awarded at DATE 2021 and announced at https://www.date-conference.com/awards

  • 2020 Honorable Mention at Formal Methods in Computer-Aided Design
    • Recipients: Florian Lonsing, Subhasish Mitra, and Clark Barrett
    • Article: A Theoretical Framework for Symbolic Quick Error Detection
    • Publication: Proceedings of Formal Methods in Computer-Aided Design (FMCAD)
    • Awarded at FMCAD 2020 and announced at: https://fmcad.forsyte.at/FMCAD20/awards/

  • 2020 ACM Transactions on Design Automation of Electronic Systems Best Paper Award
    • Recipients: Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, and Sharad Malik
    • Article: Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification
    • Publication: Volume 24, Issue 1, Article 10, January 2019
    • Awarded at DAC 2020 and announced at: https://dl.acm.org/journal/todaes/honors-and-awards

  • 2019 Oski Award at HWMCC 2019
    • Recipients: Makai Mann, Ahmed Irfan, Florian Lonsing, and Clark Barrett
    • Tool: CoSA2 model checker, for solving the largest number of benchmarks overall
    • Event: Hardware Model Checking Competition (HWMCC) 2019
    • Awarded at FMCAD 2019 and announced at: http://fmv.jku.at/hwmcc19/


Instruction level abstractions
  • Y. Xing, H. Lu, A. Gupta, and S. Malik, “Leveraging Processor Modeling and Verification for General Hardware Modules,” in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2021. DATE 2021 Best Paper Award
  • H. Zhang, A. Gupta, and S. Malik, “Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking,” in 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2021.
  • H. Zhang, W.Yang, G. Fedyukovich, A. Gupta, and S. Malik, “Synthesizing Environment Invariants for Modular Hardware Verification,” in 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2020.
  • B.-Y. Huang, H. Zhang, A. Gupta, and S. Malik, "ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions," in 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019.
  • B.-Y. Huang, H. Zhang, P. Subramanyan, Y. Vizel, A. Gupta, and S. Malik, "Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification," in ACM Transaction on Design Automation of Electronic Systems (TODAES), vol. 24, no. 10, pp. 10:1-10:24, Jan. 2019. 2020 ACM TODAES Best Paper Award
  • Y. Xing, B.-Y. Huang, A. Gupta, and S. Malik, "A Formal Instruction-Level GPU Model for Scalable Verification," in Proceedings of International Conference on Computer-Aided Design (ICCAD), 2018.
  • H. Zhang, C. Trippel, Y. A. Manerkar, A. Gupta, M. Martonosi, and S. Malik, "ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification," in Proceedings of Formal Methods in Computer Aided Design (FMCAD), 2018.
  • B.-Y. Huang, S. Ray, A. Gupta, J. M. Fung, and S. Malik,"Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware," in Proceedings of 55th ACM/ESDA/IEEE Design Automation Conference (DAC), 2018.
  • P. Subramanyan, B.-Y. Huang, Y. Vizel, A. Gupta, and S. Malik, "Template-based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 37, no. 8, pp. 1692-1705, 2018.
  • S. Malik and P. Subramanyan,"Specification and Modeling for Systems-on-Chip Security Verification," in Proceedings of 53th ACM/EDAC/IEEE Design Automation Conference (DAC), 2016.
  • P. Subramanyan, S. Malik, H. Khattri, A. Maiti, and J. Fung,"Verifying Information Flow Properties of Firmware using Symbolic Execution," in Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016.
  • P. Subramanyan, Y. Vizel, S. Ray, and S. Malik,"Template-based Synthesis of Instruction-Level Abstraction for SoC Verification", in Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD), 2015.


Functional modeling and validating analog functional models
  • B. C. Lim and M. Horowitz, "An Analog Model Template Library: Simplifying Chip-Level, Mixed-Signal Design Verification," in IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 27, no. 1, pp. 193-204, Jan. 2019.
  • S. Herbst, B. C. Lim, and M. Horowitz. 2018. Fast FPGA emulation of analog dynamics in digitally-driven systems. In Proceedings of the International Conference on Computer-Aided Design (ICCAD '18). ACM, New York, NY, USA, Article 131, 8 pages.
  • B. C. Lim and M. Horowitz, "Error Control and Limit Cycle Elimination in Event-Driven Piecewise Linear Analog Functional Models," in IEEE Transactions on Circuits and Systems I: Regular Papers, vol. 63, no. 1, pp. 23-33, Jan. 2016.
  • B. C. Lim, J. Jang, J. Mao, J. Kim and M. Horowitz, "Digital Analog Design: Enabling Mixed-Signal System Validation," in IEEE Design & Test, vol. 32, no. 1, pp. 44-52, Feb. 2015.


Symbolic quick error detection
  • S. Chattopadhyay, F. Lonsing, L. Piccolboni, D. Soni, P. Wei, X. Zhang, Y. Zhou, L. P. Carloni, D. Chen, J. Cong, R. Karri, Z. Zhang, C. Trippel, C. W. Barrett, S. Mitra: Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD) 2021: 42-52.
  • E. Singh, F. Lonsing, S. Chattopadhyay, M. Strange, P. Wei, X. Zhang, Y. Zhou, D. Chen, J. Cong, P. Raina, Z. Zhang, C. Barrett, S. Mitra: A-QED Verification of Hardware Accelerators. In Proceedings of Design Automation Conference (DAC), ACM/IEEE, 2020.
  • F. Lonsing, S. Mitra, C. Barrett: A Theoretical Framework for Symbolic Quick Error Detection. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD) 2020: 1-10. FMCAD 2020 Honorable Mention
  • F. Lonsing, K. Ganesan, M. Mann, S. S. Nuthakki, E. Singh, M. Srouji, Y. Yang, S. Mitra, C. Barrett: Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper. In Proceedings of International Conference on Computer-Aided Design (ICCAD) 2019: 1-8.
  • M. R. Fadiheh, J. Urdahl, S. S. Nuthakki, S. Mitra, C. Barrett, D. Stoffel, W. Kunz: Symbolic quick error detection using symbolic initial state for pre-silicon verification. In Proceedings of Design, Automation, and Test (DATE), IEEE, 2018.
  • E. Singh, C. Barrett, S. Mitra: E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods. In Proceedings of Computer Aided Verification (CAV) (2), LNCS, Springer, 2017.
  • E. Singh, D. Lin, C. Barrett, S. Mitra: Symbolic Quick Error Detection for Pre-Silicon and Post-Silicon Validation: Frequently Asked Questions. IEEE Design & Test 33(6): 55-62 (2016).
  • D. Lin, E. Singh, C. Barrett, S. Mitra: A structured approach to post-silicon validation and debug using symbolic quick error detection. In Proceedings of International Test Conference (ITC), IEEE, 2015.


Model checking
  • M. Mann, A. Irfan, A. Griggio, O. Padon, C. Barrett: Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Springer, 2021.
  • M. Mann, A. Wilson, Y. Zohar, L. Stuntz, A. Irfan, K. Brown, C. Donovick, A. Guman, C. Tinelli, C. Barrett: Smt-Switch: A Solver-agnostic C++ API for SMT Solving. In Proceedings of Theory and Applications of Satisfiability Testing (SAT), LNCS, Springer, 2021.
  • M. Mann, A. Irfan, F. Lonsing, Y. Yang, H. Zhang, K. Brown, A. Gupta, C. Barrett: Pono: A Flexible and Extensible SMT-based Model Checker. In Proceedings of Computer Aided Verification (CAV), LNCS, Springer, 2021.
  • M. Mann, C. Barrett: Partial Order Reduction for Deep Bug Finding in Synchronous Hardware. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, Springer, 2020.
  • C. Mattarei, M. Mann, C. Barrett, R. G. Daly, D. Huff, P. Hanrahan: CoSA: Integrated Verification for Agile Hardware Design. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD), IEEE, 2018.
CONTACT




Prof. Clark Barrett



Associate Professor (Research) of Computer Science

email: barrett@cs.stanford.edu


COPYRIGHT © 2018-2021. ALL RIGHTS RESERVED.