bsc regression with custom enums

[czeck]

I have a bsc regression introduced in rev: 629c10a Custom enums (#298).

We have a pattern where we define enums as one-hot and use a custom Eq instance to obtain the one-hot encoding in verilog/rtl. This technique was sufficient to have the scheduler understand that rule scheduling based on one-hot enum are disjoint. With the above commit, the scheduler not longs sees disjoint rules as expected.

A failing test case is attached and it be run with
bsc -v --verilog CheckSum.bsv

Any ideas on work-arounds to redefine this this type or its Bits class? The code of interest shown

typedef enum {
              Accum        = 1
              ,Finalize1   = 2
              ,Finalize2   = 4
   } CS4Mode
deriving (Bits, FShow);

function Bool oneHotEquality (t a, t b)
   provisos (Bits#(t, st));
   Vector#(st, Bool) av = unpack(pack(a));
   Vector#(st, Bool) bv = unpack(pack(b));
   Vector#(st, Bool) anded = zipWith( \&& ,av, bv);
   return any(id, anded);
endfunction

instance Eq#(CS4Mode);
   function \== = oneHotEquality;
endinstance

checksum.zip

[quark17]

I asked @nanavati to have a look at this and he said:

I took a quick look and concluded this was an expected side effect of the change. Properly optimizing away "pack . unpack" means that you can't count on it to restrict values to legal bit patterns the way that the one-hot code does. Note that the innermost unpack in the chain of operations is implicit because that how you get from a register or other hardware bit pattern to the user-defined type in the first place.

I think the right solution is probably to manually write the old instances or to explicitly inject some sort of legalization function that removes illegal patterns (or transforms them to undefined values).

As he says, there are two workarounds. One is, where you are calling unpack(pack(a)) apply an explicitly written function that legalizes the values. The code pack(a) is actually pack(unpack(a_raw)) (as Ravi notes) when a comes from a state element. And BSC's old behavior was for pack(unpack(x)) to insert extra (often unwanted) logic to guarantee that the packed value is legal even if the original x was not (see below). Now that BSC is not doing that, you can workaround it by doing that explicitly.

Alternatively, if you want to continue using the Bits instance to do this legalizing for you, then you can stop deriving Bits and define it explicitly. I found, for example, that writing it like this works:

instance Bits#(CS4Mode,3);
  function pack (x);
    case (x) matches
      Accum : return 1;
      Finalize1 : return 2;
      Finalize2 : return 4;
    endcase
  endfunction
  function unpack (x);
    case (x)
      1: return Accum;
      2: return Finalize1;
      default: return Finalize2;  // <--
    endcase
  endfunction
endinstance

I tried the following, which I thought might work, but it didn't:

  function unpack (x);
    case (x)
      1: return Accum;
      2: return Finalize1;
      4: return Finalize2;
      default: return ?;
    endcase
  endfunction

The change in BSC was to delay the handling of the case-statement fall-through, so pack(unpack(bs)) would reduce to just bs and not reduce to if_legal(bs) ? bs : legalized_value. Implicitly inserting this legalizing introduced extra code in places that people didn't want -- for example, when you're just moving a value from one register (or state element) to another. If these one-hot values are being stored in state and moved around, you may want to keep BSC's new derived Bits instance, so that you get good code-gen in the places in the design that don't need to check for validity; you'd then define a legalizing function and call it explicity in the places where you do want that behavior.

[czeck]

I much prefer the new pack/unpack behavior, and it does not introduce useless logic transformations. However its interaction with rule scheduling is really the primary issue with this change. In general I am looking for a solution that provides the following: 1) A true one-hot verilog generation as logic timing is critical. 2) Scheduler understands mutually exclusion of state -- (reduce logic) 3) Would like to keep the new pack/unpack behavior -- (reduce logic) 4) We are willing to use verilog post processing to achieve this. I tried using the OInt package, and found that while the generated verilog is one-hot, the scheduler does not understand that rules are mutually exclusive. Are there other ideas I can try to nudge the scheduler into understanding one-hot encodings? Thanks, Ed.

…

