SAT solver inputs

[gribeill]

Hello!

Is there a convenient way to output the SMT/SAT problems that are solved as part of the Bluespec compilation process?

Thanks!

[rsnikhil]

Shouldn't be too difficult, since bsc is using 3rd party SAT solvers anyway (Yices or STP), i.e., it must be preparing the problems for those solvers anyway.

Hopefully someone else can comment on what's needed to output these separately.

[quark17]

There are trace flags that developers have inserted, for helping to debug the behavior of BSC. One of those is -trace-smt-test, which prints information when queries are made. There's no guarantee that this will dump everything, but I had a quick look and it seems fairly good. (As these are trace output for developers, in theory they could change, so you should not rely on the format of the output; but in practice they haven't changed in a long time.) You could also go into the BSC source and insert more print statements, if you need something that's not being traced.

These traces happen in the modules AExpr2Yices.hs and Pred2Yices.hs (for the Yices solver, or AExpr2STP.hs and Pred2STP.hs for the STP solver ). They correspond to SMT/SAT queries on combinational logic (represented by the AExpr data structure in BSC) and queries on provisos (represented as Pred structures in BSC). To make a query, BSC must convert the AExpr or Pred to the solver's representation, hence the names <rep>2<solver>.

The packages not only convert the BSC structure to the solver structure, but they also export a set of query functions. For AExpr2<solver>, the exported functions are:

• checkDisjointExpr e1 e2 = whether two expressions are mutually exclusive
• checkDisjointRulePair r1 r2 = whether the conditions of two rules are mutually exclusive
• checkBiImplication e1 e2 = whether e1 implies e2 and e2 implies e1
• isConstExpr e = whether an expression is constant True or constant False and which
• checkEq e1 e2 = whether two expressions are equal
• checkNotEq e1 e2 = whether two expressions are not equal

For Pred2<solver>, the exported function is:

• solvePred given_preds query_pred = whether a proviso in question is implied by the provisos already in hand

The trace-smt-test flag will indicate which of those exported functions are being called and what the arguments are. There is also a flag trace-smt-conv that may give some more detail about the conversion from AExpr/Pred to the solver representation. If you want to know the specific C API calls being made to the solver, though, that's not being dumped -- but you could insert trace statements in the BSC source to do that.

FYI, the SMT/SAT solvers are imported in three abstraction layers:

1. The C API for the solvers (Yices and STP) is imported directly into Haskell, in src/vendor/yices/v2.6/HaskellIfc/ and src/vendor/stp/HaskellIfc/.
2. The modules src/comp/AExpr2Yices.hs and src/comp/Pred2Yices.hs (or AExpr2STP.hs and Pred2STP.hs) use that imported API to provide the higher level functions.
3. The separate AExpr2Yices.hs and AExpr2STP.hs are combined into a single SAT.hs module which provides the same higher level functions (and just dispatches the call to the specific solver). Similarly, Pred2Yices.hs and Pred2STP.hs are combined into SATPred.hs.

These SAT.hs and SATPred.hs libraries are called in four places inside BSC:

1. ADumpSchedule.hs = uses checkEq from SAT to identify rules/methods that are never ready
2. AOpt.hs = can use checkBiImplication and isConstExpr from SAT to simplify logic in the Verilog backend
3. AProof.hs = uses checkEq and checkNotEq from SAT to test assertions, such as when a method needs to be always enabled (the sum of the EN signals from all the users must be constant True) or always ready (the RDY expression must be constant True)
4. TCMisc.hs = uses SATPred to reduce numeric provisos

[gribeill]

Wow, thank you so much for this incredibly detailed reply! This should get me started.

[rsnikhil]

Please do let us know (if it is not proprietary), briefly, what you're planning to do with this! We like to keep abreast of the BSV/BH/bsc compiler community's activities.

[gribeill]

This is actually only peripherally related to bsc (other than my being a big fan of Bluespec!) -- we are working on some SAT solving hardware, and it's useful to have "real-world" examples of problems at various scales to use to test the system.