add a manpage for yosys-smtbmc

Also add infrastructure for building manpages with txt2man, lifted from
fpga-icestorm.

7 files changed, 62 insertions, 0 deletions

diff --git a/debian/changelog b/debian/changelog
index 9db98e18..570b6f64 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -7,6 +7,7 @@ yosys (0.6-1) UNRELEASED; urgency=medium
     - don't run make as part of dh_auto_configure, it'll get run by
         dh_auto_build later
     - enable parallel build
+  * add a manpage for the new yosys-smtbmc executable
 
  -- Sebastian Kuzminsky <seb@highlab.com>  Sun, 28 Feb 2016 10:48:44 -0700
 
diff --git a/debian/control b/debian/control
index 35b4616d..07c3d4cc 100644
--- a/debian/control
+++ b/debian/control
@@ -12,6 +12,7 @@ Build-Depends: debhelper (>= 9),
                gawk,
                libffi-dev,
                pkg-config,
+               txt2man,
                python3
 Standards-Version: 3.9.7
 Vcs-Browser: https://anonscm.debian.org/cgit/debian-science/packages/yosys.git
diff --git a/debian/man/.gitignore b/debian/man/.gitignore
new file mode 100644
index 00000000..f7e585b8
--- /dev/null
+++ b/debian/man/.gitignore
@@ -0,0 +1 @@
+*.1
diff --git a/debian/man/genmanpages.sh b/debian/man/genmanpages.sh
new file mode 100755
index 00000000..8c6f6e71
--- /dev/null
+++ b/debian/man/genmanpages.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+txt2man -d "${CHANGELOG_DATE}" -t YOSYS-SMTBMC -s 1 yosys-smtbmc.txt > yosys-smtbmc.1
diff --git a/debian/man/yosys-smtbmc.txt b/debian/man/yosys-smtbmc.txt
new file mode 100644
index 00000000..3f2df5fc
--- /dev/null
+++ b/debian/man/yosys-smtbmc.txt
@@ -0,0 +1,44 @@
+NAME
+  yosys-smtbmc - write design to SMT2-LIBv2 file
+
+SYNOPSIS
+  yosys-smtbmc [options] <yosys_smt2_output>
+
+OPTIONS
+
+  -t [<skip_steps>:]<num_steps>  
+      default: skip_steps=0, num_steps=20
+
+  -u <start_step>  
+      assume asserts in skipped steps in BMC
+
+  -S <step_size>  
+      proof <step_size> time steps at once
+
+  -c <vcd_filename>  
+      write counter-example to this VCD file (hint: use 'write_smt2
+      -wires' for maximum coverage of signals in generated VCD file)
+
+  -i  
+      instead of BMC run temporal induction
+
+  -m <module_name>  
+      name of the top module
+
+  -s <solver>  
+      Set SMT solver: z3, cvc4, yices, mathsat. default: z3
+
+  -v  
+      enable debug output
+
+  -p  
+      disable timer display during solving
+
+  -d <filename>  
+      write smt2 statements to file
+
+ 
+AUTHOR
+
+  This manual page was written by Sebastian Kuzminsky <seb@highlab.com>
+  for the Debian project (and may be used by others).
diff --git a/debian/rules b/debian/rules
index 3146665e..10dc50d8 100755
--- a/debian/rules
+++ b/debian/rules
@@ -5,9 +5,20 @@
 
 export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed
 
+CHANGELOG_DATE ?= $(shell LC_ALL=C date -u -d "`dpkg-parsechangelog --show-field Date`" +"%d %B %Y")
+
+
 %:
 	PREFIX=/usr dh $@ --parallel
 
 
+override_dh_auto_clean:
+	dh_auto_clean
+	$(RM) debian/man/*.1
+
 override_dh_auto_configure:
 	make config-gcc
+
+override_dh_installman:
+	cd debian/man ; CHANGELOG_DATE="$(CHANGELOG_DATE)" ./genmanpages.sh
+	dh_installman
diff --git a/debian/yosys.manpages b/debian/yosys.manpages
index bc62137a..11159f1d 100644
--- a/debian/yosys.manpages
+++ b/debian/yosys.manpages
@@ -2,3 +2,4 @@ debian/yosys.1
 debian/yosys-config.1
 debian/yosys-filterlib.1
 debian/yosys-abc.1
+debian/man/*.1