ISA Modeling with Trace Notation for Context Free Property Generation
TimeWednesday, December 8th11:30am - 11:52am PST
Event Type
Research Manuscript
Virtual Programs
Presented In-Person
Design Verification and Validation
DescriptionThe scalable and extendable RISC-V ISA introduced a new level of flexibility in embedded processor design. However, the required modeling and verification expertise are the major hurdles in leveraging the flexibility provided by the ISA. Formal verification is increasingly used for design verification and the properties are manually written or partially generated. Additional microarchitectural details are added manually, thus increasing the efforts needed.
We propose a trace notation for ISA definition to capture the implicit execution behavior of a processor. The trace notation is annotated with timing and hierarchy information to adapt the trace to any kind of processor architecture.