Skip to content
This repository has been archived by the owner on Aug 20, 2024. It is now read-only.

smt: add support for uninterpreted ext modules #1994

Merged
merged 2 commits into from
Dec 2, 2020

Conversation

ekiwi
Copy link
Contributor

@ekiwi ekiwi commented Dec 1, 2020

Contributor Checklist

  • Did you add Scaladoc to every public function/method?
  • n/a Did you update the FIRRTL spec to include every new feature/behavior?
  • 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 state the API impact?
  • Did you specify the code generation impact?
  • Did you request a desired merge strategy?
  • Did you add text to be included in the Release Notes for this change?

Type of Improvement

  • new feature/API

API Impact

  • adds a new UninterpretedModuleAnnotation which is consumed by the SMT backend to model ExtModules with uninterpreted functions / constant arrays

Backend Code Generation Impact

  • uses UninterpretedFunctions in the SMTLib backend
  • uses constant arrays for the btor2 backend

Desired Merge Strategy

  • squash

Release Notes

The SMT backend now has support for modelling with uninterpreted functions using the UninterpretedModuleAnnotation.

Reviewer Checklist (only modified by reviewer)

  • Did you add the appropriate labels?
  • Did you mark the proper milestone (1.2.x, 1.3.0, 1.4.0) ?
  • Did you review?
  • Did you check whether all relevant Contributor checkboxes have been checked?
  • Did you mark as Please Merge?

@ekiwi ekiwi requested a review from azidar December 1, 2020 23:22
@ekiwi ekiwi added this to the 1.4.x milestone Dec 2, 2020
@ekiwi ekiwi added the Please Merge Accepted PRs that are ready to be merged. Useful when waiting on CI. label Dec 2, 2020
ekiwi added a commit to ekiwi/paso that referenced this pull request Dec 2, 2020
@mergify mergify bot merged commit 228878e into chipsalliance:master Dec 2, 2020
mergify bot pushed a commit that referenced this pull request Dec 2, 2020
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
(cherry picked from commit 228878e)
@mergify mergify bot added the Backported This PR has been backported to marked stable branch label Dec 2, 2020
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
Backported This PR has been backported to marked stable branch Please Merge Accepted PRs that are ready to be merged. Useful when waiting on CI.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants