Skip to content

Formal flow tries to treat a FormalCfg as a SimCfg #133

Closed

Description

@rswarbrick

With the current head of OpenTitan and the current head of dvsim (version 1.17.3), trying to run the formal flow fails in the following way:

Image

Activity

  1. AlexJones0 commented on Apr 1, 2026

    @AlexJones0
    Contributor

    Ah, this one's my fault. I've made a PR to fix it: #139

    Because of our current lack of end-to-end tests for DVSim, this is a consequence of me making changes to improve the reports and only testing on the sim flow.

    The issue is not that the flow tries to treat the FormalCfg as a SimCfg - that is a misnomer in the current Deploy implementation, where from the names and types it seems like it should expect to take a SimCfg, but actually it can take any FlowCfg. Indeed, the OneShotCfg and FormalCfg use it in this way. This part of the code needs refactoring as a whole because of the lack of strict typing and structure, but this issue by itself is fairly easy to fix by just moving the commit computation to the correct location. Also see some discussion in this issue: #119

    This should get rid of this error at least, hopefully I didn't break any other parts of the formal flow. Can you check if this PR works for you?

  2. rswarbrick commented on Apr 2, 2026

    @rswarbrick
    ContributorAuthor

    Upsettingly, there were several other problems here as well. On the plus side, I've just had a happy afternoon hacking on the code in deploy.py and adding type annotations. The problem is fully fixed once the changes in PRs #144, #145, #146, #147, #148, #149, #150, #151, #152, #153, #154, #155, #156, #157, #158, #159, #160 are merged.

    (Yes, this is a ridiculous list! But I think the easiest was to sort out the typing problems was to make Pyright and Ruff happier about the file)

  3. hcallahan-lowrisc commented on Aug 20, 2026

    @hcallahan-lowrisc
    Contributor

    Upsettingly, there were several other problems here as well. On the plus side, I've just had a happy afternoon hacking on the code in deploy.py and adding type annotations. The problem is fully fixed once the changes in PRs #144, #145, #146, #147, #148, #149, #150, #151, #152, #153, #154, #155, #156, #157, #158, #159, #160 are merged.

    (Yes, this is a ridiculous list! But I think the easiest was to sort out the typing problems was to make Pyright and Ruff happier about the file)

    All the listed issues are now closed, hence I'm going to close this one too. Feel free to re-open if it's not fully resolved!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions