this line set default behaviour of reset to synchronous one. in both cases. checker could not work with async version.

Also I don't think mix the verification code into function ones is a good idea, even when the output synthesible code is consistent.

The coupling is not preferred in modern engineering, which make things hard to read and debug.

For verification of StreamFifo, see this file. The Fifo is the first component verified by an inductive prover.

this line set default behaviour of reset to synchronous one. in both cases. checker could not work with async version.

Should the SpinalFormal config just use sync resets across the board then? I get this behavior even with formal tests I didn't modify; so I think something must be different on my setup than say the CI server.

The coupling is not preferred in modern engineering, which make things hard to read and debug.

Where should it go then? I considered making a trait with a function like withFormalAsserts that could be recursively activated but it seemed elaborate. It would, though, allow for something like withFormalAssumuptions though which might me nice to have.

The main use case I want to enable here is that if someone wants to perform formal analysis on their design which incorporates library components like these, it's easy and doesn't require calling them out individually in the higher levels test harness. With even the BMC formal methods, the higher level component doesn't need those asserts at all but withProve tends to need all of those asserts to make meaningful results.

For verification of StreamFifo, see this file. The Fifo is the first component verified by an inductive prover.

That isn't an inductive proof of StreamFifo, it's a unit test for it -- which is great but not needed for the induction case. The inductive proof for StreamFifo is here: https://github.com/SpinalHDL/SpinalHDL/blob/dev/tester/src/test/scala/spinal/tester/scalatest/FormalFifoTester.scala.

Part of the idea with this PR is that the asserts here: https://github.com/SpinalHDL/SpinalHDL/blob/dev/tester/src/test/scala/spinal/tester/scalatest/FormalFifoTester.scala#L104 being only in the test harness is not useful if you have a StreamFifo in your design and want to run withProve on your design -- without these asserts to keep the SMT solvers on the rails you just get a bunch of irrelevant results.

For instance, the added inductive proof for PipelinedMemoryBusArbiter relies on the asserts around StreamFifo being active.

this line set default behaviour of reset to synchronous one. in both cases. checker could not work with async version.

Should the SpinalFormal config just use sync resets across the board then? I get this behavior even with formal tests I didn't modify; so I think something must be different on my setup than say the CI server.

If I remember right, it is merged in the latest 1.11.0 or 1.10.2a. Where I have fixed some conceptual bugs on.

The coupling is not preferred in modern engineering, which make things hard to read and debug.

Where should it go then? I considered making a trait with a function like withFormalAsserts that could be recursively activated but it seemed elaborate. It would, though, allow for something like withFormalAssumuptions though which might me nice to have.

I sugguest to define formalXXXX function into corresponding component, and call it in your doVerify implementation, or called by other formalYYYY method using this component.

The main use case I want to enable here is that if someone wants to perform formal analysis on their design which incorporates library components like these, it's easy and doesn't require calling them out individually in the higher levels test harness. With even the BMC formal methods, the higher level component doesn't need those asserts at all but withProve tends to need all of those asserts to make meaningful results.

For verification of StreamFifo, see this file. The Fifo is the first component verified by an inductive prover.

That isn't an inductive proof of StreamFifo, it's a unit test for it -- which is great but not needed for the induction case. The inductive proof for StreamFifo is here: https://github.com/SpinalHDL/SpinalHDL/blob/dev/tester/src/test/scala/spinal/tester/scalatest/FormalFifoTester.scala.

Right, that's the place.

Part of the idea with this PR is that the asserts here: https://github.com/SpinalHDL/SpinalHDL/blob/dev/tester/src/test/scala/spinal/tester/scalatest/FormalFifoTester.scala#L104 being only in the test harness is not useful if you have a StreamFifo in your design and want to run withProve on your design -- without these asserts to keep the SMT solvers on the rails you just get a bunch of irrelevant results.

I can understand that, and agree these part is important for usage. Put some commonly required assertion into formalXXXX method is for this purpose.

For instance, the added inductive proof for PipelinedMemoryBusArbiter relies on the asserts around StreamFifo being active.

Does the pattern in 3109aa5 work? I didn't do it to everything, just enough to get a feel for how it'd work (StreamFifo, StreamArbiter, PMBArbiter).

Generate notes:

