diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-05-19 22:13:02 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-05-19 22:13:02 +0100 |
commit | fe60271a6a57955497ca96127916f96f1ee6e20c (patch) | |
tree | 7c5572533da487d19fe3968ad464c201822cf40e /src/Verismith/Verilog/CodeGen.hs | |
parent | 97cac4b338962c6311721efdf9422c6d6e4baec0 (diff) | |
download | verismith-fe60271a6a57955497ca96127916f96f1ee6e20c.tar.gz verismith-fe60271a6a57955497ca96127916f96f1ee6e20c.zip |
Add formal properties to AST
Diffstat (limited to 'src/Verismith/Verilog/CodeGen.hs')
-rw-r--r-- | src/Verismith/Verilog/CodeGen.hs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Verismith/Verilog/CodeGen.hs b/src/Verismith/Verilog/CodeGen.hs index 9c7a6da..9a4c12c 100644 --- a/src/Verismith/Verilog/CodeGen.hs +++ b/src/Verismith/Verilog/CodeGen.hs @@ -133,6 +133,12 @@ moduleItem (Decl dir p ini) = moduleItem (ParamDecl p) = hcat [paramList p, semi] moduleItem (LocalParamDecl p) = hcat [localParamList p, semi] moduleItem (ModItemAnn a mi) = sep [hsep ["/*", pretty $ show a, "*/"], moduleItem mi] +moduleItem (Property l e bl br) = + sep [hcat [identifier l, ":"], "assume property", parens $ event e, + hcat [case bl of + Just bl' -> sep [expr bl', "|=>", expr br] + Nothing -> expr br, semi] + ] mConn :: ModConn -> Doc a mConn (ModConn c) = expr c |