On Sun, Oct 3, 2021 at 7:15 PM Julie Schwartz ***@***.***> wrote: I asked @nanavati <https://github.com/nanavati> to have a look at this and he said: I took a quick look and concluded this was an expected side effect of the change. Properly optimizing away "pack . unpack" means that you can't count on it to restrict values to legal bit patterns the way that the one-hot code does. Note that the innermost unpack in the chain of operations is implicit because that how you get from a register or other hardware bit pattern to the user-defined type in the first place. I think the right solution is probably to manually write the old instances or to explicitly inject some sort of legalization function that removes illegal patterns (or transforms them to undefined values). As he says, there are two workarounds. One is, where you are calling unpack(pack(a)) apply an explicitly written function that legalizes the values. The code pack(a) is actually pack(unpack(a_raw)) (as Ravi notes) when a comes from a state element. And BSC's old behavior was for pack(unpack(x)) to insert extra (often unwanted) logic to guarantee that the packed value is legal even if the original x was not (see below). Now that BSC is not doing that, you can workaround it by doing that explicitly. Alternatively, if you want to continue using the Bits instance to do this legalizing for you, then you can stop deriving Bits and define it explicitly. I found, for example, that writing it like this works: instance Bits#(CS4Mode,3); function pack (x); case (x) matches Accum : return 1; Finalize1 : return 2; Finalize2 : return 4; endcase endfunction function unpack (x); case (x) 1: return Accum; 2: return Finalize1; default: return Finalize2; // <-- endcase endfunction endinstance I tried the following, which I thought might work, but it didn't: function unpack (x); case (x) 1: return Accum; 2: return Finalize1; 4: return Finalize2; default: return ?; endcase endfunction The change in BSC was to delay the handling of the case-statement fall-through, so pack(unpack(bs)) would reduce to just bs and not reduce to if_legal(bs) ? bs : legalized_value. Implicitly inserting this legalizing introduced extra code in places that people didn't want -- for example, when you're just moving a value from one register (or state element) to another. If these one-hot values are being stored in state and moved around, you may want to keep BSC's new derived Bits instance, so that you get good code-gen in the places in the design that don't need to check for validity; you'd then define a legalizing function and call it explicity in the places where you do want that behavior. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#417 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB24HQGDJEENW2J7UFSYCP3UFDPXPANCNFSM5EWXZXIQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[quark17]

Ok, I'm starting to realize that the enum and pack/unpack are a bit of red-herring. And I do wonder, did this actually work before?

If one rule has the condition mode_r[0] and another rule has the condition mode_r[1], then BSC has to conclude that the rules might be enabled at the same time, because it doesn't know that the register will never contain more than one asserted bit.

This scheduling analysis is done after elaboration, so changes in how BSC handles pack/unpack of the data type really has nothing to do with it -- it's knowledge about the contents of that register, and there's never been a way to tell BSC that.

So how then could BSC previously notice that the rules were exclusive? I believe it's because BSC was not producing one-hot Verilog! I'm seeing that it produced this:

  always@(mode_r)
  begin
    case (mode_r)
      3'd1, 3'd2:
	  IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = mode_r;
      default: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 =
		   3'd4;
    endcase
  end

  assign RDY_accum =
	     IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10[0] ;

The change in scheduling behavior is because BSC is only now generating the one-hot extraction that we expect. I confirm this by dumping the ATS prior to scheduling with -dATS. And I rewrote the example to use OInt and I see that -dATS shows that it too produces the one-hot extraction.

So the question is what can we do to help the scheduler see that mode_r[0] and mode_r[1] are exclusive expressions (and not anything to with enums or pack/unpack or anything during elaboration or earlier).

I've always thought that it would be useful to have a syntax for telling BSC some equations that it can assume to be true -- which BSC could then add to its SMT analysis. For example, if a module has two inputs X and Y and they are known to never be the same value, you might want to assert to BSC that "x != y". If we had this facility, it could be used to tell BSC that the bits of the mode_r register are exclusive. (We may not have to write this explicitly; we could define a "onehot" attribute, that BSC desugars into SMT information for one-hot-ness. This attribute may not even be needed explicitly from the user, if it's part of the OInt library or otherwise appears automatically inside certain modules or types.)