• It requires breaking some areas out (ie rspSingle and rspQueue areas) to get access to their internals. I don't think this is a big deal though.
• I think the WithFormalAsserts trait is ultimately required with this approach -- so many library helper functions construct components you ultimately don't have a handle for (myStream.queue(cnt) for instance) and so you'd want to be able to just walkComponents recursively to activate them

If I remember right, it is merged in the latest 1.11.0 or 1.10.2a. Where I have fixed some conceptual bugs on.

I'm working off of dev which would have those? Looking into it further, it only happens when there are asserts inside a component with FormalDut called on it. The generated SV has the asserts in a async reset clock even as the rest of the logic for that component properly has the sync resets. I can open a separate issue for this if you want.

I've been testing this locally on one of my own designs / test benches and have some notes on the approach:

• The trait approach seems to work for the most part. Where it does seem to not work though is things which generate just a composite / area instead of a component -- those things are not registered or walkable at all from their containing component (AFAICT anyway), and so can not be conditionally activated. For now I just invoke them unconditionally inline.
• I think having asserts inside a FormalDut component needs to be allowed and handled in a way that doesn't break sby. I'm not sure the best way to do that. For now, I pushed 6b56b1d which sets the reset clock for formal testing to default as SYNC, and for testing that relies on it being ASYNC, there is a mutator for it. I mostly did this just to get unit testing working on this PR; there is some context around why it was set as ASYNC before and I don't have a strong opinion on which is the default.
• Due to the asserts being inlined for composite / area, the asserts are included in other testing. I don't think this is bad necessarily. It did require 1dd6993 though to lock down the initial reset line for the test to pass.

I think a reasonable approach is for those small load bearing things needed in the various utility areas (roundRobin, Counter, StateMachine, etc) to be invoked inline as assumes and to have the larger chunks of logic tied to the formalAsserts of their respective component. I could have those classes implement the FormalAsserts trait to for traceability, or just not to keep it simple.

I'll probably rename WithFormalAsserts to HasFormalAsserts unless another name seems better. with WithFormalAsserts looks goofy.

I've been testing this locally on one of my own designs / test benches and have some notes on the approach:

• The trait approach seems to work for the most part. Where it does seem to not work though is things which generate just a composite / area instead of a component -- those things are not registered or walkable at all from their containing component (AFAICT anyway), and so can not be conditionally activated. For now I just invoke them unconditionally inline.

That's why I suggest designing a calling tree to formalAsserts method explicitly.

• I think having asserts inside a FormalDut component needs to be allowed and handled in a way that doesn't break sby. I'm not sure the best way to do that. For now, I pushed 6b56b1d which sets the reset clock for formal testing to default as SYNC, and for testing that relies on it being ASYNC, there is a mutator for it. I mostly did this just to get unit testing working on this PR; there is some context around why it was set as ASYNC before and I don't have a strong opinion on which is the default.

According to tutorial -> multi-clocked section from ZipCPU, even verification of asynchronous design is using clocks and resets synchronized with the globalclk. I rememeber that there is a demo checker for FIFOCC.

So the default clock domain of FormalDut has been set to SYNC kind in formal verification.
Is it necessary to set all ClockDomain in DUT component into SYNC mode?

• Due to the asserts being inlined for composite / area, the asserts are included in other testing. I don't think this is bad necessarily. It did require 1dd6993 though to lock down the initial reset line for the test to pass.

The initial reset status could be done by assumeInitial I suppose. From the link above, the default reset is set when the default domain's reset active, and fixed to high level kind, it seems that not decoupled with clock domain.

I think a reasonable approach is for those small load bearing things needed in the various utility areas (roundRobin, Counter, StateMachine, etc) to be invoked inline as assumes and to have the larger chunks of logic tied to the formalAsserts of their respective component. I could have those classes implement the FormalAsserts trait to for traceability, or just not to keep it simple.

Because the keyword assert have at least two usages, one is for status checking during simulation, the other is for formal verification. So that I personally think assert in design for the first use case, and assert in formalXXX method for the second one might be a better solution.

I'll probably rename WithFormalAsserts to HasFormalAsserts unless another name seems better. with WithFormalAsserts looks goofy.

That's why I suggest designing a calling tree to formalAsserts method explicitly.

As far as I know, this would require adding a mechanism to link areas to their refOwner component in the general case; which doesn't exist currently. In the simple case where you have a handle to the area -- such as CounterUpDown this could be made to work maybe but there are a ton of examples where you wont necessarily have that handle or type erasure kicks in -- stream arbiters have a few of these kinds of areas, SteamFork2 also drops the logic area. I think there are a lot of overrides and convenience functions that do this.

For child components, I have it using walkComponents to handle calling formalAsserts -- there are a ton of cases too where you don't have any kind of handle to the child component and so this is required but there is a component tree to walk and so that works.

Because the keyword assert have at least two usages, one is for status checking during simulation, the other is for formal verification. So that I personally think assert in design for the first use case, and assert in formalXXX method for the second one might be a better solution.

AFAIK, assume usage is far less overloaded so if these were just invoked inline as assume; I think it has minimal impact. In all the ones I've added so far they are pretty short 1 or 2 line additions. The options I understand to be at play here:

• Add a way to iterate through areas at the component level ala walkComponents that could be triggered from a components formalAssert call.
• Force the user to refactor to expose an area handle so they can call formalAsserts on whatever area subclass needs it.
• Have the necessary assume calls in Area classes with state be invoked inline

The first option seems like a substantial change that I'm sure has a bunch of corner cases to add and consider. The second makes it much harder to add formal tests to a user component and maybe impossible in some cases (for instance if you have something like an interconnect which creates areas with state). The third option has the downside of the assumptions being present everywhere but I can't think of any way this breaks any existing designs or simulations.

So the default clock domain of FormalDut has been set to SYNC kind in formal verification.
Is it necessary to set all ClockDomain in DUT component into SYNC mode?

I'm not sure on this. The FifoCC formal test doesn't work if you set it to a SYNC reset. I didn't dig a ton into why this was the case. Since StreamFifoCC doesn't have inline asserts, it works in ASYNC mode. I think if you walked the design and put only the asserts under a sync clock, it seems like this might also miss real issues in a design around async resets.

I think a default SYNC reset for formal methods here is pragmatic given the limitations in sby but I'm not sure what downsides that as a default presents and I imagine there are some.

For child components, I have it using walkComponents to handle calling formalAsserts -- there are a ton of cases too where you don't have any kind of handle to the child component and so this is required but there is a component tree to walk and so that works.

How about add an optional function for internal formal assertions and run them during the FormalPhase.
But implicitly call this function would lead to amount of implicit calling which makes it very difficult to debug, especially for ones who is not know things well.

AFAIK, assume usage is far less overloaded so if these were just invoked inline as assume; I think it has minimal impact. In all the ones I've added so far they are pretty short 1 or 2 line additions. The options I understand to be at play here:

• Add a way to iterate through areas at the component level ala walkComponents that could be triggered from a components formalAssert call.
• Force the user to refactor to expose an area handle so they can call formalAsserts on whatever area subclass needs it.
• Have the necessary assume calls in Area classes with state be invoked inline

The first option seems like a substantial change that I'm sure has a bunch of corner cases to add and consider. The second makes it much harder to add formal tests to a user component and maybe impossible in some cases (for instance if you have something like an interconnect which creates areas with state). The third option has the downside of the assumptions being present everywhere but I can't think of any way this breaks any existing designs or simulations.

assume is not play important in induction proof. In that mode, every assertion would be used as assumption for next k-induction inference. So for the target to simplify induction assumption, it is best to embbed several key synchronization assert inside the component is enough.

I'm not sure on this. The FifoCC formal test doesn't work if you set it to a SYNC reset. I didn't dig a ton into why this was the case. Since StreamFifoCC doesn't have inline asserts, it works in ASYNC mode. I think if you walked the design and put only the asserts under a sync clock, it seems like this might also miss real issues in a design around async resets.

When you use the FormalDut, it will generate SYNC reset even you use Clock Domain with async reset, it's for purpose.
The generated SV code is in synchronouse reset pattern.

There are functions in GlobalClock to synchronize the async resets, if you do not call that functions, the resets are async theoritically.
The functions include assumeResetReleaseSync, assumeIOSync2Clock, alignAsyncResetStart, etc.

