Request pointers on unbounded model checking in IVy

[zgzn]

We have been working on checking existence of an infinite state-transition path for a complex network-on-chip routing algorithm. Dr. McMillan mentioned the unbounded model checking and in counterexample generation in IVy. We would like to get some pointers and a simple example on how we may use it. Thank you.

[kenmcmil]

There's a very simple example of using unbounded model checking in:

ivy/doc/examples/client_server_example_mv.ivy

For unbounded model checking, all your types have to be finite, which means either enumerated types or bit vector types. I can provide some more complex examples of unbounded model checking if you are interested.

To use unbounded model checking, you need to install the abc model checker, which is available here:

https://github.com/berkeley-abc/abc

For bounded model checking, you can use unbounded data types. Add this statement in your .ivy file:

attribute method = bmc[N]

where N is the upper bound on the number of actions in the trace.

[landonjefftaylor]

Thank you for the pointers. After following those instructions, I have a couple of follow-up questions:

1. Is there a specific requirement to invoke this model checker from the command line (ivy ___.ivy, ivy_check ___.ivy, etc)?
2. Upon testing using ivy_check client_server_example_mv.ivy, I run into an error as follows:

   
   Isolate this:

---

clientsrv_mc.ivy: line 27: Model checking invariant

Instantiating quantifiers (see ivy_mc.log for instantiations)... Expanding schemata... Instantiating axioms... error: failed to run aigtoaig

I have ABC and AIGER installed.

Thank you.

[kenmcmil]

1. You can choose model checking for a given isolate by putting this directive in the isolate:

   attribute method = mc

or, on the command line, you can use mc=true to check all isolates with model checking.

2. Have you checked that aigtoaig and abc are in your path?

[landonjefftaylor]

Thank you for such a speedy reply! That solved the problem (I just completely forgot to add AIGER to the path). Now, the model checker appears to be working well.