unknown
 
| About ALCom | News | People | Research | Publications | Tools | Student Info | Links |
unknown

 

ResQu

News

      -  2011-07:  Version 0.1 released
      -  2013-05:  Version 1.0 released (now also works with QRP)
      -  2014-05:  Version 2.0 released (can perform certificate minimization)
      -  2015-01:  Version LP  released (works with LQ resolution proofs)

Description

      - ResQu is a tool for deriving Herbrand/Skolem functions from Q-resolution and Q-consensus proofs.
      - Input formats:

- QBC (proof formats of Squolem, EBDDRES);
- Proof format of Qube-cert;
- QRP (Proof format of cDepQBF);
- RFAO (local input format as a right-firat-and-or formula just for certificate optimization)

      - Output formats: BLIF (format of ABC synthesis tool), RFAO (same as above)

Link

      ResQu


 

Software Workaround Benchmarks

News

      -  2013-02:  Released

Download

      SWW Benchmarks

Description

      - This set of benchmark examples was used in the experiments of software workaround of microprocessor errors of the following paper.

References

      Tsung-Po Liu, Shuo-Ren Lin, and Jie-Hong R. Jiang. Software Workarounds for Hardware Errors: Instruction Patch Synthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), to appear.

 


   
© 2007 Applied Logic and Computation Laboratory, GIEE, NTU. All rights reserved.