Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Formal] Expose Btor2 target #4035

Merged
merged 12 commits into from
May 16, 2024
Merged

Conversation

dobios
Copy link
Member

@dobios dobios commented May 1, 2024

This PR exposes the btor2 target in Chisel. This is done through an emitBtor2 method in ChiselStage.
This currently depends on a CIRCT PR to support AssertProperty.

Contributor Checklist

  • Did you add Scaladoc to every public function/method?
  • Did you add at least one test demonstrating the PR?
  • Did you delete any extraneous printlns/debugging code?
  • Did you specify the type of improvement?
  • Did you add appropriate documentation in docs/src?
  • Did you request a desired merge strategy?
  • Did you add text to be included in the Release Notes for this change?

Type of Improvement

  • Feature (or new API)

Desired Merge Strategy

  • Squash: The PR will be squashed and merged (choose this if you have no preference).

Release Notes

  • [Formal] Allow for Chisel to be compiled to btor2 for Bounded Model Checking using ChiselStage.emitBtor2.

Reviewer Checklist (only modified by reviewer)

  • Did you add the appropriate labels? (Select the most appropriate one based on the "Type of Improvement")
  • Did you mark the proper milestone (Bug fix: 3.6.x, 5.x, or 6.x depending on impact, API modification or big change: 7.0)?
  • Did you review?
  • Did you check whether all relevant Contributor checkboxes have been checked?
  • Did you do one of the following when ready to merge:
    • Squash: You/ the contributor Enable auto-merge (squash), clean up the commit message, and label with Please Merge.
    • Merge: Ensure that contributor has cleaned up their commit history, then merge with Create a merge commit.

Copy link

linux-foundation-easycla bot commented May 1, 2024

CLA Signed

The committers listed above are authorized under a signed CLA.

Copy link
Member

@sequencer sequencer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! can't wait to use this feature! My repo haven't go though the formal pass since I upgrade to chisel5.

src/test/scala/circtTests/stage/ChiselStageSpec.scala Outdated Show resolved Hide resolved
@dobios dobios marked this pull request as ready for review May 1, 2024 23:14
@dobios
Copy link
Member Author

dobios commented May 3, 2024

The blocking PR has been merged in and should be included in the next firtool release, which would make this work.

@jackkoenig jackkoenig added the Feature New feature, will be included in release notes label May 3, 2024
@jackkoenig jackkoenig added this to the 7.0 milestone May 3, 2024
@dobios dobios changed the title [Formal] Exposed Btor2 target [Formal] Expose Btor2 target May 16, 2024
@dobios
Copy link
Member Author

dobios commented May 16, 2024

The new firtool release now supports everything that is needed for this PR!

Copy link
Contributor

@jackkoenig jackkoenig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great! Awesome work.

@jackkoenig jackkoenig enabled auto-merge (squash) May 16, 2024 23:00
@jackkoenig jackkoenig merged commit dce2fe8 into chipsalliance:main May 16, 2024
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Feature New feature, will be included in release notes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants