vericert.Compiler

• Compiler Proof
  • Imports
  • Declarations
    • Top-level Translation
  • Correctness Proof
    • Backward Simulation

vericert.Simulator

vericert.HLSOpts

vericert.common.IntegerExtra

vericert.common.Maps

vericert.common.Monad

vericert.common.Show

vericert.common.Statemonad

vericert.common.Vericertlib

vericert.common.ZExtra

vericert.hls.Abstr

• • Schedule Oracle

vericert.hls.Array

vericert.hls.AssocMap

vericert.hls.FunctionalUnits

vericert.hls.HTL

• Operational Semantics

vericert.hls.HTLBlockgen

vericert.hls.HTLPargen

vericert.hls.HTLgen

vericert.hls.HTLgenproof

vericert.hls.HTLgenspec

• Relational specification of the translation

vericert.hls.HashTree

vericert.hls.IfConversion

• If conversion

vericert.hls.Memorygen

vericert.hls.Pipeline

vericert.hls.PipelineOp

vericert.hls.Predicate

vericert.hls.RTLBlock

vericert.hls.RTLBlockInstr

• RTLBlock Instructions
  • Instruction Definition
  • Control-Flow Instruction Definition
  • Helper functions
    • Instruction State
  • Top-Level Type Definitions
  • Semantics

vericert.hls.RTLBlockgen

vericert.hls.RTLPar

vericert.hls.RTLParFU

vericert.hls.RTLParFUgen

vericert.hls.RTLPargen

• RTLPar Generation
  • Abstract Computations
    • Update Function
  • Top-level Functions

vericert.hls.RTLPargenproof

vericert.hls.Sat

• Problem Definition
• Subroutines
• The SAT Solver

vericert.hls.Value

vericert.hls.ValueInt

• Value
  • Value conversions
  • Arithmetic operations

vericert.hls.ValueVal

• Value

vericert.hls.Verilog

• • Verilog AST
    • Value
    • Binary Operators
    • Unary Operators
    • Expressions
    • Statements
    • Edges
    • Module Items
    • State

vericert.hls.Veriloggen

vericert.hls.Veriloggenproof

vericert.bourdoncle.Bourdoncle