Skip to content

[dv/formal] Relax memory bounds for open source formal flow #2320

@mndstrmr

Description

@mndstrmr

Currently, in the OSS flow all memory operations are assumed to granted/responded to as soon as the protocol allows (immediately for req_o/gnt_i and after one cycle for gnt_i/rvalid_i).

For Jasper we allow anything between the minimum and a 10 cycle delay. Ideally we would do this for the OSS flow too.

In principle this should not be difficult, but it would be reasonable to expect a fairly significant slowdown on some properties, though hopefully not too many.

This may be as simple as just running the flow with relaxed constraints and seeing what happens, or it may require SST work.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Component:DVDesign verification (DV) or testing issueType:EnhancementFeature requests, enhancements

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions