Merge pull request #1880 from GaloisInc/sb/yosys-comp

Yosys: Support compositional translation of sequential circuits

doc/manual/manual.md

@@ -3297,3 +3297,244 @@ problem with this aspect of the translation.
 
 [^5]: https://coq.inria.fr
 [^6]: https://github.com/mit-plv/fiat-crypto
+
+# Analyzing Hardware Circuits using Yosys
+SAW has experimental support for analysis of hardware descriptions written in VHDL ([via GHDL](https://github.com/ghdl/ghdl-yosys-plugin)) through an intermediate representation produced by [Yosys](https://yosyshq.net/yosys/).
+This generally follows the same conventions and idioms used in the rest of SAWScript.
+
+## Processing VHDL With Yosys
+Given a VHDL file `test.vhd` containing an entity `test`, one can generate an intermediate representation `test.json` suitable for loading into SAW:
+
+~~~~
+$ ghdl -a test.vhd
+$ yosys
+...
+Yosys 0.10+1 (git sha1 7a7df9a3b4, gcc 10.3.0 -fPIC -Os)
+yosys> ghdl test
+
+1. Executing GHDL.
+Importing module test.
+
+yosys> write_json test.json
+
+2. Executing JSON backend.
+~~~~
+
+It can sometimes be helpful to invoke additional Yosys passes between the `ghdl` and `write_json` commands.
+For example, at present SAW does not support the `$pmux` cell type.
+Yosys is able to convert `$pmux` cells into trees of `$mux` cells using the `pmuxtree` command.
+We expect there are many other situations where Yosys' considerable library of commands is valuable for pre-processing.
+
+## Example: Ripple-Carry Adder
+Consider three VHDL entities.
+First, a half-adder:
+
+~~~~vhdl
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity half is
+  port (
+    a : in std_logic;
+    b : in std_logic;
+    c : out std_logic;
+    s : out std_logic
+  );
+end half;
+
+architecture halfarch of half is
+begin
+  c <= a and b;
+  s <= a xor b;
+end halfarch;
+~~~~
+
+Next, a one-bit adder built atop that half-adder:
+
+~~~~vhdl
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity full is
+  port (
+    a : in std_logic;
+    b : in std_logic;
+    cin : in std_logic;
+    cout : out std_logic;
+    s : out std_logic
+  );
+end full;
+
+architecture fullarch of full is
+  signal half0c : std_logic;
+  signal half0s : std_logic;
+  signal half1c : std_logic;
+begin
+  half0 : entity work.half port map (a => a, b => b, c => half0c, s => half0s);
+  half1 : entity work.half port map (a => half0s, b => cin, c => half1c, s => s);
+  cout <= half0c or half1c;
+end fullarch;
+~~~~
+
+Finally, a four-bit adder:
+
+~~~~vhdl
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity add4 is
+  port (
+    a : in std_logic_vector(0 to 3);
+    b : in std_logic_vector(0 to 3);
+    res : out std_logic_vector(0 to 3)
+  );
+end add4;
+
+architecture add4arch of add4 is
+  signal full0cout : std_logic;
+  signal full1cout : std_logic;
+  signal full2cout : std_logic;
+  signal ignore : std_logic;
+begin
+  full0 : entity work.full port map (a => a(0), b => b(0), cin => '0', cout => full0cout, s => res(0));
+  full1 : entity work.full port map (a => a(1), b => b(1), cin => full0cout, cout => full1cout, s => res(1));
+  full2 : entity work.full port map (a => a(2), b => b(2), cin => full1cout, cout => full2cout, s => res(2));
+  full3 : entity work.full port map (a => a(3), b => b(3), cin => full2cout, cout => ignore, s => res(3));
+end add4arch;
+~~~~
+
+Using GHDL and Yosys, we can convert the VHDL source above into a format that SAW can import.
+If all of the code above is in a file `adder.vhd`, we can run the following commands:
+
+~~~~
+$ ghdl -a adder.vhd
+$ yosys -p 'ghdl add4; write_json adder.json'
+~~~~
+
+The produced file `adder.json` can then be loaded into SAW with `yosys_import`:
+
+~~~~
+$ saw
+...
+sawscript> enable_experimental
+sawscript> m <- yosys_import "adder.json"
+sawscript> :type m
+Term
+sawscript> type m
+[23:57:14.492] {add4 : {a : [4], b : [4]} -> {res : [4]},
+ full : {a : [1], b : [1], cin : [1]} -> {cout : [1], s : [1]},
+ half : {a : [1], b : [1]} -> {c : [1], s : [1]}}
+~~~~
+
+`yosys_import` returns a `Term` with a Cryptol record type, where the fields correspond to each VHDL module.
+We can access the fields of this record like we would any Cryptol record, and call the functions within like any Cryptol function.
+
+~~~~
+sawscript> type {{ m.add4 }}
+[00:00:25.255] {a : [4], b : [4]} -> {res : [4]}
+sawscript> eval_int {{ (m.add4 { a = 1, b = 2 }).res }}
+[00:02:07.329] 3
+~~~~
+
+We can also use all of SAW's infrastructure for asking solvers about `Term`s, such as the `sat` and `prove` commands.
+For example:
+
+~~~~
+sawscript> sat w4 {{ m.add4 === \_ -> { res = 5 } }}
+[00:04:41.993] Sat: [_ = (5, 0)]
+sawscript> prove z3 {{ m.add4 === \inp -> { res = inp.a + inp.b } }}
+[00:05:43.659] Valid
+sawscript> prove yices {{ m.add4 === \inp -> { res = inp.a - inp.b } }}
+[00:05:56.171] Invalid: [_ = (8, 13)]
+~~~~
+
+The full library of `ProofScript` tactics is available in this setting.
+If necessary, proof tactics like `simplify` can be used to rewrite goals before querying a solver.
+
+Special support is provided for the common case of equivalence proofs between HDL modules and other `Term`s (e.g. Cryptol functions, other HDL modules, or "extracted" imperative LLVM or JVM code).
+The command `yosys_verify` has an interface similar to `llvm_verify`: given a specification, some lemmas, and a proof tactic, it produces evidence of a proven equivalence that may be passed as a lemma to future calls of `yosys_verify`.
+For example, consider the following Cryptol specifications for one-bit and four-bit adders:
+
+~~~~cryptol
+cryfull :  {a : [1], b : [1], cin : [1]} -> {cout : [1], s : [1]}
+cryfull inp = { cout = [cout], s = [s] }
+  where [cout, s] = zext inp.a + zext inp.b + zext inp.cin
+
+cryadd4 : {a : [4], b : [4]} -> {res : [4]}
+cryadd4 inp = { res = inp.a + inp.b }
+~~~~
+
+We can prove equivalence between `cryfull` and the VHDL `full` module:
+
+~~~~
+sawscript> full_spec <- yosys_verify {{ m.full }} [] {{ cryfull }} [] w4;
+~~~~
+
+The result `full_spec` can then be used as an "override" when proving equivalence between `cryadd4` and the VHDL `add4` module:
+
+~~~~
+sawscript> add4_spec <- yosys_verify {{ m.add4 }} [] {{ cryadd4 }} [full_spec] w4;
+~~~~
+
+The above could also be accomplished through the use of `prove_print` and term rewriting, but it is much more verbose.
+
+`yosys_verify` may also be given a list of preconditions under which the equivalence holds.
+For example, consider the following Cryptol specification for `full` that ignores the `cin` bit:
+
+~~~~cryptol
+cryfullnocarry :  {a : [1], b : [1], cin : [1]} -> {cout : [1], s : [1]}
+cryfullnocarry inp = { cout = [cout], s = [s] }
+  where [cout, s] = zext inp.a + zext inp.b
+~~~~
+
+This is not equivalent to `full` in general, but it is if constrained to inputs where `cin = 0`.
+We may express that precondition like so:
+
+~~~~
+sawscript> full_nocarry_spec <- yosys_verify {{ adderm.full }} [{{\(inp : {a : [1], b : [1], cin : [1]}) -> inp.cin == 0}}] {{ cryfullnocarry }} [] w4;
+~~~~
+
+The resulting override `full_nocarry_spec` may still be used in the proof for `add4` (this is accomplished by rewriting to a conditional expression).
+
+## API Reference
+N.B: The following commands must first be enabled using `enable_experimental`.
+
+* `yosys_import : String -> TopLevel Term` produces a `Term` given the path to a JSON file produced by the Yosys `write_json` command.
+  The resulting term is a Cryptol record, where each field corresponds to one HDL module exported by Yosys.
+  Each HDL module is in turn represented by a function from a record of input port values to a record of output port values.
+  For example, consider a Yosys JSON file derived from the following VHDL entities:
+  ~~~~vhdl
+  entity half is
+    port (
+      a : in std_logic;
+      b : in std_logic;
+      c : out std_logic;
+      s : out std_logic
+    );
+  end half;
+  
+  entity full is
+    port (
+      a : in std_logic;
+      b : in std_logic;
+      cin : in std_logic;
+      cout : out std_logic;
+      s : out std_logic
+    );
+  end full;
+  ~~~~
+  The resulting `Term` will have the type:
+  ~~~~
+  { half : {a : [1], b : [1]} -> {c : [1], s : [1]}
+  , full : {a : [1], b : [1], cin : [1]} -> {cout : [1], s : [1]}
+  }
+  ~~~~
+* `yosys_verify : Term -> [Term] -> Term -> [YosysTheorem] -> ProofScript () -> TopLevel YosysTheorem` proves equality between an HDL module and a specification.
+  The first parameter is the HDL module - given a record `m` from `yosys_import`, this will typically look something like `{{ m.foo }}`.
+  The second parameter is a list of preconditions for the equality.
+  The third parameter is the specification, a term of the same type as the HDL module, which will typically be some Cryptol function or another HDL module.
+  The fourth parameter is a list of "overrides", which witness the results of previous `yosys_verify` proofs.
+  These overrides can be used to simplify terms by replacing use sites of submodules with their specifications.
+
+  Note that `Term`s derived from HDL modules are "first class", and are not restricted to `yosys_verify`: they may also be used with SAW's typical `Term` infrastructure like `sat`, `prove_print`, term rewriting, etc.
+  `yosys_verify` simply provides a convenient and familiar interface, similar to `llvm_verify` or `jvm_verify`.

saw-script.cabal

@@ -192,6 +192,7 @@ library
     SAWScript.Yosys.State
     SAWScript.Yosys.Theorem
     SAWScript.Yosys.TransitionSystem
+    SAWScript.Yosys.CompositionalTranslation
     SAWScript.Yosys.Utils
 
   other-modules:

src/SAWScript/Yosys.hs

@@ -30,11 +30,12 @@ module SAWScript.Yosys
 
 import Control.Lens.TH (makeLenses)
 
-import Control.Lens (view, (^.))
+import Control.Lens (view, (^.), (.~))
 import Control.Exception (throw)
 import Control.Monad (foldM)
 import Control.Monad.IO.Class (MonadIO(..))
 
+import Data.Function ((&))
 import qualified Data.List.NonEmpty as NE
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -60,10 +61,10 @@ import qualified SAWScript.Crucible.Common as Common
 
 import SAWScript.Yosys.Utils
 import SAWScript.Yosys.IR
-import SAWScript.Yosys.Netgraph
 import SAWScript.Yosys.State
 import SAWScript.Yosys.Theorem
 import SAWScript.Yosys.TransitionSystem
+import qualified SAWScript.Yosys.CompositionalTranslation as Comp
 
 --------------------------------------------------------------------------------
 -- ** Building the module graph from Yosys IR
@@ -82,7 +83,7 @@ yosysIRModgraph ir =
     moduleToNode :: (Text, Module) -> (Module, Text, [Text])
     moduleToNode (nm, m) = (m, nm, deps)
       where
-        deps = view cellType <$> Map.elems (m ^. moduleCells)
+        deps = Text.pack . show . view cellType <$> Map.elems (m ^. moduleCells)
     nodes = moduleToNode <$> Map.assocs (ir ^. yosysModules)
     (_modgraphGraph, _modgraphNodeFromVertex, _modgraphVertexFromKey)
       = Graph.graphFromEdges nodes
@@ -93,15 +94,15 @@ convertYosysIR ::
   MonadIO m =>
   SC.SharedContext ->
   YosysIR ->
-  m (Map Text ConvertedModule)
+  m (Map Text Comp.TranslatedModule)
 convertYosysIR sc ir = do
   let mg = yosysIRModgraph ir
   let sorted = reverseTopSort $ mg ^. modgraphGraph
   foldM
     (\env v -> do
         let (m, nm, _) = mg ^. modgraphNodeFromVertex $ v
-        cm <- convertModule sc env m
-        _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ cm ^. convertedModuleTerm
+        tm <- Comp.translateModule sc env m
+        _ <- validateTerm sc ("translating the combinational circuit \"" <> nm <> "\"") $ tm ^. Comp.translatedModuleTerm
         n <- liftIO $ Nonce.freshNonce Nonce.globalNonceGenerator
         let frag = Text.pack . show $ Nonce.indexValue n
         let uri = URI.URI
@@ -112,9 +113,9 @@ convertYosysIR sc ir = do
               , URI.uriFragment = URI.mkFragment frag
               }
         let ni = SC.ImportedName uri [nm]
-        tc <- liftIO $ SC.scConstant' sc ni (cm ^. convertedModuleTerm) (cm ^. convertedModuleType)
-        let cm' = cm { _convertedModuleTerm = tc }
-        pure $ Map.insert nm cm' env
+        tc <- liftIO $ SC.scConstant' sc ni (tm ^. Comp.translatedModuleTerm) (tm ^. Comp.translatedModuleType)
+        let tm' = tm & Comp.translatedModuleTerm .~ tc
+        pure $ Map.insert nm tm' env
     )
     Map.empty
     sorted
@@ -127,10 +128,10 @@ yosysIRToTypedTerms ::
   m (Map Text SC.TypedTerm)
 yosysIRToTypedTerms sc ir = do
   env <- convertYosysIR sc ir
-  pure . flip fmap env $ \cm ->
+  pure . flip fmap env $ \tm ->
     SC.TypedTerm
-    (SC.TypedTermSchema $ C.tMono $ cm ^. convertedModuleCryptolType)
-    $ cm ^. convertedModuleTerm
+    (SC.TypedTermSchema $ C.tMono $ tm ^. Comp.translatedModuleCryptolType)
+    $ tm ^. Comp.translatedModuleTerm
 
 -- | Given a Yosys IR, construct a SAWCore record containing terms for each module
 yosysIRToRecordTerm ::
@@ -140,8 +141,8 @@ yosysIRToRecordTerm ::
   m SC.TypedTerm
 yosysIRToRecordTerm sc ir = do
   env <- convertYosysIR sc ir
-  record <- cryptolRecord sc $ view convertedModuleTerm <$> env
-  let cty = C.tRec . C.recordFromFields $ (\(nm, cm) -> (C.mkIdent nm, cm ^. convertedModuleCryptolType)) <$> Map.assocs env
+  record <- cryptolRecord sc $ view Comp.translatedModuleTerm <$> env
+  let cty = C.tRec . C.recordFromFields $ (\(nm, tm) -> (C.mkIdent nm, tm ^. Comp.translatedModuleCryptolType)) <$> Map.assocs env
   let tt = SC.TypedTerm (SC.TypedTermSchema $ C.tMono cty) record
   pure tt