Tech Tip: Distributing Incisive Enterprise Verifier (IEV) Engines and Assertions with LSF and Enterprise Manager

A common problem when distributing engines and assertions in Incisive Enterprise Verifier (IEV) and Incisive Enterprise Manager (EMGR) at the same time using LSF with big machines is the following: if you use the "define engine auto_dist" setting, but only reserve 1 slot in LSF, then IEV will spawn off more than 16 processes within each job, overloading the machine quickly. The attention of your IT department will be guaranteed.  Hence, we recommend against using auto_dist on LSF (unless you reserve 16 slots per LSF job, which is unreasonably high and will probably never get scheduled).

Instead, we recommend to set the engine to 2 or 3 of the best performing engines (for example "sword3", "bow", and one "halo" (auto)) and submit them to LSF requesting 2 slots with the switch setting "-n 2".  (A little bit overloading is probably ok, since on average we typically use less than 2 CPUs over the proof time.)

Another recommendation is to set the max_number_parallel_runs in EMGR to about the same number of licenses available, and not much higher than the LSF job limit per user.  Otherwise you will find 1,000 jobs in the pending queue of LSF or the license manager, which can make killing a session a mess.

If you want to learn more about distribution using LSF, and alternative strategies for optimizing the number of engines automatically to match the reserved slots in LSF, do not hesitate to contact us.

Joerg Muller
Solutions Engineer
for Team Verify

On Twitter: http://twitter.com/teamverify, @teamverify