Expand description
Spec Encoding: BoundedExpr → Kernel Term
Translates hardware verification expressions from the bounded timestep model into kernel Terms. Under Curry-Howard, these Terms are types — inhabiting them constitutes a proof that the hardware satisfies the specification.
This is the bridge between the SVA verification pipeline and the CoIC kernel.
Functions§
- encode_
bounded_ expr - Encode a BoundedExpr as a kernel Term.