Approximate medians and their formal verifications

This repository shows implementations of approximate medians described in paper submitted to ISCAS conference. The implementations and their parameters can be found in directories

• netlist netlists for CGP (and for this tool)
• vhdl exports of all proposed

The complete parameters of the proposed medians can be found at the end of this document.

MRAZEK Vojtech and VASICEK Zdeněk. AxMED: Formal Analysis and Automated Design of Approximate Median Filters using BDDs. In: 2025 IEEE International Symposium on Circuits and Systems (ISCAS). London, 2025, p. 5.

@INPROCEEDINGS{mrazek:axmed:iscas25,
   author = "Vojtech Mrazek and Zdenek Vasicek",
   title = "AxMED: Formal Analysis and Automated Design of Approximate Median Filters using BDDs",
   pages = 5,
   booktitle = "2025 IEEE International Symposium on Circuits and Systems (ISCAS)",
   year = 2025,
   location = "London, GB"
}

The netlists can also be combined together using median of medians approach using mom.py script.

# 9-input median of medians (3x 03-input + 1x 03-input)
python3 mom.py 9 netlist/m03.cha netlist/m03.cha | tail -1 > tmp.cha

# 15-input median of medians (5x 03 + 1x 05)
python3 mom.py 15 netlist/m03.cha netlist/m05.cha | tail -1 > tmp.cha


# 15-input median of medians (3x 05 + 1x 03) - as illustrated
python3 mom.py 15 netlist/m05.cha netlist/m03.cha | tail -1 > tmp.cha

# Also the approximate implementations can be used from the netlist folder

This tool is able to determine the histogram of errors for arbitrary approximate median having accurate Compare & swap units but somehow pruned. An example of this median is also median of medians shown the abovementioned folders.

Firstly, it is imporant to build the BuDDy library (for BDDs) and

cmake -B ./build
cmake --build ./build --config Release -j 8 

Then you can test the circuit

./median-validate ../netlist/s_9_3.cha

For details about formal verification, please reffer PrintFitness function in fitnessbdd.cxx folder.

It is possible to export C / VHDL (pipelined) representation

./median-validate -ccode.c ../netlist/s_9_3.cha
./median-validate -varch.vhdl ../netlist/s_9_3.cha