Of course, it might also be nice if BSC could figure these equations out on its own. For example, some basic model checking could detect that the register is only ever written with one-hot values. (This analysis may be too much to perform on every register, so an attribute could be used to tell BSC to consider it for this register.) However, if values are coming in from outside the current module boundary, then BSC would not be able to check this when code-generating for this module, but would have to check it later, when BSC has the full design. (We'd also have to make sure that we're taking reset values -- and lack of reset values -- into account.)

I was trying to think about whether (as another alternative) you could encode the exclusive-ness in the scheduling annotations of an imported Verilog module -- say, a OIntReg module with separate methods for each bit. But I don't believe that BSC currently supports any attributes that would communicate mutual-exclusion.

[czeck]

Thanks for the response. I have some thoughts on how we add constraints for the SMT solver and I see a big value in that. I'll add those in another thread sometime later. Currently I am working on using the 21.07 bsc release with our current codebase and looking for a work-around to the change in the pack/unpack behavior. Specifically I am attempting to revert to the previous Bits behavior for some one-hot enum types. One-hot enums require 2 things -- a one-hot encoding and a equality test that depends on the one-hot encoding. In code for this is as follows and worked until the pack/unpack change. typedef enum {E0 = 1 ,E1 = 2 ,E2 = 4 } OHE4 deriving (FShow, Bits); instance Eq#(OHE4); function Bool \== (OHE4 a, OHE4 b) provisos (Bits#(OHE4, st)); Bit#(st) ab = pack(a); Bit#(st) bb = pack(b); Vector#(st, Bool) av = unpack(pack(a)); Vector#(st, Bool) bv = unpack(pack(b)); Vector#(st, Bool) anded = zipWith( \&& ,av, bv); return any(id, anded); endfunction endinstance If I define and new instances of Bits as @nanavati suggested. E.g. instance Bits#(OHE4, 3); function Bit#(3) pack(OHE4 e); return case (e) E0 : return 1; E1 : return 2; E2 : return 4; //default:return 0; endcase; endfunction function OHE4 unpack(Bit#(3) b); return case (b) 1: return E0; 2: return E1; 4: return E2; //default: return ?; endcase; endfunction endinstance I end up with a circular dependency that is, pack() requires ==() and ==() require pack(). Question: Any idea how I can get have both a custom Bits and a custom Eq instance? One I have these, the scheduling and verilog problem have been solved. Thanks

…

