Subscribe to the OHO Newsletter Description of the OHO System (paper) IP (Intellectual Property) issues OHO - OBDD Heuristics Online This is a system that allows the use of a number of BDD-based tools online. The User can submit benchmarks via web-form. These benchmarks are then executed on a cluster of Computers and the results are reported to the user by email or web page. Intentions behind the OHO system The intention of OHO is to facilitate the evaluation of OBDD heuristics developed by the OBDD group in Trier for everyone interested. Classically evaluation of such heuristics mean you would have to compile a larger and not easy to use pice of software, deal with bugs and portability problems and other troubles. It may even be that you would have to reimplement the heuristic. If you want to include a new heuristic into some special OBDD package, you will have to reimplement it, but before you do, you might have some indication whether this is worth your while. The first such indication is given by the tables included in the scientific paper describing the heuristic. But that is usually not enough. OHO fills the gap between these tables and building the software yourself, by letting you do limited experiments on a standard platform without great effort. OHO can also give you indications what heuristic would be best suited for some kind of circuit class you might be working in. How to use OHO You can just explore the site and read about the OBDD heuristics contained. However, if you want to try one of the heuristics, say Block Restricted Sifting, you have to learn a bit about the tool the heuristic is included in. If you are, e.g. interested in what Block Restricted Sifting may do for combinatoric verification, you may want to have the OBDD for some (combinatoric) circuit synthesised. In this case you might want to use the Block Restricted Sifting added to the tool Nanotrav. Just go to the OHO user interface page and select the submit form for Block Restricted Sifting with Nanotrav. The for will show you some parameters you can modify and ask you to submit a file describing the circuit in the BLIF format or to select one of the predefined files. If you are unsure about the Parameters, go back to the heuristics page and read the short description or other documentation linked next to the link to the submit form. If you want to learn what this BLIF format is, you can select the name directly to be taken to some documentation. Let's now assume, you have your circuit description (BLIF) and have chosen the parameter(s) to your liking. Transfer the file with the file transfer element of the form and select the submit button on the bottom of the form. You will be take to a short confirmation page, stating what you just requested, and giving an ID for the request. You need this ID only if you submitted more circuits and requested notification via email. In that case you might need the ID to tell which notification corresponds to which request. Now click the continue button and be taken to the results page for your request. It will show you whether your job is waiting to be executed (and in that case how much other jobs will be processed before your job is), welter it is active and if it is done it will give the results. These result pages have some parameters in their URL and for that reason can be bookmarked. If you didn't specify a notification email address, you can get results only via the specific results page for your job. That's it! Of course you might want to experiment with the parameters or try different circuits. Just keep in mind, that the computational power of this system is limited. It my be that jobs taking longer than some minutes will be executed at night, or my be stored for some time. However no job should be lost. Technical Details Computations are currently done on 3 Pentium Pro 200 workstations, running Linux. Should all machines be busy, the newly submitted benchmarks will wait in a queue until a machine becomes free. At the moment there is no limit on this waiting time, meaning every submission will be processed eventually. Limits on the actual execution are: Memory: 80 MB Time: 2 hour cpu time Input file size: 1 MB The memory limit is checked by an external program and the computation will be killed externally if the limit is exceeded. At the moment the user cannot modify these limits. As we are upgrading our computing equipment at the moment, this numbers will change in the near future. Please be patient if computations are slow at the moment, fewer than 3 machines might be available because of the upgrades. We expect to have around 5-10 Pentium III 500 cpu's available for the computations in the near future.