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

Fix SMT Memory Bug #1942

Merged
merged 4 commits into from
Nov 10, 2020
Merged

Fix SMT Memory Bug #1942

merged 4 commits into from
Nov 10, 2020

Conversation

ekiwi
Copy link
Contributor

@ekiwi ekiwi commented Nov 9, 2020 •
edited
Loading

This fixes two bugs in the SMT backend:

  • I forgot to scan assert/assume expressions to see if they use memory read ports
  • there was a typo in the code that generates conditions to detect write/write conflicts

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?

Type of Improvement

  • bug fix

API Impact

  • none

Backend Code Generation Impact

  • fixes generated SMTLib/Btor2 representation

Desired Merge Strategy

  • squash

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 a team as a code owner November 9, 2020 19:43
@ekiwi ekiwi requested review from jackkoenig and removed request for a team November 9, 2020 19:43
@ekiwi ekiwi changed the title Fix smt memory bug Fix SMT Memory Bug Nov 9, 2020
@ekiwi ekiwi added the bugfix label Nov 9, 2020
@ekiwi ekiwi added this to the 1.4.0 milestone Nov 9, 2020
@ekiwi
Copy link
Contributor Author

ekiwi commented Nov 9, 2020 •
edited
Loading

@jackkoenig do you know why the Chisel3 tests might be failing?

I am going to rebase and see if it fixes anything,

@ekiwi ekiwi force-pushed the fix-smt-memory-bug branch from 11ff055 to f62336a Compare November 9, 2020 21:06
@jackkoenig
Copy link
Contributor

@jackkoenig do you know why the Chisel3 tests might be failing?

It's known flakiness (but unknown reason why), just restart the test

@ekiwi ekiwi force-pushed the fix-smt-memory-bug branch from f62336a to 456d394 Compare November 9, 2020 22:18
@ekiwi
Copy link
Contributor Author

ekiwi commented Nov 9, 2020

Seems like the Chisel test always exceeds its maximum length (+ it has all the broken pipe warnings).
Since the Chisel tests do not use the smt backend, I am not sure why this is the case for this PR.

I did restart the tests twice by force pushing to the PR branch.

@ekiwi ekiwi force-pushed the fix-smt-memory-bug branch from 456d394 to c55c907 Compare November 10, 2020 00:15
@jackkoenig
Copy link
Contributor

Travis is having issues and pulling resources away from their free open-source offering, that could be related. We probably need to switch to a different CI host anyway and perhaps that can at least workaround this issue. I'll poke around with Github Actions

@ekiwi ekiwi added the Please Merge Accepted PRs that are ready to be merged. Useful when waiting on CI. label Nov 10, 2020
@ekiwi ekiwi added the Backport Automated backport, please consider for minor release label Nov 10, 2020
@mergify mergify bot merged commit 4c6993b into chipsalliance:master Nov 10, 2020
@ekiwi
Copy link
Contributor Author

ekiwi commented Nov 10, 2020

@Mergifyio backport 1.4.x

@jackkoenig jackkoenig removed the Backport Automated backport, please consider for minor release label Nov 10, 2020
mergify bot pushed a commit that referenced this pull request Nov 10, 2020
@ekiwi
Fix SMT Memory Bug (#1942)
2743011 
* smt: add test for write port collision

* smt: add missing call to insertDummyAssignsForMemoryOutputs

* smt: fix typo in write port code

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
(cherry picked from commit 4c6993b)

# Conflicts:
#	src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
@mergify mergify bot mentioned this pull request Nov 10, 2020
Closed
@mergify
Copy link
Contributor

mergify bot commented Nov 10, 2020

Command backport 1.4.x: success

Backports have been created

@ekiwi
Copy link
Contributor Author

ekiwi commented Nov 11, 2020

@Mergifyio backport 1.4.x

@mergify
Copy link
Contributor

mergify bot commented Nov 11, 2020

Command backport 1.4.x: success

Backports have been created

ekiwi added a commit that referenced this pull request Nov 11, 2020
@ekiwi @mergify
Fix SMT Memory Bug (#1942)
c080933 
* smt: add test for write port collision

* smt: add missing call to insertDummyAssignsForMemoryOutputs

* smt: fix typo in write port code

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
mergify bot added a commit that referenced this pull request Nov 11, 2020
@ekiwi @mergify
Fix SMT Memory Bug (#1942) (#1950)
1eb752f 
* smt: add test for write port collision

* smt: add missing call to insertDummyAssignsForMemoryOutputs

* smt: fix typo in write port code

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@azidar azidar azidar approved these changes

@jackkoenig jackkoenig Awaiting requested review from jackkoenig

Assignees
No one assigned
Labels
bugfix Please Merge Accepted PRs that are ready to be merged. Useful when waiting on CI.
Projects
None yet
Milestone
1.4.0
Development

Successfully merging this pull request may close these issues.
3 participants
@ekiwi @jackkoenig @azidar