I think a default SYNC reset for formal methods here is pragmatic given the limitations in sby but I'm not sure what downsides that as a default presents and I imagine there are some.

Overall, I think your most important pain point is the lack of assertion on internal signal's synchronization of facilities provide in lib. You want to call those assertion methods automatically by default, so that you can concentrate on the verification by interface. Did I get it right?

If so, how about add a traits with optional function which can be executed at FormalPhase for all components and areas.

For now, the method name could be formalAsserts, as it is already in StreamFifoCC and StreamTransactionCounter

The only problem is that formalAsserts is also used by Axi4's formalContext which is a composite generating helper logic for bus verification. If we change the define of Composite by adding trait with optional formalAsserts and run by default, then this code might be affected.
In this stage, it could be changed.

At last, the most important if we want to run the formalAsserts by default, as I described firstly?
@Dolu1990

assume is not play important in induction proof. In that mode, every assertion would be used as assumption for next k-induction inference. So for the target to simplify induction assumption, it is best to embbed several key synchronization assert inside the component is enough.

I think if you want any hope in scaling a formal proof to a complicated design I think it only works if you can do two things:
a) Formally prove the sub-components of that design individually
b) In the design under test, have the sub-components assume their properties rather than assert them.

Assuming that the sub-components properties are actually valid, I would of course expect whether it passes or fails induction to be the same but when set as assumes it would take less time.

Overall, I think your most important pain point is the lack of assertion on internal signal's synchronization of facilities provide in lib. You want to call those assertion methods automatically by default, so that you can concentrate on the verification by interface. Did I get it right?

This is mostly right. Calling them automatically isn't a goal in and of itself for me though -- it is just the most straight forward way to invoke them in instances where there is no handle to call it explicitly.

I guess to take a step back -- is there a way to traverse a components areas like there is for traversing a components nested components? I did not find one and assume one doesn't exist. But if there was a walkAreas in the style of walkComponents, it'd make sense to never call any of these functions implicitly.

For now, the method name could be formalAsserts, as it is already in StreamFifoCC and StreamTransactionCounter

The only problem is that formalAsserts is also used by Axi4's formalContext which is a composite generating helper logic for bus verification. If we change the define of Composite by adding trait with optional formalAsserts and run by default, then this code might be affected.
In this stage, it could be changed.

The PR as it is now has that function. I think the usages of formalAsserts in those instances matches the intention of the overrides in the trait; but if there is some conflict we can rename the ones in the HasFormalAsserts trait.

At last, the most important if we want to run the formalAsserts by default, as I described firstly?

I do think we should only ever do assumes by default if we have defaults. This is enough to make the induction provers happy without impacting simulations with an unknown reset line at startup.

I did add another optional function to that trait --

This makes it more straight forward to add asserts at the interface, but also offers a place on components to formally specify any particularities in what they expect on their interface. For StreamFifo I am somewhat tempted to add an assertion assert(!io.flush || !io.pop.isStall). I papered over this in the Formal test runner but without it, the pop stream can be technically invalid.

I think if you want any hope in scaling a formal proof to a complicated design I think it only works if you can do two things: a) Formally prove the sub-components of that design individually b) In the design under test, have the sub-components assume their properties rather than assert them.

I remember that there is a discussion on the ZipCPU's blog about this kind of hierarchical verification in practice, may be it worth to read.
I searched a while, fortunatly I find it and read again, serveral years later.:)

I remember that there is a discussion on the ZipCPU's blog about this kind of hierarchical verification in practice, may be it worth to read.

I had read that before but hadn't internalized it properly I think. It's a good point. I swapped the formalAssertInputs to instead require a formalValidInputs predicate to be specified. This predicates formalAssumes like so:

In this way it never assumes something unless the input to the component is valid.

To prove it, I also added a test case loosely based on the blog post that shows it fails when the top level input constraints aren't applied.

I'd have to benchmark to be sure but I think this still has a large performance improvement. Since we typically will assert that the inputs into a nested component are valid, it will demonstrate the predicate is an invariant to the system (or fail to do so and error out) and then add all the given assumptions as known lemmas as opposed to trying to prove them all out individually.

