#lang yosys

  produced from the following Verilog :
;
; module counter(
      input clk ,
      input nrst ,
;     input en,
      output [ 7:0 ] count ,
; );
      reg [ 7:0 ] count ;
;
;     always @(posedge clk) begin
;         if (!nrst) begin
              count < = 8'h0 ;
;         end
;         else if (en) begin
              count < = count + 1 ;
;         end
;     end
; endmodule

; by running the command:
;
  yosys -p ' read_verilog counter.v ' -p ' prep ' -p ' write_smt2  counter.rkt '

  SMT - LIBv2 description generated by Yosys 0.9 + 2406 ( git sha1 584780d7 , clang 10.0.1 -fPIC -Os )
; yosys-smt2-stdt
; yosys-smt2-module counter
(declare-datatype |counter_s| ((|counter_mk|
  (|counter_is| Bool)
  (|counter#0| Bool) ; \clk
  (|counter#1| (_ BitVec 8)) ; \count
  (|counter#2| Bool) ; \en
  (|counter#3| Bool) ; \nrst
)))
  yosys - smt2 - input clk 1
; yosys-smt2-clock clk posedge
(define-fun |counter_n clk| ((state |counter_s|)) Bool (|counter#0| state))
  yosys - smt2 - output count 8
  yosys - smt2 - register count 8
(define-fun |counter_n count| ((state |counter_s|)) (_ BitVec 8) (|counter#1| state))
  yosys - smt2 - input en 1
(define-fun |counter_n en| ((state |counter_s|)) Bool (|counter#2| state))
  yosys - smt2 - input nrst 1
(define-fun |counter_n nrst| ((state |counter_s|)) Bool (|counter#3| state))
(define-fun |counter#4| ((state |counter_s|)) (_ BitVec 8) (bvadd (|counter#1| state) #b00000001)) ; $add$counter.v:14$3_Y
(define-fun |counter#5| ((state |counter_s|)) (_ BitVec 8) (ite (|counter#2| state) (|counter#4| state) (|counter#1| state))) ; $procmux$4_Y
  $ 0\count[7:0 ]
(define-fun |counter_a| ((state |counter_s|)) Bool true)
(define-fun |counter_u| ((state |counter_s|)) Bool true)
(define-fun |counter_i| ((state |counter_s|)) Bool true)
(define-fun |counter_h| ((state |counter_s|)) Bool true)
(define-fun |counter_t| ((state |counter_s|) (next_state |counter_s|)) Bool
  (= (|counter#6| state) (|counter#1| next_state)) ; $procdff$9 \count
) ; end of module counter
; yosys-smt2-topmod counter
; end of yosys output


 module counter(
     input en,
 );


     always @(posedge clk) begin
         if (!nrst) begin

         end
         else if (en) begin

         end
     end
 endmodule
 by running the command:

 yosys-smt2-stdt
 yosys-smt2-module counter
 \clk
 \count
 \en
 \nrst
 yosys-smt2-clock clk posedge
 $add$counter.v:14$3_Y
 $procmux$4_Y
 $procdff$9 \count
 end of module counter
 yosys-smt2-topmod counter
 end of yosys output
#lang yosys

  produced from the following Verilog :
      input clk ,
      input nrst ,
      output [ 7:0 ] count ,

  yosys -p ' read_verilog counter.v ' -p ' prep ' -p ' write_smt2  counter.rkt '

  SMT - LIBv2 description generated by Yosys 0.9 + 2406 ( git sha1 584780d7 , clang 10.0.1 -fPIC -Os )
(declare-datatype |counter_s| ((|counter_mk|
  (|counter_is| Bool)
)))
  yosys - smt2 - input clk 1
(define-fun |counter_n clk| ((state |counter_s|)) Bool (|counter#0| state))
  yosys - smt2 - output count 8
  yosys - smt2 - register count 8
(define-fun |counter_n count| ((state |counter_s|)) (_ BitVec 8) (|counter#1| state))
  yosys - smt2 - input en 1
(define-fun |counter_n en| ((state |counter_s|)) Bool (|counter#2| state))
  yosys - smt2 - input nrst 1
(define-fun |counter_n nrst| ((state |counter_s|)) Bool (|counter#3| state))
  $ 0\count[7:0 ]
(define-fun |counter_a| ((state |counter_s|)) Bool true)
(define-fun |counter_u| ((state |counter_s|)) Bool true)
(define-fun |counter_i| ((state |counter_s|)) Bool true)
(define-fun |counter_h| ((state |counter_s|)) Bool true)
(define-fun |counter_t| ((state |counter_s|) (next_state |counter_s|)) Bool
