1074: Automated Generation of Interval Properties From Trace-Based Function Models

Function set modeling is a specification methodology striving for the unified description of general hardware systems. Based on the Instruction Set Architecture (ISA) of processors, function set modeling specifies systems exclusively by their executable functions and the relevant system state. While this methodology has been used in formal verification and behavioral modeling, the abstraction gap between system-level function models and design implementation limits its significance. We use traces, time-annotated representations of functions, to additionally model architecture parameters. Hierarchical State Machines (HSMs) are leveraged as a notation to capture the refined and conditional execution of the underlying function set. Moreover, we show the transformation of traces into formal assertion properties spanning over fixed-length intervals. The extracted interval set jointly verifies the complete behavior captured by the traces, thereby checking the functional and temporal correctness of the Design Under Verification (DUV).