luke
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Added notes.txt

This commit is contained in:
AdvaySingh1 2026-02-12 14:28:37 -08:00
parent e4734e6ca9
commit 0396bf48d1
1 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
notes.txt
View File

@ -292,4 +292,15 @@ Where the MUX has (for the select inputs the input values, and then has random v
SAT returns the combination of the values for d which make this work.
But in this case, how can I go from determining the values of the Ds to determine the gates and converting that to combinational logic? And also, how can I Universially Quantize the other values?
But in this case, how can I go from determining the values of the Ds to determine the gates and converting that to combinational logic? And also, how can I Universially Quantize the other values?
This is difficult due to QBF (Quantified Boolean Format) engines being very expensive and slow.
Rather than this, potentially trying CEGAR (not sure if this is practical). Idea is this:
1. Start with a CANDIDATE solution (guess/abstraction)
2. CHECK: Does candidate work for ALL inputs? (via SAT) (UNSAT for XOR means they are the same)
- If YES → Done, return candidate ✓
- If NO → SAT gives a COUNTEREXAMPLE (inputs where it fails)
3. REFINE: Use counterexample to improve candidate
4. GOTO 2