On Mon, Oct 4, 2021 at 11:30 PM Julie Schwartz ***@***.***> wrote: Ok, I'm starting to realize that the enum and pack/unpack are a bit of red-herring. And I do wonder, did this actually work before? If one rule has the condition mode_r[0] and another rule has the condition mode_r[1], then BSC has to conclude that the rules might be enabled at the same time, because it doesn't know that the register will never contain more than one asserted bit. This scheduling analysis is done after elaboration, so changes in how BSC handles pack/unpack of the data type really has nothing to do with it -- it's knowledge about the contents of that register, and there's never been a way to tell BSC that. So how then could BSC previously notice that the rules were exclusive? I believe it's because BSC was *not* producing one-hot Verilog! I'm seeing that it produced this: always@(mode_r) begin case (mode_r) 3'd1, 3'd2: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = mode_r; default: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = 3'd4; endcase end assign RDY_accum = IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10[0] ; The change in scheduling behavior is because BSC is only now generating the one-hot extraction that we expect. I confirm this by dumping the ATS prior to scheduling with -dATS. And I rewrote the example to use OInt and I see that -dATS shows that it too produces the one-hot extraction. So the question is what can we do to help the scheduler see that mode_r[0] and mode_r[1] are exclusive expressions (and not anything to with enums or pack/unpack or anything during elaboration or earlier). I've always thought that it would be useful to have a syntax for telling BSC some equations that it can assume to be true -- which BSC could then add to its SMT analysis. For example, if a module has two inputs X and Y and they are known to never be the same value, you might want to assert to BSC that "x != y". If we had this facility, it could be used to tell BSC that the bits of the mode_r register are exclusive. (We may not have to write this explicitly; we could define a "onehot" attribute, that BSC desugars into SMT information for one-hot-ness. This attribute may not even be needed explicitly from the user, if it's part of the OInt library or otherwise appears automatically inside certain modules or types.) Of course, it might also be nice if BSC could figure these equations out on its own. For example, some basic model checking could detect that the register is only ever written with one-hot values. (This analysis may be too much to perform on every register, so an attribute could be used to tell BSC to consider it for this register.) However, if values are coming in from outside the current module boundary, then BSC would not be able to check this when code-generating for this module, but would have to check it later, when BSC has the full design. (We'd also have to make sure that we're taking reset values -- and lack of reset values -- into account.) I was trying to think about whether (as another alternative) you could encode the exclusive-ness in the scheduling annotations of an imported Verilog module -- say, a OIntReg module with separate methods for each bit. But I don't believe that BSC currently supports any attributes that would communicate mutual-exclusion. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#417 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB24HQFTJNKODSCSAC7IIELUFJWNJANCNFSM5EWXZXIQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[quark17]

Add the matches keyword to your case to avoid the circular dependency. A non-matching case uses equality to test the arms, while pattern matching uses the structure itself.

However... I wonder if you missed the point of my previous message? Your code did NOT work before. It was NOT generating one-hot Verilog. And that's the reason why scheduling was able to work: because the rule conditions were testing all of the bits of the register (not just a single bit), the SMT analysis could tell that the conditions were exclusive.

Going back to the old behavior means writing rule conditions that look at all the bits.

As I showed with the Verilog snippet above:

wire __d10 = ( (mode_r == 1) || (mode_r == 2) ? mode_r : 4)
RDY_accum = __d10 [0];

Here, the value of bit 0 of __d10 is mode_r == 1, which is testing all of the bits.

Once I have these, the scheduling and verilog problem have been solved

I don't believe that's true. If the Verilog is truly one hot (rule conditions are rg[0] and rg[1]) then scheduling will NOT be able to tell that they are exclusive (until we add a way to assert this for the SMT solver). Older BSC was never able to figure this out either. (Older BSC only worked because your conditions reduced to mode_r==3'b001, mode_r==3'b010 and ! (mode_r==3'b001 || mode_r==3'b010).)

[czeck]

I also found that using primOrd in place of pack works as well. W.r.t. the verilog generated, we have a perl script to modify the generated verilog removing the "default" arm from the case statement in the unpack arm. So during scheduling and the SMT solver the ATS contains decode logic to insure one-hot, conditions, while the final verilog for synthesis the code is one-hot. I.e., always@(mode_r) begin case (mode_r) 3'd1, 3'd2: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = mode_r; default: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = 3'd4; endcase end becomes always@(mode_r) begin case (mode_r) 3'd1, 3'd2: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = mode_r; default: IF_mode_r_read_EQ_1_OR_mode_r_read_EQ_2_THEN_m_ETC___d10 = mode_r; endcase end Synthesis tools will reduce this to __d10 == mode_r; and we have one-hot decode logic! As a project/enhancement I would like to add a scheduling attribute, which is an expression considered during disjoint testing but not included in the output verilog. To support one-hot with this enhancement, the simple (default) pack/unpack instances would be used, A custom Eq instance needed, rule would require the attribute, and no verilog hacking needed. E.g. (* scheduling_assumption = "validDomain(state)" *) rule state1 (state == X1); endrule funcion Bool validDomain(Ex x); return x == X1 || X == X2 ... endfunction Thoughts? Ed.

[quark17]

we have a perl script to modify the generated verilog removing the "default" arm from the case statement in the unpack arm. So during scheduling and the SMT solver the ATS contains decode logic to insure one-hot, conditions

FYI, nothing you're doing about one-hotness was affecting scheduling. Using the default Eq and Bits would give you the same scheduling you were getting before -- so if you're willing to edit the generated Verilog, then you could just use the default Eq and Bits for enums, and then edit the generated Verilog to replace == 1 with [0], == 2 with [1], and == 4 with [2] (that is, introduce the one-hotness in the Verilog, which is the only place where it mattered).

But, yes, I agree that the way forward is to avoid needing any editing of the Verilog, by having BSC elaborate to one-hot conditions (which the latest BSC does just by defining a special Eq instance) and then helping the scheduler to deal with one-hot conditions. However, rather than an attribute, I was thinking of a function that can take actual expressions. For example, the same way that we have addRules, we can have:

addAssumption :: (IsModule m _) => Bool -> m ()

which can be used like this:

Reg#(CS4Mode)    mode_r <- ...;

addAssumption ( (mode_r == 1) || (mode_r == 2) || (mode_r == 4) );

(You could also express it as a series of assumptions that say that mode_r[0] implies not mode_r[1] or mode_r[2] etc. But I assume that's unnecessarily verbose.)

The benefit of writing it this way is that the assumption expression gets parsed and typechecked and becomes a handle to the actual objects, which can be easily converted into SMT objects in the same way that happens for rule conditions (which get parsed, typechecked, and converted to SMT objects for making queries on). Implementing addAssumption would be super easy.

This probably isn't sufficient, though, because we'll also want add assumptions about method arguments. Or about local variables, inside a rule or method (or even a function). In that case, it might be sufficient to make a version of addAssumption that can be called from any context, not just module monads (like unsafeIO). But we may also want to add assumptions that refer across methods (say, that the arguments to two methods will never be the same), and it's not how clear how we can write that in this way -- although maybe we can create a special type of expression that is allowed inside addAssumption arguments, and refers to method arguments, but results in an error if evaluated in any other context.

[czeck]

addAssumption :: (IsModule m _) => Bool -> m () This is wonderful. I was starting to consider if we want to add assumptions to rule syntax E.g. rule <rulename> [assume (<expr>)] [if] [(<predicate>)]; but addAssumption is cleaner and more concise. I think it will be sufficient for what I am looking for in one-hotness, even if it is limited only to module context. Tight scheduling with methods usually involves writing method data to wires. While having assumptions in various contexts may be helpful for lots of things, I see the first use of assumptions in scheduling specifically disjoint tests. We have the SMT solver in place and the assumptions become another expression in the test. I have some old ideas on inductive model checking I need to dust off, where bsc can prove properties, E.g., assume the system lies in a valid state, then any rule fire will transition to a valid state. Maybe addProof :: (IsModule m _) => Bool -> m () This is a topic for another day (month). I don't mind putting in some work on this project. I'll need a little direction to get started. I appreciate your comments, best, Ed.

…

On Tue, Oct 19, 2021 at 4:35 AM Julie Schwartz ***@***.***> wrote: we have a perl script to modify the generated verilog removing the "default" arm from the case statement in the unpack arm. So during scheduling and the SMT solver the ATS contains decode logic to insure one-hot, conditions FYI, nothing you're doing about one-hotness was affecting scheduling. Using the default Eq and Bits would give you the same scheduling you were getting before -- so if you're willing to edit the generated Verilog, then you could just use the default Eq and Bits for enums, and then edit the generated Verilog to replace == 1 with [0], == 2 with [1], and == 4 with [2] (that is, introduce the one-hotness in the Verilog, which is the only place where it mattered). But, yes, I agree that the way forward is to avoid needing any editing of the Verilog, by having BSC elaborate to one-hot conditions (which the latest BSC does just by defining a special Eq instance) and then helping the scheduler to deal with one-hot conditions. However, rather than an attribute, I was thinking of a function that can take actual expressions. For example, the same way that we have addRules, we can have: addAssumption :: (IsModule m _) => Bool -> m () which can be used like this: Reg#(CS4Mode) mode_r <- ...; addAssumption ( (mode_r == 1) || (mode_r == 2) || (mode_r == 4) ); (You could also express it as a series of assumptions that say that mode_r[0] implies not mode_r[1] or mode_r[2] etc. But I assume that's unnecessarily verbose.) The benefit of writing it this way is that the assumption expression gets parsed and typechecked and becomes a handle to the actual objects, which can be easily converted into SMT objects in the same way that happens for rule conditions (which get parsed, typechecked, and converted to SMT objects for making queries on). Implementing addAssumption would be super easy. This probably isn't sufficient, though, because we'll also want add assumptions about method arguments. Or about local variables, inside a rule or method (or even a function). In that case, it might be sufficient to make a version of addAssumption that can be called from any context, not just module monads (like unsafeIO). But we may also want to add assumptions that refer across methods (say, that the arguments to two methods will never be the same), and it's not how clear how we can write that in this way -- although maybe we can create a special type of expression that is allowed inside addAssumption arguments, and refers to method arguments, but results in an error if evaluated in any other context. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#417 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB24HQGX5COJ3PU5XTBOJVLUHUUV7ANCNFSM5EWXZXIQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.

[quark17]

The file ASchedule is where scheduling is done, but all of the SMT handling is asbtracted inside DisjointTest.hs. And DisjointTest.hs is built on top of AExpr2Yices.hs (and AExpr2STP.hs). You'll notice that ASchedule first calls DisjointTest::initDisjointTestState to initialize the SMT solver. Then later, ASchedule calls checkDisjointExpr* to tests if two expressions are disjoint -- and that uses the AExpr2Yices functions to (a) convert the two expressions to Yices objects (hence the name AExpr2Yices) and (b) run a Yices query using those two objects. The AExpr2Yices state that we initialized includes a cache of previously mapped expressions (and ports and defs), so that we're not duplicating the work of converting. And the way that we query disjointness is roughly: assert expression e1 in the current state; assert expression e2; test if the current state has a solution, and if so then that means they are not disjoint; pop the two asserted expressions from the current state/context, so that we can make a fresh query later.

What you'll want to do for addAssumption is to carry that assumption along until ASchedule and then assert those expressions in the Yices state, so that they'll be in the context when queries are made. This could be done by adding the assumptions as a new argument to the init function, but maybe simpler is to just add a new function to DisjointTest which is addAssumpToDisjointTestState (analogous to the existing addADefToDisjointTestState function). Once you've added all of the user's assumptions, you probably want to sanity check that the current context is not contradictory -- and if it is, then report an error. (You'll probably want to write a test that asserts both x==y and x!=y, say.) That check might be best done in the add function, so maybe it should be addAssumps (plural) and take all the assumptions at once and do the sanity check.

To get the assumptions to the scheduler, you will need to add a new field to the IPackage and APackage. The field in the IPackage will get populated by the evaluator (IExpand) and then it will get copied over to the APackage by AConv (which converts from IPackage to APackage).

The way that you populate the field in the evaluator is by creating a new primitive PrimAddAssump -- you can follow how this works for PrimAddRules and do roughly the same thing. That is, in Prelude.bs you will declare primAddAssump and then wrap it as a user function called addAssumption (or whatever). You'll add it to Prims.hs. and then in IExpand.hs you'll add an arm for it in handlePrim, where (and this is where the similarity with PrimAdd stops) you will force evaluation of the expression.

Exactly how to force evaluation is an interesting question. I would suggest using evalNF in the same way that evalRule uses it to fully evaluate the condition c and body e of a rule. You'll note that evalNF returns both an expression and any implicit conditions. If you want, we could start by not supporting assumptions with implicit conditions (see how evaleUH produces an error if the condition is not pTrue). However, we could also keep the condition, as part of the assumption. To do that, you'll want to fully evaluate the predicate expression (with evalPred) and then AND that into the assumption (with ieAnd) in the same way that evalRule adds the implicit condition to the explicit condition. Or, maybe we want to say that the assumption holds when the two conditions are true ... so maybe we need !impcond || assump? (Or maybe you could decide to store a pair of the assumptions and their predicates, in case the SMT solver has a better way of expressing the assumption given a conditions -- I recall that yices might have an implies operator -- but I think NOT-OR should work, yes?) (For example, do we want to write a test case where we assert that f1.first != f2.first for two FIFOs, and have two rules that fire based on each FIFO and check that their actions, based on the value in the FIFOs, are determined not to conflict?)

And I think that's everything?