Open-source model checkers to provide an alternative to commercial tools for performing formal verification queries.
Provide a layer of abstraction similar to that provided by instruction set architectures, but for arbitrary hardware modules.
Mixed-signal models needed to allow formal techniques to be applied to designs with analog components.
Fully automatic methodology for verifying processor cores or SoC’s that does not require property specification
Clark Barrett
Professor of Computer Science, Stanford University
Aarti Gupta
Professor of Computer Science, Princeton University
Mark Horowitz
Professor of Computer Science and Electrical Engineering, Stanford University
Sharad Malik
Professor of Electrical Engineering, Princeton University
Subhasish Mitra
Professor of Computer Science and Electrical Engineering, Stanford University
Florian Lonsing
Research Scientist, Stanford University
Satisfiability solving, model checking, and formal verification
Makai Mann
PH.D. Candidate, Stanford University
Formal verification
Steven Herbst
PH.D. Candidate, Stanford University
Analog functional modeling and emulation
Sung-Jin Kim
PH.D. Candidate, Stanford University
Open-source high-speed phy
Zach Myers
PH.D. Candidate, Stanford University
Analog functional modeling and open-source high-speed phy
Saranyu Chattopadhyay
Graduate Student, Stanford University
Bo-Yuan Huang
PH.D. Candidate, Princeton University
Hongce Zhang
PH.D. Candidate, Princeton University
Yue Xing
PH.D. Candidate, Princeton University
Huaixi Lu
PH.D. Candidate, Princeton University
Yu Zeng
PH.D. Candidate, Princeton University
Qinhan Tan
PH.D. Candidate, Princeton University
cvc5
Cooperating Validity Checker
An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. cvc5 is the successor of CVC4.
CVC4
Cooperating Validity Checker
CVC4 is an award-winning automatic theorem prover for satisfiability modulo theories (SMT) problems
Boolector
Bitvector solver
Boolector is an award-winning SMT solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions
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
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.
CoSA and CoSA2
CoreIR Symbolic Analyzer
CoSA/CoSA2 is an SMT-based symbolic model checker for hardware designs
ILAng
Instruction Level Abstraction
ILAng is a modeling and verification platform for system-on-chips (SoCs) using instruction level abstractions (ILAs)
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.
Upscale
A repository containing case studies using our tools. The case studies are presented in the following.
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.
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.
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.
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.
Accelerator Quick Error Detection
Artifact demonstrating accelerator quick error detection (A-QED) on several designs
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.
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.
HSLINK_PHY
Verilog functional model for PHY
HSLINK_EMU
Event-driven FPGA emulation model of a high-speed link
AES-ILASIM
Co-simulation model generation demo
Associate Professor (Research) of Computer Science
email: barrett@cs.stanford.edu