I've seen people do similar things in D (although the "D way" of doing it would probably be to parse some kind of textual description and turn it into code at compile time). The cost/benefit of making a metaprogramming library just to write a lexer is fairly bad, however.

wrt to the SMT integration, it's something that I would very much like to try in D, but it's quite difficult to work out exactly where to start (and means bolting a fairly big dependency on the compiler). There also seems to be a big gap in the literature between "practical" verification done "in" the widget being verified (e.g. SystemVerilog code) and more academic work where, effectively, a parallel structure is built which represents the semantics of the widget.