For the implicit / explicit areas thing -- if I added areas list to Component in the same way that children are, would that be an acceptable addition to the library? I don't particularly like mucking around with central objects like that but it'd mean nothing had to be called automatically and might end up being a relatively simple change that maybe other features could end up using. I could submit this as another PR and rebase this one on top of it.

So the target could be add an option withInternalInputAsserts to FormalConfig. So that if it is true, then all formalAssertInputs are called by default. If not, user can call it manually.
Is this good enough?

If so extend Component and Area's definition to extend HasFormalAsserts by default is a solution.

The principal issue though is that there isn't a list / tree of areas we can walk through. Whether we do it from the Phase context or the top level design object we would need such a mechanism? Having that be a part of Component seems more and more like it makes sense to me.

I did benchmark it loosely, it's about twice as fast with the PipelinedMemoryBus formal testers to allow it to use assumptions for nested components instead of asserts.

The principal issue though is that there isn't a list / tree of areas we can walk through. Whether we do it from the Phase context or the top level design object we would need such a mechanism? Having that be a part of Component seems more and more like it makes sense to me.

I did benchmark it loosely, it's about twice as fast with the PipelinedMemoryBus formal testers to allow it to use assumptions for nested components instead of asserts.

The first possible thing is to change the define of Area and Component to

// Here I have changed the name HasFormalAsserts into FormalAssertable.
trait Area extends NameableByComponent with ContextUser with OwnableRef with ScalaLocated with ValCallbackRec with OverridedEqualsHashCode with FormalAssertable

abstract class Component extends NameableByComponent with ContextUser with ScalaLocated with PostInitCallback with Stackable with OwnableRef with SpinalTagReady with OverridedEqualsHashCode with ValCallbackRec with FormalAssertable

In the FormalAssertable, we define a formalAssertInputs method only, so that in FormalPhase we might do following things.

          s match {
            case t: FormalAssertable => t.formalAssertInputs()
            case _ => 
          }

@Dolu1990 is that possible to apply such a big change to Area and Component?

The second is to define formalAssertInputs in Area case by case.

c = new Component(){
  val test = new Area{
    def formalAssertInputs() {
      assert(io.never_true === False)
    }
  }

  def formalAssertInput() {
    test.formalAssertInputs()
  }
}

// in doVerify you can call
dut.formalAssertInput()

The shortage of this way is that some object apply method just return the output Stream which do not hold the instance, so that it could not call the formalAssertInputs correspondingly.

The shortage of this way is that some object apply method just return the output Stream which do not hold the instance, so that it could not call the formalAssertInputs correspondingly.

This is why I've been sort of fixated on being able to walk through created areas -- there are enough of these patterns (rightly so -- they are much cleaner overall) in play that it seems required.

Here I have changed the name HasFormalAsserts into FormalAssertable.

I can make this name change if desired; let me know what works for everyone.

I don't think we should extend Area and Component with the trait though. The way it works in the PR now it just attaches to Component / Areas that need it and that seems to work well. You can still run that exact match code block this way too.

I think the big change required though is maintaining a tree of areas for a component. Not sure if that is too big of a change.

Quasi related -- I get that there isn't a solid spec written around PipelinedMemoryBus but a thing I've run afoul of before is whether or not async response are allowed (ie, cmd.fire and rsp.valid for that command in the same clock cycle). I have the code written as of now to NOT allow that since the arbiter does not work with async responses. I sort of think that should be fixed and such usages allowed but wanted to get a sense of if this case has been decided firmly one way or another.

I don't think we should extend Area and Component with the trait though. The way it works in the PR now it just attaches to Component / Areas that need it and that seems to work well. You can still run that exact match code block this way too.

The problem is that we need to change the interface of facilities involved one by one. There might be a lot.

I think the big change required though is maintaining a tree of areas for a component. Not sure if that is too big of a change.

In formal phase, you can traverse all statements, where all assignment, init and related strings are structed and can be accessed.

Quasi related -- I get that there isn't a solid spec written around PipelinedMemoryBus but a thing I've run afoul of before is whether or not async response are allowed (ie, cmd.fire and rsp.valid for that command in the same clock cycle). I have the code written as of now to NOT allow that since the arbiter does not work with async responses. I sort of think that should be fixed and such usages allowed but wanted to get a sense of if this case has been decided firmly one way or another.

I suggest to split this PR into several ones, we have talked too much in this thread.