Overview Search Downloads Up
Category: Interpolant Compaction
Order by: Default | Name | Date | Hits | [Descending]
Files:
Readme

Download
Download

README

In order to reproduce the experimental results presented in our journal pubblication "Logic Synthesis for Interpolant Circuit Compaction", we present in this txt file a description of PdTRAV and ABC commands used.




Created
Size
Downloads
2018-02-16 13:18:02
1.23 KB
11
PdTrav (static linux exe) Version:3.4.0

Download
Download

PdTRAV (Politecnico di Torino Reachability Analysis & Verification)

PdTRAV is an academic tool developed by the Formal Methods Group, as a platform to evaluate Model Checking algorithms. So far it should not be considered as a development/verification tool, but rather as a collection of MC engines.

PdTRAV's most powerful engines are based on Craig interpolation, on BDDs, on IC3.
We also have a multithreaded version of the tool, running several tools on a "winner-takes-it-all" basis. 

 




Created
Size
Downloads
2018-02-14 16:29:50
13.07 MB
11
Single Output Interpolants

Download
Download

Set of selected interpolants used for benchmarking. 

Interpolants were extracted, as single-output AIG circuits, from model checking runs on publicly available benchmarks from the HWMCC set (http://fmv.jku.at/hwmcc17/). 
They were selected by considering size, SAT time, and circuit sampling, among non trivially solved problems.




Created
Size
Downloads
2018-01-24 14:32:52
492.68 MB
14